Fortuny (2024): Deducing the Coordinand Constraint

Fortuny deduces the Coordinand Constraint, Grosu's half of Ross's Coordinate Structure Constraint, that no coordinand may be moved (5). A coordinator is Steedman's categorial-grammar functor (X/X)/X (10), so two constituents coordinate exactly when they are of one category, and a category is its set of generalized categorial features together with its bar-level features (12), (18)–(21). The Coordinability Condition (22) is therefore a theorem (coordinable_iff), not a stipulation. A coordinand moved for a criterial feature the other coordinand lacks is not coordinable with it (Case 1, not_coordinable_of_mem_of_notMem), and neither are two coordinands moved for different features (Case 2, subcase I). Categorially identical coordinands fall under the Integrity Condition (50), by which a probe targets the coordinate structure and never a coordinand within it, and the same constituent cannot occupy both coordinated positions (71), a coordination the coordinator's denotation makes semantically vacuous (Coordinator.denote_pair_self).

The paper's judgments are the rows of Data/Examples/Fortuny2024.json; rows_predicted checks them against the three-factor decomposition, and rows_factor that each ill-formed coordination falls under exactly one factor, as §2.3 claims.

Implementation notes

• Movement is not derived: the rows record which coordinands move, and the Integrity Condition is stated as the paper states it, with its Least Effort rationale (58) as superfluous_of_twice.
• Base categorial features are the paper's [D], [P], [C], [I], [V], [Adj] of (14) plus the criterial [wh], [focus], [topic] ([Riz97]) and the unvalued case feature of (59)–(62); bar-level features follow [Muy82]. All coordinands in the data are maximal projections.
• Feature percolation (§2.2.1.3) is recorded on the rows rather than computed.

References

• [For24]
• [Gro73]
• [Ros67]
• [Ste85]
• [Muy82]
• [Riz97]
• [Cho91]
• [Zha10]

Categories as feature clusters (§2.1)

structure Fortuny2024.BarLevel : Type

The bar-level features of [Muy82] make a minimal category [−projected, −maximal], an intermediate one [+projected, −maximal] and a maximal one [+projected, +maximal] (18)–(20).

• projected : Bool
• maximal : Bool

@[instance_reducible]

instance Fortuny2024.instDecidableEqBarLevel : DecidableEq BarLevel

Equations

• Fortuny2024.instDecidableEqBarLevel = Fortuny2024.instDecidableEqBarLevel.decEq

def Fortuny2024.instDecidableEqBarLevel.decEq (x✝ x✝¹ : BarLevel) : Decidable (x✝ = x✝¹)

Equations

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

def Fortuny2024.instReprBarLevel.repr : BarLevel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Fortuny2024.instReprBarLevel : Repr BarLevel

Equations

• Fortuny2024.instReprBarLevel = { reprPrec := Fortuny2024.instReprBarLevel.repr }

def Fortuny2024.BarLevel.max : BarLevel

A maximal projection is projected and maximal.

Equations

• Fortuny2024.BarLevel.max = { projected := true, maximal := true }

inductive Fortuny2024.CatFeature : Type

The generalized categorial features (12) determine a constituent's distribution. They are the base categories of (14), the criterial features of the left periphery ([Riz97]) that trigger internal Merge (23), and the unvalued case feature of (59)–(62).

• D : CatFeature
• P : CatFeature
• C : CatFeature
• I : CatFeature
• V : CatFeature
• Adj : CatFeature
• wh : CatFeature
• focus : CatFeature
• topic : CatFeature
• uCase : CatFeature

@[instance_reducible]

instance Fortuny2024.instDecidableEqCatFeature : DecidableEq CatFeature

Equations

• Fortuny2024.instDecidableEqCatFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Fortuny2024.instReprCatFeature : Repr CatFeature

Equations

• Fortuny2024.instReprCatFeature = { reprPrec := Fortuny2024.instReprCatFeature.repr }

def Fortuny2024.instReprCatFeature.repr : CatFeature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Fortuny2024.instReprCatFeature.repr Fortuny2024.CatFeature.D prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.CatFeature.D")).group prec✝
• Fortuny2024.instReprCatFeature.repr Fortuny2024.CatFeature.P prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.CatFeature.P")).group prec✝
• Fortuny2024.instReprCatFeature.repr Fortuny2024.CatFeature.C prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.CatFeature.C")).group prec✝
• Fortuny2024.instReprCatFeature.repr Fortuny2024.CatFeature.I prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.CatFeature.I")).group prec✝
• Fortuny2024.instReprCatFeature.repr Fortuny2024.CatFeature.V prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.CatFeature.V")).group prec✝

structure Fortuny2024.Category : Type

A category is its categorial features and its bar level (18)–(21).

