Chomsky (1981): the binding theory

This file formalizes the binding theory of Government and Binding as an instance of the framework-neutral conditions of Syntax/Binding. A noun phrase binds another when the two are coindexed and the first c-commands the second; an anaphor is bound in its governing category (Principle A), a pronominal is free there (Principle B), and an R-expression is free (Principle C). The positions are the noun phrases of a phrase-structure tree, the command relation is Reinhart's c-command, the binding domain of a noun phrase is the minimal clause containing it (PhraseStructure.Tree.clauseConfiguration), the dependency is coindexation, and no anaphor is exempt. An indexing is licit when coindexed noun phrases agree in φ-features and it satisfies the three principles, and a tree is grammatical when some indexing is licit.

Since nothing is exempt, an anaphor that nothing in its clause c-commands is out under every indexing, which excludes an anaphoric subject. For two noun phrases coindexed with each other alone, Principle C is Reinhart's restriction (10b) read with c-command. The textbook paradigm checks the instance: a reflexive object must corefer with its subject and agree with it, a pronominal object cannot corefer with it, locality separates the two in an embedded clause, and an R-expression cannot corefer with a c-commanding pronoun at any distance.

Main definitions

• Chomsky1981.configuration: c-command and the minimal clause on the noun phrases of a tree.
• Chomsky1981.Licit, Grammatical, CanCorefer, MustCorefer.

Main results

• Chomsky1981.not_grammatical_of_not_locallyCommanded: an anaphor with nothing in its clause c-commanding it rules the tree out.
• Chomsky1981.permits_iff: Principle C for a coindexed pair is Reinhart's restriction (10b).

Implementation notes

A one-word noun phrase is a terminal of category NP, and the positions are those terminals. The governing category is approximated by the minimal clause: the governor and the accessible subject that refine it are not modelled, nor are noun phrases with subjects. Indexings range over maps from the noun phrases to themselves, which realize every partition of them.

TODO

The paradigm is the textbook one; check each sentence against Chapter 3 of the book, which was not available, and move the verified ones to Data/Examples.

References

• N. Chomsky, Lectures on government and binding (1981)
• T. Reinhart, The syntactic domain of anaphora (1976)

Clauses and their noun phrases

def Chomsky1981.np (w : Morphology.Word) : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word

np w is the one-word noun phrase w.

Equations

• Chomsky1981.np w = PhraseStructure.Tree.terminal PhraseStructure.Cat.N w

def Chomsky1981.clause (subj v : Morphology.Word) (comp : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word

clause subj v comp is the clause with subject subj, verb v and complement comp.

Equations

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

def Chomsky1981.nominals (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) : List (Core.Order.TreePath × Morphology.Word)

nominals t lists the noun phrases of t, each with its position.

Equations

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

@[reducible, inline]

abbrev Chomsky1981.Nominal (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) : Type

Nominal t is the type of noun phrases of t.

Equations

• Chomsky1981.Nominal t = { x : Core.Order.TreePath × Morphology.Word // x ∈ Chomsky1981.nominals t }

The binding configuration

@[reducible, inline]

abbrev Chomsky1981.configuration (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) : Binding.Configuration (Nominal t)

The configuration on the noun phrases of t is the clause configuration of t restricted to them.

Equations

• Chomsky1981.configuration t = Binding.Configuration.comap (fun (x : Chomsky1981.Nominal t) => (↑x).1) t.clauseConfiguration

def Chomsky1981.classOf {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} (x : Nominal t) : Option Binding.BindingClass

The binding class of a noun phrase is the binding class of its word.

Equations

• Chomsky1981.classOf x = Binding.bindingClassOf (↑x).2

def Chomsky1981.Licit (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) {κ : Type u_1} (idx : Nominal t → κ) : Prop

An indexing is licit when coindexed noun phrases agree and coindexation satisfies the three principles, with no anaphor exempt.

Equations

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

@[instance_reducible]

instance Chomsky1981.instDecidableLicitOfDecidableEq {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} {κ : Type u_1} [DecidableEq κ] (idx : Nominal t → κ) : Decidable (Licit t idx)

Equations

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

def Chomsky1981.Grammatical (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) : Prop

A tree is grammatical when some indexing of its noun phrases is licit.

Equations

• Chomsky1981.Grammatical t = ∃ (idx : Chomsky1981.Nominal t → Chomsky1981.Nominal t), Chomsky1981.Licit t idx

def Chomsky1981.CanCorefer (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) (p q : Core.Order.TreePath) : Prop

The noun phrases at p and q can corefer when some licit indexing coindexes them.

Equations

• Chomsky1981.CanCorefer t p q = ∃ (idx : Chomsky1981.Nominal t → Chomsky1981.Nominal t), Chomsky1981.Licit t idx ∧ ∀ (a b : Chomsky1981.Nominal t), (↑a).1 = p → (↑b).1 = q → idx a = idx b

def Chomsky1981.MustCorefer (t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word) (p q : Core.Order.TreePath) : Prop

The noun phrases at p and q must corefer when every licit indexing coindexes them.

Equations

• Chomsky1981.MustCorefer t p q = ∀ (idx : Chomsky1981.Nominal t → Chomsky1981.Nominal t), Chomsky1981.Licit t idx → ∀ (a b : Chomsky1981.Nominal t), (↑a).1 = p → (↑b).1 = q → idx a = idx b

@[instance_reducible]

instance Chomsky1981.instDecidableGrammatical {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} : Decidable (Grammatical t)

Equations

• Chomsky1981.instDecidableGrammatical = { decide := decide (∃ a ∈ Finset.univ, Chomsky1981.Licit t a), reflects_decide := ⋯ }

@[instance_reducible]

instance Chomsky1981.instDecidableCanCorefer {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} (p q : Core.Order.TreePath) : Decidable (CanCorefer t p q)

Equations

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

@[instance_reducible]

instance Chomsky1981.instDecidableMustCorefer {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} (p q : Core.Order.TreePath) : Decidable (MustCorefer t p q)

Equations

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

Principle A without exemption

theorem Chomsky1981.not_grammatical_of_not_locallyCommanded {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} {b : Nominal t} {c : Binding.BindingClass} (hb : classOf b = some c) (hc : c.IsAnaphor) (hl : ¬(configuration t).LocallyCommanded b) : ¬Grammatical t

An anaphor that nothing in its clause c-commands violates Principle A under every indexing, so the tree is out.

Principle C and Reinhart's restriction

theorem Chomsky1981.permits_iff {t : PhraseStructure.Tree PhraseStructure.Cat Morphology.Word} {a b : Nominal t} (hab : a ≠ b) (pron : List Core.Order.TreePath) : Reinhart1976.Permits (RoseTree.CCommands t) pron (↑a).1 (↑b).1 ↔ ((↑b).1 ∉ pron → ¬(configuration t).Bound (Binding.pair a b) b) ∧ ((↑a).1 ∉ pron → ¬(configuration t).Bound (Binding.pair a b) a)

For two noun phrases coindexed with each other alone, Principle C is Reinhart's restriction (10b) read with c-command, the R-expressions being the noun phrases outside pron.

The paradigm