Ross (1967): Constraints on Variables in Syntax

This file formalizes the dissertation's constraints on the variables of reordering transformations, stated over the positions a moved constituent leaves behind in a constituent-structure tree: the Complex NP Constraint, that nothing is moved out of a sentence dominated by a noun phrase with a lexical head noun (CNPC); the Coordinate Structure Constraint, that no conjunct is moved and nothing is moved out of a conjunct (CSC); the Left Branch Condition, that no noun phrase on the left branch of a larger noun phrase is moved out of it (LBC); and the Sentential Subject Constraint, that nothing is moved out of a sentence in subject position (SSC). A movement is a source position and a landing position in a tree, and a constraint is violated when the positions the movement crosses, the ancestors of the source that do not dominate the landing site, contain the configuration the constraint names. The dissertation's examples are rows whose trees and movements are built here, and chopping_rows reads their judgments as the constraints predict, the acceptable ones being exactly those that violate none; copying_rows is the dissertation's other generalization, that a copying rule such as Left Dislocation, which leaves a pronoun behind, crosses every one of these islands freely.

Implementation notes

Trees carry the categories of PhraseStructure.Cat, which have no levels: a noun phrase is a node of category N, a coordinate structure a node of category Conj headed by its conjunction word, whose other daughters are the conjuncts, and a noun phrase has a lexical head noun when its head daughter is a noun. The trees are the dissertation's diagrams reduced to the categories the constraints mention, with the moved constituent in its source position; questions and topicalizations land at the root and relativizations at the relative clause. Dominance in the Sentential Subject Constraint is read as immediate, the configuration of a sentence exhaustively dominated by a subject NP, so that the constraint does not reach a clause inside a relative clause on a subject. The A-over-A principle, the pied-piping convention, upward boundedness, and the definition of islands as the domains of chopping rules are not formalized.

References

• [Ros67]

Trees and movements

def Ross1967.w (pos : UD.UPOS) (form : String) : PhraseStructure.Tree PhraseStructure.Cat String

A word of a part of speech.

Equations

• Ross1967.w pos form = PhraseStructure.Tree.terminal (PhraseStructure.Cat.lex pos) form

structure Ross1967.Movement : Type

A movement in a tree records the position of the moved constituent and the position it lands at.

• tree : PhraseStructure.Tree PhraseStructure.Cat String
• source : List ℕ
• landing : List ℕ

def Ross1967.Movement.at? (m : Movement) (p : List ℕ) : Option (PhraseStructure.Tree PhraseStructure.Cat String)

The subtree at a position.

Equations

• m.at? p = RoseTree.subtreeAt m.tree p

def Ross1967.Movement.cat? (m : Movement) (p : List ℕ) : Option PhraseStructure.Cat

The category at a position.

Equations

• m.cat? p = Option.map PhraseStructure.Tree.cat (m.at? p)

def Ross1967.Movement.crossed (m : Movement) : List (List ℕ)

The positions the movement crosses are the strict ancestors of the source that do not dominate the landing site, the constituents the moved element is moved out of.

Equations

• m.crossed = List.filter (fun (p : List ℕ) => decide (p ≠ m.source ∧ ¬p <+: m.landing)) m.source.inits

def Ross1967.Movement.LexicalNP (t : PhraseStructure.Tree PhraseStructure.Cat String) : Prop

A noun phrase has a lexical head noun when its head daughter is a noun, a word.

Equations

• Ross1967.Movement.LexicalNP t = (t.cat = PhraseStructure.Cat.N ∧ ∃ d ∈ t.headIndex?.bind fun (x : ℕ) => (RoseTree.children t)[x]?, d.children = [])

@[instance_reducible]

instance Ross1967.Movement.instDecidableLexicalNP (t : PhraseStructure.Tree PhraseStructure.Cat String) : Decidable (LexicalNP t)

Equations

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

def Ross1967.Movement.IsConjunct (m : Movement) (p : List ℕ) : Prop

A conjunct is a daughter of a coordinate structure other than its head, the conjunction.

Equations

• m.IsConjunct p = (m.cat? p.dropLast = some PhraseStructure.Cat.Conj ∧ ¬m.tree.HeadDaughterAt { toList := p.dropLast } { toList := p })

@[instance_reducible]

instance Ross1967.Movement.instDecidableIsConjunct (m : Movement) (p : List ℕ) : Decidable (m.IsConjunct p)

Equations

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