• cf : Finset CatFeature
• bar : BarLevel

theorem Fortuny2024.Category.ext_iff {x y : Category} : x = y ↔ x.cf = y.cf ∧ x.bar = y.bar

theorem Fortuny2024.Category.ext {x y : Category} (cf : x.cf = y.cf) (bar : x.bar = y.bar) : x = y

def Fortuny2024.instDecidableEqCategory.decEq (x✝ x✝¹ : Category) : Decidable (x✝ = x✝¹)

Equations

• Fortuny2024.instDecidableEqCategory.decEq { cf := a, bar := a_1 } { cf := b, bar := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Fortuny2024.instDecidableEqCategory : DecidableEq Category

Equations

• Fortuny2024.instDecidableEqCategory = Fortuny2024.instDecidableEqCategory.decEq

theorem Fortuny2024.Category.eq_iff (a b : Category) : a = b ↔ a.cf = b.cf ∧ a.bar = b.bar

Categorial identity is identity of categorial and bar-level features (21).

The categorematic coordinator (10)–(11)

inductive Fortuny2024.CGType : Type

Among the categorial-grammar types over categories, slash r a selects an a and yields an r.

• of : Category → CGType
• slash : CGType → CGType → CGType

@[instance_reducible]

instance Fortuny2024.instDecidableEqCGType : DecidableEq CGType

Equations

• Fortuny2024.instDecidableEqCGType = Fortuny2024.instDecidableEqCGType.decEq

def Fortuny2024.instDecidableEqCGType.decEq (x✝ x✝¹ : CGType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Fortuny2024.instDecidableEqCGType.decEq (Fortuny2024.CGType.of a) (Fortuny2024.CGType.of b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Fortuny2024.instDecidableEqCGType.decEq (Fortuny2024.CGType.of a) (a_1.slash a_2) = isFalse ⋯
• Fortuny2024.instDecidableEqCGType.decEq (a.slash a_1) (Fortuny2024.CGType.of a_2) = isFalse ⋯

def Fortuny2024.CGType.apply : CGType → CGType → Option CGType

Functional application of r / a to a yields r.

Equations

• (r.slash a).apply x✝ = if a = x✝ then some r else none
• (Fortuny2024.CGType.of a).apply x✝ = none

def Fortuny2024.coord (X : Category) : CGType

A coordinator is (X/X)/X (10). It selects an internal coordinand of category X, yields X/X, selects an external coordinand of category X, and yields a coordinate structure of category X.

Equations

• Fortuny2024.coord X = ((Fortuny2024.CGType.of X).slash (Fortuny2024.CGType.of X)).slash (Fortuny2024.CGType.of X)

def Fortuny2024.coordinate (X α β : Category) : Option CGType

coordinate X α β applies the coordinator to the internal coordinand β and then to the external coordinand α (11).

Equations

• Fortuny2024.coordinate X α β = ((Fortuny2024.coord X).apply (Fortuny2024.CGType.of β)).bind fun (x : Fortuny2024.CGType) => x.apply (Fortuny2024.CGType.of α)

theorem Fortuny2024.coordinate_eq (X α β : Category) : coordinate X α β = if X = β ∧ X = α then some (CGType.of X) else none

theorem Fortuny2024.coordinate_eq_some_iff (X α β : Category) : coordinate X α β = some (CGType.of X) ↔ α = X ∧ β = X

The coordination projects X exactly when both coordinands are of category X.

theorem Fortuny2024.coord_apply_single (X : Category) : (coord X).apply (CGType.of X) = some ((CGType.of X).slash (CGType.of X))

Applied to a single coordinand, the coordinator is the unsaturated X/X (66), the structure a sideward-moved coordinate phrase would land in (65).

def Fortuny2024.Coordinable (α β : Category) : Prop

Two constituents are coordinable when some category is projected for them (22).

Equations

• Fortuny2024.Coordinable α β = ∃ (X : Fortuny2024.Category), Fortuny2024.coordinate X α β = some (Fortuny2024.CGType.of X)

theorem Fortuny2024.coordinable_iff (α β : Category) : Coordinable α β ↔ α.cf = β.cf ∧ α.bar = β.bar

The Coordinability Condition (22) follows from the categorematic coordinator (10) and categorial identity (21), since two constituents are coordinable iff they have the same categorial and bar-level features.

@[instance_reducible]

instance Fortuny2024.instDecidableCoordinable (α β : Category) : Decidable (Coordinable α β)

Equations

• Fortuny2024.instDecidableCoordinable α β = decidable_of_iff (α.cf = β.cf ∧ α.bar = β.bar) ⋯

Case 1 and Case 2, subcase I (§2.2.1, §2.2.2.1)

theorem Fortuny2024.not_coordinable_of_mem_of_notMem {α β : Category} {φ : CatFeature} (hα : φ ∈ α.cf) (hβ : φ ∉ β.cf) : ¬Coordinable α β

A coordinand carrying a categorial feature the other lacks, as when it alone is attracted by a probe for that feature (23), is not coordinable with it (24).

The Integrity Condition (50) and its rationale (§2.2.2.2)

inductive Fortuny2024.Position : Type

A probe might target the whole coordinate structure or one of its two coordinands.

• whole : Position
• left : Position
• right : Position

@[instance_reducible]

instance Fortuny2024.instDecidableEqPosition : DecidableEq Position

Equations

• Fortuny2024.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fortuny2024.instReprPosition.repr : Position → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Fortuny2024.instReprPosition.repr Fortuny2024.Position.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.Position.left")).group prec✝

@[instance_reducible]

instance Fortuny2024.instReprPosition : Repr Position

Equations

• Fortuny2024.instReprPosition = { reprPrec := Fortuny2024.instReprPosition.repr }

structure Fortuny2024.CoordStructure : Type

A well-formed coordinate structure has a coordinator of some role with two coordinands of one category X, which it projects.

• role : Coordinator.Role
• X : Category

def Fortuny2024.CoordStructure.Goal (cs : CoordStructure) (φ : CatFeature) (p : Position) : Prop

In a well-formed coordinate structure of category X whose coordinands carry φ, a probe searching for [+φ] targets the coordinate structure and not a coordinand within it (50).

Equations

• cs.Goal φ p = (φ ∈ cs.X.cf ∧ p = Fortuny2024.Position.whole)

theorem Fortuny2024.CoordStructure.not_goal_coordinand (cs : CoordStructure) (φ : CatFeature) : ¬cs.Goal φ Position.left ∧ ¬cs.Goal φ Position.right

In Pattern 1 (51b), (53), neither coordinand is a goal, so the coordinands cannot move to separate specifiers, with or without the coordinate structure.

theorem Fortuny2024.CoordStructure.goal_uCase (r : Coordinator.Role) : { role := r, X := { cf := {CatFeature.D, CatFeature.uCase}, bar := BarLevel.max } }.Goal CatFeature.uCase Position.whole ∧ ¬{ role := r, X := { cf := {CatFeature.D, CatFeature.uCase}, bar := BarLevel.max } }.Goal CatFeature.uCase Position.left

A probe for the unvalued case feature targets a DP coordination as a whole, so a single coordinand cannot raise to the subject position (59)–(62).

def Fortuny2024.Derivation : Type

A derivation records the positions moved for each feature.

Equations

• Fortuny2024.Derivation = (Fortuny2024.CatFeature → List Fortuny2024.Position)

def Fortuny2024.Derivation.Superfluous (d : Derivation) : Prop

A derivation is superfluous when a coordinand moves twice for one feature, once on its own and once inside the coordinate structure (58), which the Least Effort Principle (79) bans.

Equations

• d.Superfluous = ∃ (φ : Fortuny2024.CatFeature), Fortuny2024.Position.whole ∈ d φ ∧ (Fortuny2024.Position.left ∈ d φ ∨ Fortuny2024.Position.right ∈ d φ)

theorem Fortuny2024.superfluous_of_twice (φ : CatFeature) : Derivation.Superfluous fun (ψ : CatFeature) => if ψ = φ then [Position.left, Position.right, Position.whole] else []

Moving the coordinate structure and both coordinands to specifiers of one head is superfluous (53).

The Prohibition against Self-Coordination (71)

structure Fortuny2024.Occurrence : Type

An occurrence of a constituent records its category and the derivational step at which it entered the computation (fn. 16), so two selections of one constituent are two occurrences.

• cat : Category
• step : ℕ

def Fortuny2024.instDecidableEqOccurrence.decEq (x✝ x✝¹ : Occurrence) : Decidable (x✝ = x✝¹)

Equations

• Fortuny2024.instDecidableEqOccurrence.decEq { cat := a, step := a_1 } { cat := b, step := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Fortuny2024.instDecidableEqOccurrence : DecidableEq Occurrence

Equations

• Fortuny2024.instDecidableEqOccurrence = Fortuny2024.instDecidableEqOccurrence.decEq

def Fortuny2024.WellFormed (α β : Occurrence) : Prop

A coordination is well formed only if its coordinands are coordinable and are distinct occurrences, so a constituent cannot appear in both coordinated positions (71). Such a coordination would also be semantically vacuous, the coordinator's operation returning the constituent (Coordinator.denote_pair_self), which §2.3 relates to the Least Effort Principle.

Equations

• Fortuny2024.WellFormed α β = (Fortuny2024.Coordinable α.cat β.cat ∧ α ≠ β)

The judgments

inductive Fortuny2024.Moved : Type

A probe outside the coordinate structure attracts no coordinand, one, both, or the whole.

• none : Moved
• left : Moved
• right : Moved
• both : Moved
• whole : Moved

@[instance_reducible]

instance Fortuny2024.instDecidableEqMoved : DecidableEq Moved

Equations

• Fortuny2024.instDecidableEqMoved x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Fortuny2024.instReprMoved : Repr Moved

Equations

• Fortuny2024.instReprMoved = { reprPrec := Fortuny2024.instReprMoved.repr }

def Fortuny2024.instReprMoved.repr : Moved → ℕ → Std.Format

Equations

• Fortuny2024.instReprMoved.repr Fortuny2024.Moved.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.Moved.none")).group prec✝
• Fortuny2024.instReprMoved.repr Fortuny2024.Moved.left prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.Moved.left")).group prec✝
• Fortuny2024.instReprMoved.repr Fortuny2024.Moved.right prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.Moved.right")).group prec✝
• Fortuny2024.instReprMoved.repr Fortuny2024.Moved.both prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.Moved.both")).group prec✝
• Fortuny2024.instReprMoved.repr Fortuny2024.Moved.whole prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fortuny2024.Moved.whole")).group prec✝

structure Fortuny2024.Row : Type

A coordination of the data records the two coordinands' categories, which of them move, and whether they are one and the same occurrence.

• left : Category
• right : Category
• moved : Moved
• same : Bool
• judgment : Judgment

@[instance_reducible]

instance Fortuny2024.instDecidableEqRow : DecidableEq Row

Equations

• Fortuny2024.instDecidableEqRow = Fortuny2024.instDecidableEqRow.decEq

def Fortuny2024.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

def Fortuny2024.Moved.Coordinand : Moved → Prop

m.Coordinand says that a coordinand, and not the whole, is attracted, which the Integrity Condition (50) forbids.

Equations

• Fortuny2024.Moved.left.Coordinand = True
• Fortuny2024.Moved.right.Coordinand = True
• Fortuny2024.Moved.both.Coordinand = True
• Fortuny2024.Moved.none.Coordinand = False
• Fortuny2024.Moved.whole.Coordinand = False

@[instance_reducible]

instance Fortuny2024.instDecidablePredMovedCoordinand : DecidablePred Moved.Coordinand

Equations

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

def Fortuny2024.Row.Factor (r : Row) : Fin 3 → Prop

The three factors of §2.3 are that the coordinands are not coordinable (10)/(22), that they are but a coordinand is attracted (50), and that the coordinands are one occurrence (71).

Equations

• r.Factor 0 = ¬Fortuny2024.Coordinable r.left r.right
• r.Factor 1 = (Fortuny2024.Coordinable r.left r.right ∧ r.moved.Coordinand)
• r.Factor 2 = (r.same = true)

@[instance_reducible]

instance Fortuny2024.instDecidableFactor (r : Row) (i : Fin 3) : Decidable (r.Factor i)

Equations

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

def Fortuny2024.IllFormed (r : Row) : Prop

Equations

• Fortuny2024.IllFormed r = ∃ (i : Fin 3), r.Factor i

@[instance_reducible]

instance Fortuny2024.instDecidablePredRowIllFormed : DecidablePred IllFormed

Equations

• Fortuny2024.instDecidablePredRowIllFormed r = { decide := decide (∃ k < 3, ∀ (h : k < 3), r.Factor ⟨k, h⟩), reflects_decide := ⋯ }

def Fortuny2024.categoryTable : List (String × Category)

Equations

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

def Fortuny2024.movedTable : List (String × Moved)

Equations

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

def Fortuny2024.sameTable : List (String × Bool)

Equations

• Fortuny2024.sameTable = [("yes", true), ("no", false)]

def Fortuny2024.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem Fortuny2024.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def Fortuny2024.rows : List Row

Equations

• Fortuny2024.rows = List.filterMap Fortuny2024.Row.ofDatum Fortuny2024.Examples.all

theorem Fortuny2024.rows_predicted (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ ¬IllFormed r)

The paper's judgments are those of the three-factor decomposition, a coordination being ungrammatical exactly when one of the factors applies.

theorem Fortuny2024.rows_factor (r : Row) : r ∈ rows → ∀ (i j : Fin 3), r.Factor i → r.Factor j → i = j

Each ill-formed coordination in the data falls under exactly one factor (§2.3). Only the coordinator's definition rules out extraction of a single coordinand, only the Integrity Condition extraction of identical coordinands, and only the Prohibition against Self-Coordination the across-the-board dependency with coordinated positions.