Processing profiles and Pareto comparison

[LV05]

A ProcessingProfile records the ordinal difficulty of a linguistic dependency along four dimensions (locality, boundaries crossed, referential load, retrieval ease). Profiles are compared by Pareto dominance — the partial order that is the product of the three cost dimensions with the dualized ease dimension — so a condition counts as harder only when it is worse-or-equal on every dimension and strictly worse on one; conflicting dimensions are honestly incomparable. Core.Optimization.Linearization characterizes this order: dominance is exactly agreement of every strictly positive weighted-sum reading, so no magic weights are chosen here.

Main definitions

• ProcessingProfile — the four ordinal dimensions, with the PartialOrder instance a ≤ b = "a at most as hard as b".
• ProcessingProfile.compare — the four-way readout of the order (harder / easier / equal / incomparable).
• HasProcessingProfile, OrderingPrediction, verifyOrdering — the interface studies use to state and decide ordinal difficulty predictions.

Main results

• compare_eq_harder (and siblings) — compare answers exactly the order.
• locality_monotone (and siblings) — increasing a cost dimension cannot make processing easier.

structure ProcessingModel.ProcessingProfile : Type

A processing profile characterizing the difficulty of a linguistic dependency. Each dimension is ordinal (higher = more of that factor); comparison is via Pareto dominance — no numeric aggregation.

• locality : ℕ

  Distance (words/nodes) between filler and integration site

• boundaries : ℕ

  Clause or phrase boundaries crossed

• referentialLoad : ℕ

  Referential processing load from intervening material (0 = none/pronominal, 1 = indefinite, 2 = definite/proper name)

• ease : ℕ

  Retrieval facilitation: richer fillers, higher predictability (higher = easier retrieval, so this dimension is dualized in comparison)

def ProcessingModel.instReprProcessingProfile.repr : ProcessingProfile → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ProcessingModel.instReprProcessingProfile : Repr ProcessingProfile

Equations

• ProcessingModel.instReprProcessingProfile = { reprPrec := ProcessingModel.instReprProcessingProfile.repr }

def ProcessingModel.instDecidableEqProcessingProfile.decEq (x✝ x✝¹ : ProcessingProfile) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ProcessingModel.instDecidableEqProcessingProfile : DecidableEq ProcessingProfile

Equations

• ProcessingModel.instDecidableEqProcessingProfile = ProcessingModel.instDecidableEqProcessingProfile.decEq

inductive ProcessingModel.CompareResult : Type

Result of comparing two processing profiles via Pareto dominance.

• harder : CompareResult

  Worse-or-equal on all dimensions, strictly worse on at least one.

• easier : CompareResult

  Better-or-equal on all dimensions, strictly better on at least one.

• equal : CompareResult

  Identical on all dimensions.

• incomparable : CompareResult

  Some dimensions harder, some easier.

@[implicit_reducible]

instance ProcessingModel.instReprCompareResult : Repr CompareResult

Equations

• ProcessingModel.instReprCompareResult = { reprPrec := ProcessingModel.instReprCompareResult.repr }

def ProcessingModel.instReprCompareResult.repr : CompareResult → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ProcessingModel.instDecidableEqCompareResult : DecidableEq CompareResult

Equations

• ProcessingModel.instDecidableEqCompareResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ProcessingModel.ProcessingProfile.instLE : LE ProcessingProfile

Pareto order: a ≤ b iff a is at most as hard as b — at most as high on every cost dimension and at least as high on ease.

Equations

• One or more equations did not get rendered due to their size.

theorem ProcessingModel.ProcessingProfile.le_def {a b : ProcessingProfile} : a ≤ b ↔ a.locality ≤ b.locality ∧ a.boundaries ≤ b.boundaries ∧ a.referentialLoad ≤ b.referentialLoad ∧ b.ease ≤ a.ease

@[implicit_reducible]