def Ross1967.Movement.CNPC (m : Movement) : Prop

The Complex NP Constraint is violated when the movement leaves a sentence and the noun phrase with a lexical head noun immediately dominating it.

Equations

• m.CNPC = ∃ s ∈ m.crossed, m.cat? s = some PhraseStructure.Cat.S ∧ s.dropLast ∈ m.crossed ∧ ∃ t ∈ m.at? s.dropLast, Ross1967.Movement.LexicalNP t

def Ross1967.Movement.CSC (m : Movement) : Prop

The Coordinate Structure Constraint is violated when the moved element is a conjunct leaving its coordinate structure, or the movement leaves a conjunct.

Equations

• m.CSC = (m.IsConjunct m.source ∧ m.source.dropLast ∈ m.crossed ∨ ∃ c ∈ m.crossed, m.IsConjunct c)

def Ross1967.Movement.SSC (m : Movement) : Prop

The Sentential Subject Constraint is violated when the movement leaves a sentence immediately dominated by a noun phrase that is itself immediately dominated by a sentence.

Equations

• m.SSC = ∃ s ∈ m.crossed, m.cat? s = some PhraseStructure.Cat.S ∧ m.cat? s.dropLast = some PhraseStructure.Cat.N ∧ m.cat? s.dropLast.dropLast = some PhraseStructure.Cat.S

def Ross1967.Movement.LBC (m : Movement) : Prop

The Left Branch Condition is violated when the moved element is a noun phrase that is the leftmost daughter of a noun phrase the movement leaves.

Equations

• m.LBC = (m.cat? m.source = some PhraseStructure.Cat.N ∧ m.source.getLast? = some 0 ∧ m.cat? m.source.dropLast = some PhraseStructure.Cat.N ∧ m.source.dropLast ∈ m.crossed)

@[instance_reducible]

instance Ross1967.Movement.instDecidableCNPC (m : Movement) : Decidable m.CNPC

Equations

• m.instDecidableCNPC = id inferInstance

@[instance_reducible]

instance Ross1967.Movement.instDecidableCSC (m : Movement) : Decidable m.CSC

Equations

• m.instDecidableCSC = id inferInstance

@[instance_reducible]

instance Ross1967.Movement.instDecidableSSC (m : Movement) : Decidable m.SSC

Equations

• m.instDecidableSSC = id inferInstance

@[instance_reducible]

instance Ross1967.Movement.instDecidableLBC (m : Movement) : Decidable m.LBC

Equations

• m.instDecidableLBC = id inferInstance

def Ross1967.Movement.Violates (m : Movement) : Prop

The movement violates one of the four constraints.

Equations

• m.Violates = (m.CNPC ∨ m.CSC ∨ m.SSC ∨ m.LBC)

@[instance_reducible]

instance Ross1967.Movement.instDecidableViolates (m : Movement) : Decidable m.Violates

Equations

• m.instDecidableViolates = { decide := decide m.CNPC || decide (m.CSC ∨ m.SSC ∨ m.LBC), reflects_decide := ⋯ }

The dissertation's examples

def Ross1967.phineas : PhraseStructure.Tree PhraseStructure.Cat String

In Who does Phineas know a girl who is jealous of? the questioned NP is inside the relative clause on girl.

Equations

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

def Ross1967.hatClaim : PhraseStructure.Tree PhraseStructure.Cat String

The relative clause of the hat which I believed the claim that Otto was wearing.

Equations

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

def Ross1967.hatThat : PhraseStructure.Tree PhraseStructure.Cat String

The relative clause of the hat which I believed that Otto was wearing.

Equations

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

def Ross1967.sofa : PhraseStructure.Tree PhraseStructure.Cat String

In What sofa will he put the chair between some table and? the questioned NP is a conjunct.

Equations

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

def Ross1967.lute : PhraseStructure.Tree PhraseStructure.Cat String

The lute which Henry plays and sings madrigals relativizes out of a conjoined VP.

Equations

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

def Ross1967.trombone : PhraseStructure.Tree PhraseStructure.Cat String

Which trombone did the nurse polish and the plumber computed my tax? questions out of a conjoined sentence.

Equations

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

def Ross1967.guardian : PhraseStructure.Tree PhraseStructure.Cat String

In The boy whose guardian's employer we elected president the possessor NPs are nested on left branches.

Equations

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

def Ross1967.battleax : PhraseStructure.Tree PhraseStructure.Cat String

