Landau (2013): Control in Generative Grammar: A Research Companion

This file formalizes the signature of obligatory control of [Lan13]: the controller must be a co-dependent of the clause, and the controlled element, or part of it, is interpreted as a bound variable. The familiar criteria follow from the two clauses: co-dependence excludes arbitrary, long-distance, and non-c-commanding control and forces the sloppy reading under ellipsis, and variable binding excludes the strict reading under only. The Control.Excludes instance records this derivation, so that the library's Control.admits returns the book's characterizations: a profile satisfying both clauses admits no criterial configuration and one satisfying neither admits them all. ofNoncoreferential reads such a profile off whether a clause type licenses a noncoreferential subject — a free reading of the controlled position, refuting co-dependence — which the studies of overt controlled subjects consume.

Implementation notes

The signature is the book's (74), in the section on the obligatory-control signature of the first chapter, and the derivation of the criteria from it runs through (75)–(79). Obligatory de se is not criterial for obligatory control, being a property of the attitude tier, and the lexical-subject diagnostic is a criterion of obligatory nullness rather than of obligatory control, the separation the overt-subject studies turn on; the positive human-reference clause of the non-obligatory signature is not modelled.

References

• [Lan13]

inductive Landau2013.Clause74 : Type

The two clauses of the signature of obligatory control: the co-dependence clause admits implicit, split, and, through "part of it", partial control.

• codependent : Clause74

  The controller or controllers must be co-dependents of the clause.

• boundVariable : Clause74

  The controlled element is interpreted as a bound variable.

@[instance_reducible]

instance Landau2013.instDecidableEqClause74 : DecidableEq Clause74

Equations

• Landau2013.instDecidableEqClause74 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Landau2013.instReprClause74.repr : Clause74 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Landau2013.instReprClause74 : Repr Clause74

Equations

• Landau2013.instReprClause74 = { reprPrec := Landau2013.instReprClause74.repr }

@[instance_reducible]

instance Landau2013.instFintypeClause74 : Fintype Clause74

Equations

• Landau2013.instFintypeClause74 = { elems := { val := ↑Landau2013.Clause74.enumList, nodup := Landau2013.Clause74.enumList_nodup }, complete := Landau2013.instFintypeClause74._proof_1 }

@[instance_reducible]

instance Landau2013.instExcludesClause74 : Control.Excludes Clause74

The derivation of the criteria from the signature: co-dependence excludes the three antecedence configurations and the strict ellipsis reading, variable binding the strict reading under only.

Equations

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

def Landau2013.ofNoncoreferential (noncoreferential : Bool) : Set Clause74

The profile determined by whether a clause type licenses noncoreferential subjects: free reference attests a free reading of the controlled position, refuting co-dependence; obligatory coreference attests nothing.

Equations

• Landau2013.ofNoncoreferential noncoreferential = Control.ofAttested {d : Control.Diagnostic | noncoreferential = true ∧ d = Control.Diagnostic.arbitraryControl}

@[simp]

theorem Landau2013.ofNoncoreferential_eq_univ_iff {b : Bool} : ofNoncoreferential b = Set.univ ↔ b = false