instance ProcessingModel.ProcessingProfile.instPartialOrder : PartialOrder ProcessingProfile

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ProcessingModel.ProcessingProfile.instDecidableLE : DecidableLE ProcessingProfile

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.locality ≤ x✝.locality ∧ x✝¹.boundaries ≤ x✝.boundaries ∧ x✝¹.referentialLoad ≤ x✝.referentialLoad ∧ x✝.ease ≤ x✝¹.ease) ⋯

@[implicit_reducible]

instance ProcessingModel.ProcessingProfile.instDecidableLT : DecidableLT ProcessingProfile

Equations

• a.instDecidableLT b = decidable_of_iff (a ≤ b ∧ ¬b ≤ a) ⋯

def ProcessingModel.ProcessingProfile.compare (a b : ProcessingProfile) : CompareResult

The four-way readout of the Pareto order.

Equations

• One or more equations did not get rendered due to their size.

theorem ProcessingModel.ProcessingProfile.compare_eq_equal {a b : ProcessingProfile} : a.compare b = CompareResult.equal ↔ a = b

theorem ProcessingModel.ProcessingProfile.compare_eq_harder {a b : ProcessingProfile} : a.compare b = CompareResult.harder ↔ b < a

theorem ProcessingModel.ProcessingProfile.compare_eq_easier {a b : ProcessingProfile} : a.compare b = CompareResult.easier ↔ a < b

theorem ProcessingModel.ProcessingProfile.compare_eq_incomparable {a b : ProcessingProfile} : a.compare b = CompareResult.incomparable ↔ ¬a ≤ b ∧ ¬b ≤ a

Monotonicity

Increasing a cost dimension (or decreasing ease) cannot make processing easier — one-line consequences of the order.

theorem ProcessingModel.ProcessingProfile.locality_monotone (p : ProcessingProfile) (k : ℕ) : { locality := p.locality + k + 1, boundaries := p.boundaries, referentialLoad := p.referentialLoad, ease := p.ease }.compare p ≠ CompareResult.easier

More locality → not easier (working memory decay).

theorem ProcessingModel.ProcessingProfile.boundaries_monotone (p : ProcessingProfile) (k : ℕ) : { locality := p.locality, boundaries := p.boundaries + k + 1, referentialLoad := p.referentialLoad, ease := p.ease }.compare p ≠ CompareResult.easier

More boundaries → not easier (interference at retrieval).

theorem ProcessingModel.ProcessingProfile.referentialLoad_monotone (p : ProcessingProfile) (k : ℕ) : { locality := p.locality, boundaries := p.boundaries, referentialLoad := p.referentialLoad + k + 1, ease := p.ease }.compare p ≠ CompareResult.easier

More referential load → not easier (similarity-based interference).

theorem ProcessingModel.ProcessingProfile.ease_monotone (p : ProcessingProfile) (k : ℕ) : { locality := p.locality, boundaries := p.boundaries, referentialLoad := p.referentialLoad, ease := p.ease + k + 1 }.compare p ≠ CompareResult.harder

More ease → not harder (facilitation aids retrieval).

class ProcessingModel.HasProcessingProfile (α : Type) : Type

Typeclass for types that can be mapped to processing profiles: the shared vocabulary modules use to state processing-based predictions.

• profile : α → ProcessingProfile

structure ProcessingModel.OrderingPrediction (α : Type) [HasProcessingProfile α] : Type

An ordering prediction: condition harder should be harder than easier.

• harder : α
• easier : α
• description : String

@[implicit_reducible]

instance ProcessingModel.instReprOrderingPrediction {α✝ : Type} {inst✝ : HasProcessingProfile α✝} [Repr α✝] : Repr (OrderingPrediction α✝)

Equations

• ProcessingModel.instReprOrderingPrediction = { reprPrec := ProcessingModel.instReprOrderingPrediction.repr }

def ProcessingModel.instReprOrderingPrediction.repr {α✝ : Type} {inst✝ : HasProcessingProfile α✝} [Repr α✝] : OrderingPrediction α✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def ProcessingModel.verifyOrdering {α : Type} [HasProcessingProfile α] (pred : OrderingPrediction α) : Bool

Verify that Pareto ordering matches the predicted direction.

Equations

• One or more equations did not get rendered due to their size.