The Calculus of Control

[Lan04a]'s calculus, as codified in [Lan13] ((137)/(178)): each clausal head — I and C — carries a ⟨T, Agr⟩ feature specification, and a head both of whose features are positive assigns [+R], licensing an independent referential subject. Control is the elsewhere case. Mutual cancellation ([Lan13] fn. 6): when C is [+T, +Agr] as well as I, R-assignment cancels and OC re-emerges — the Hebrew subjunctive effect, inexpressible on a flat tense scale. [Lan04a]'s scale of finiteness (ClauseClass) abbreviates clauses so specified, and ClauseClass.HasOC is derived from the calculus via ClauseClass.toClause.

Main definitions

• Control.Head, Control.Clause
• Control.Clause.HasControl: control as the elsewhere condition
• Control.ClauseClass: the scale of finiteness, with derived ClauseClass.HasOC

structure Control.Head : Type

A clausal head as the calculus sees it: its ⟨T, Agr⟩ feature specification ([Lan04a]; [Lan13] (137)).

• tense : Bool

  Semantic tense, [±T].

• agr : Bool

  Agreement, [±Agr].

def Control.instDecidableEqHead.decEq (x✝ x✝¹ : Head) : Decidable (x✝ = x✝¹)

Equations

• Control.instDecidableEqHead.decEq { tense := a, agr := a_1 } { tense := b, agr := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Control.instDecidableEqHead : DecidableEq Head

Equations

• Control.instDecidableEqHead = Control.instDecidableEqHead.decEq

def Control.instReprHead.repr : Head → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Control.instReprHead : Repr Head

Equations

• Control.instReprHead = { reprPrec := Control.instReprHead.repr }

def Control.Head.RAssigning (h : Head) : Prop

A head is R-assigning when both features are positive: it licenses an independent referential subject ([Lan13] (137a)).

Equations

• h.RAssigning = (h.tense = true ∧ h.agr = true)

@[instance_reducible]

instance Control.instDecidableRAssigning (h : Head) : Decidable h.RAssigning

Equations

• Control.instDecidableRAssigning h = Control.instDecidableRAssigning._aux_1 h

structure Control.Clause : Type

A clause as the calculus sees it: its inflectional and complementizer heads.

• i : Head

  The inflectional head.

• c : Head

  The complementizer head.

@[instance_reducible]

instance Control.instDecidableEqClause : DecidableEq Clause

Equations

• Control.instDecidableEqClause = Control.instDecidableEqClause.decEq

def Control.instDecidableEqClause.decEq (x✝ x✝¹ : Clause) : Decidable (x✝ = x✝¹)

Equations

• Control.instDecidableEqClause.decEq { i := a, c := a_1 } { i := b, c := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Control.instReprClause : Repr Clause

Equations

• Control.instReprClause = { reprPrec := Control.instReprClause.repr }

def Control.instReprClause.repr : Clause → Nat → Std.Format

Equations

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

def Control.Clause.HasControl (cl : Clause) : Prop

Control is the elsewhere case ([Lan13] (178) with fn. 6): an R-assigning I destroys control unless C is R-assigning too — mutual cancellation.

Equations

• cl.HasControl = (cl.i.RAssigning → cl.c.RAssigning)

@[instance_reducible]

instance Control.instDecidableHasControl (cl : Clause) : Decidable cl.HasControl

Equations

• Control.instDecidableHasControl cl = Control.instDecidableHasControl._aux_1 cl

theorem Control.Clause.hasControl_of_c_rAssigning {cl : Clause} (h : cl.c.RAssigning) : cl.HasControl

Mutual cancellation: a fully specified C restores OC in a fully finite clause — Hebrew subjunctives ([Lan13] fn. 6).

Clause classes

inductive Control.ClauseClass : Type

[Lan04a]'s scale positions, in [Ost26]'s terminology: C-subjunctives are [−T] complements (OC whatever the Agr value), F-subjunctives [+T] complements (OC unless [+Agr], per the OC-NC generalization), and finite the fully finite remainder. The positions are tense cells, not mood or finiteness categories — [−T] covers bare infinitives and untensed subjunctives alike, and OC occurs in inflected complements. [Lan15] subsumes the [±T] split under attitude/nonattitude (the tier reading lives with Studies/Landau2015.lean).

• cSubjunctive : ClauseClass

  [−T] complement: OC at any Agr value

• fSubjunctive : ClauseClass

  [+T] complement: OC unless [+Agr]

• finite : ClauseClass

  Fully finite: [+T, +Agr] on I. No control unless C is fully specified too (mutual cancellation, Clause.hasControl_of_c_rAssigning)

@[instance_reducible]

instance Control.instDecidableEqClauseClass : DecidableEq ClauseClass

Equations

• Control.instDecidableEqClauseClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Control.instReprClauseClass : Repr ClauseClass

Equations

• Control.instReprClauseClass = { reprPrec := Control.instReprClauseClass.repr }

def Control.instReprClauseClass.repr : ClauseClass → Nat → Std.Format

Equations

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

def Control.ClauseClass.ofFiniteness (unrestrictedTAM independentTense : Bool) : ClauseClass

The scale position determined by the two clause-typology observables of [Ost26]-style fragments: unrestricted TAM marks a fully finite clause; among the TAM-restricted clauses, independent tense separates [+T] from [−T] ([Lan04a]'s feature, diagnosed by temporal mismatch). Per-language scale maps derive from this single classifier rather than restating the case table.

Equations

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

def Control.ClauseClass.toClause (c : ClauseClass) (agr : Bool) : Clause

The clause a scale position abbreviates, at a given Agr value: [±T] on I per the position, C unspecified. The scale cannot express a fully specified C — mutual cancellation needs the calculus directly.

Equations

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

def Control.ClauseClass.HasOC (c : ClauseClass) (agr : Bool) : Prop

OC is realized in a clause class iff the calculus leaves control at the clause it abbreviates: the elsewhere condition on toClause.

Equations

• c.HasOC agr = (c.toClause agr).HasControl

@[instance_reducible]

instance Control.instDecidableHasOC (c : ClauseClass) (agr : Bool) : Decidable (c.HasOC agr)

Equations

• Control.instDecidableHasOC c agr = Control.instDecidableHasOC._aux_1 c agr

theorem Control.ClauseClass.hasOC_iff (c : ClauseClass) (agr : Bool) : c.HasOC agr ↔ c = cSubjunctive ∨ c = fSubjunctive ∧ agr = false

OC obtains exactly on C-subjunctives (any Agr) and [−Agr] F-subjunctives.