The predicate of the teacher sentences.

Equations

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

def Ross1967.fireClause : PhraseStructure.Tree PhraseStructure.Cat String

that the principal would fire who.

Equations

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

def Ross1967.teacherActive : PhraseStructure.Tree PhraseStructure.Cat String

The teacher who the reporters expected that the principal would fire.

Equations

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

def Ross1967.teacherPassive : PhraseStructure.Tree PhraseStructure.Cat String

In The teacher who that the principal would fire was expected by the reporters the that-clause is a sentential subject.

Equations

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

def Ross1967.teacherExtraposed : PhraseStructure.Tree PhraseStructure.Cat String

In The teacher who it was expected by the reporters that the principal would fire the that-clause is extraposed.

Equations

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

def Ross1967.hoods : PhraseStructure.Tree PhraseStructure.Cat String

Of which cars were the hoods damaged by the explosion? moves a subconstituent of a phrasal subject.

Equations

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

def Ross1967.father : PhraseStructure.Tree PhraseStructure.Cat String

In My father, the man he works with in Boston is going to tell the police … the dislocated NP is the subject of a relative clause.

Equations

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

def Ross1967.guitar : PhraseStructure.Tree PhraseStructure.Cat String

In This guitar, I've sung folksongs and accompanied myself on it all my life the dislocated NP is inside a conjunct.

Equations

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

def Ross1967.lived : PhraseStructure.Tree PhraseStructure.Cat String

In My father, that he's lived here all his life is well-known to the cops the dislocated NP is inside a sentential subject.

Equations

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

def Ross1967.handbag : PhraseStructure.Tree PhraseStructure.Cat String

In My wife, somebody stole her handbag last night the dislocated NP is a possessor on a left branch.

Equations

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

def Ross1967.movement : String → Option Movement

The movement of each example, by the dissertation's number. Questions and dislocations land at the root, relativizations at the relative clause.

Equations

• Ross1967.movement "(4.15a)" = some { tree := Ross1967.phineas, source := [1, 1, 2, 1, 1, 1, 1], landing := [] }
• Ross1967.movement "(4.18a)" = some { tree := Ross1967.hatClaim, source := [0, 2, 1, 1, 2, 2, 2], landing := [0, 2] }
• Ross1967.movement "(4.18b)" = some { tree := Ross1967.hatThat, source := [0, 2, 1, 1, 2, 2], landing := [0, 2] }
• Ross1967.movement "(2.18)" = some { tree := Ross1967.sofa, source := [1, 2, 1, 2], landing := [] }
• Ross1967.movement "(4.82a)" = some { tree := Ross1967.lute, source := [0, 2, 1, 0, 1], landing := [0, 2] }
• Ross1967.movement "(4.82d)" = some { tree := Ross1967.trombone, source := [0, 0, 1, 1], landing := [] }
• Ross1967.movement "(4.184a)" = some { tree := Ross1967.guardian, source := [0, 2, 1, 1], landing := [0, 2] }
• Ross1967.movement "(4.184b)" = some { tree := Ross1967.guardian, source := [0, 2, 1, 1, 0], landing := [0, 2] }
• Ross1967.movement "(4.184c)" = some { tree := Ross1967.guardian, source := [0, 2, 1, 1, 0, 0], landing := [0, 2] }
• Ross1967.movement "(4.251a)" = some { tree := Ross1967.teacherActive, source := [0, 2, 1, 1, 2, 2], landing := [0, 2] }
• Ross1967.movement "(4.251b)" = some { tree := Ross1967.teacherPassive, source := [0, 2, 0, 0, 2, 2], landing := [0, 2] }
• Ross1967.movement "(4.251c)" = some { tree := Ross1967.teacherExtraposed, source := [0, 2, 1, 3, 2, 2], landing := [0, 2] }
• Ross1967.movement "(4.252)" = some { tree := Ross1967.hoods, source := [0, 2], landing := [] }
• Ross1967.movement "(6.128b)" = some { tree := Ross1967.father, source := [0, 2, 0], landing := [] }
• Ross1967.movement "(6.135b)" = some { tree := Ross1967.guitar, source := [1, 1, 2, 2, 1], landing := [] }
• Ross1967.movement "(6.136)" = some { tree := Ross1967.lived, source := [0, 0, 1], landing := [] }
• Ross1967.movement "(6.137)" = some { tree := Ross1967.handbag, source := [1, 1, 0], landing := [] }
• Ross1967.movement x✝ = none

The rows

inductive Ross1967.Rule : Type

Whether a reordering rule chops its term, substituting nothing or another term for it, or copies it, leaving a pronoun in its place.

• chopping : Rule
• copying : Rule

@[instance_reducible]

instance Ross1967.instDecidableEqRule : DecidableEq Rule

Equations

• Ross1967.instDecidableEqRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ross1967.instReprRule : Repr Rule

Equations

• Ross1967.instReprRule = { reprPrec := Ross1967.instReprRule.repr }

def Ross1967.instReprRule.repr : Rule → ℕ → Std.Format

Equations

• Ross1967.instReprRule.repr Ross1967.Rule.chopping prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ross1967.Rule.chopping")).group prec✝
• Ross1967.instReprRule.repr Ross1967.Rule.copying prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ross1967.Rule.copying")).group prec✝

inductive Ross1967.Constraint : Type

The four constraints.

• cnpc : Constraint
• csc : Constraint
• ssc : Constraint
• lbc : Constraint

@[instance_reducible]

instance Ross1967.instDecidableEqConstraint : DecidableEq Constraint

Equations

• Ross1967.instDecidableEqConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ross1967.instReprConstraint.repr : Constraint → ℕ → Std.Format

Equations

• Ross1967.instReprConstraint.repr Ross1967.Constraint.cnpc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ross1967.Constraint.cnpc")).group prec✝
• Ross1967.instReprConstraint.repr Ross1967.Constraint.csc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ross1967.Constraint.csc")).group prec✝
• Ross1967.instReprConstraint.repr Ross1967.Constraint.ssc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ross1967.Constraint.ssc")).group prec✝
• Ross1967.instReprConstraint.repr Ross1967.Constraint.lbc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ross1967.Constraint.lbc")).group prec✝

@[instance_reducible]

instance Ross1967.instReprConstraint : Repr Constraint

Equations

• Ross1967.instReprConstraint = { reprPrec := Ross1967.instReprConstraint.repr }

def Ross1967.Constraint.Fires : Constraint → Movement → Prop

The constraint's condition on a movement.

Equations

• Ross1967.Constraint.cnpc.Fires x✝ = x✝.CNPC
• Ross1967.Constraint.csc.Fires x✝ = x✝.CSC
• Ross1967.Constraint.ssc.Fires x✝ = x✝.SSC
• Ross1967.Constraint.lbc.Fires x✝ = x✝.LBC

@[instance_reducible]

instance Ross1967.instDecidableFires (c : Constraint) (m : Movement) : Decidable (c.Fires m)

Equations

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

structure Ross1967.Row : Type

An example records its movement, the kind of rule that moved it, the constraint the dissertation holds responsible, if any, and its judgment.

• movement : Movement
• rule : Rule
• constraint : Option Constraint
• judgment : Judgment

def Ross1967.Row.ofDatum (r : Datum) : Option Row

The row of an example.

Equations

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

def Ross1967.data : List Row

The examples.

Equations

• Ross1967.data = List.filterMap Ross1967.Row.ofDatum Ross1967.Examples.all

theorem Ross1967.data_length : data.length = Examples.all.length

Every row has its movement.

theorem Ross1967.chopping_rows (d : Row) : d ∈ data → d.rule = Rule.chopping → (d.judgment = Judgment.acceptable ↔ ¬d.movement.Violates)

Under the constraints on chopping rules, a question or relativization is acceptable exactly when it violates none of the four.

theorem Ross1967.attributions (d : Row) : d ∈ data → ∀ c ∈ d.constraint, c.Fires d.movement

The constraint the dissertation names for a starred example, or for a dislocation, is one its movement violates.

theorem Ross1967.copying_rows (d : Row) : d ∈ data → d.rule = Rule.copying → d.judgment = Judgment.acceptable ∧ d.movement.Violates

Copying rules are not subject to the constraints, since each Left Dislocation crosses one of the four islands and is acceptable.

theorem Ross1967.ssc_cnpc_independent : (∃ d ∈ data, d.movement.SSC ∧ ¬d.movement.CNPC) ∧ ∃ d ∈ data, d.movement.CNPC ∧ ¬d.movement.SSC

The Sentential Subject Constraint is not the Complex NP Constraint, since the sentential subject has no lexical head noun, and the noun complement clause is not a subject.