Allotey (2021): overt pronouns of infinitival predicates of Gã

This file formalizes [All21]. Obligatory control into Gã irrealis ni-clauses requires an overt subject proclitic: null PRO is ungrammatical, a lexical subject is ungrammatical, and the proclitic shows the whole OC signature (Table 2). The controlled clause is non-finite and irrealis rather than subjunctive — it bars tense and aspect, focus fronting and free reference, licenses NPIs across its boundary, negates preverbally, and carries the irrealis marker only as a high tone on its subject (Table 4). The pronoun is overt because that tone needs a segmental host. The subject markers are pronouns, not agreement: the verb is invariant across subjects (§4.4) and a marker cannot double a lexical subject (§6.1), against the affixal analysis of [Cam17]; Gã is therefore a non-pro-drop language (§2.1). [DH13b]'s 101A coding of Gã, made from [AO68], is affixal too.

Everything is read off the paper's example rows and the Fragment. The control profile of a clause type is [Lan13]'s signature as the rows attest it (Control.ofAttested): no row attests a criterial configuration of the ni-clause, so it is obligatory control, while the finite akɛ-clause attests free reference. Complementizer selection is Verb.Takes over the Fragment's frames; every finiteness diagnostic is a row theorem conditioned on the complementizer's finiteness alone, the paper's convergence argument; Table 4 is the exponents the rows show in each irrealis context, and the tone-hosting requirement then derives the overt pronoun from the minimal-pronoun inventory.

Implementation notes

The paper's pro-drop status is its own reading of its 101A cell, obligatory subject pronouns (§4.2), and is stated here rather than in the Fragment because [DH13b] codes the same markers as affixes; wals_codes_affixes records the discrepancy and no_agreement_rows the paper's evidence against it. The bound-variable row of Table 2 rests on the de se example (53); the paper has no only test, so Control.Diagnostic.strictUnderOnly is never attested and the bound-variable clause of the signature holds unrefuted rather than tested. The paper tests reference only in the ni- and akɛ-clauses, so the comparison with [Lan04a]'s scale is stated for those two.

References

• [All21]
• [AO68]
• [Cam17]
• [Lan13]
• [Lan04a]
• [Sza09]
• [Hor99]
• [Sat19]
• [Kar71a]
• [Noo07]
• [Riz97]
• [DH13b]
• [WL23]
• [Wur24]

Pronouns (Table 3)

theorem Allotey2021.objective_form_iff (p : Person) (n : Number) : (∃ q ∈ Ga.Pronouns.pronouns, q.person = some p ∧ q.number = some n ∧ q.case_ = some Case.acc) ↔ n = Number.singular ∧ (p = Person.second ∨ p = Person.third)

Only second and third person singular have a dedicated objective form.

theorem Allotey2021.card_paradigm (c : Person.Category) : (Ga.Pronouns.paradigm c).card = if c = Person.Category.addressee ∨ c = Person.Category.other then 2 else 1

The paradigm distinguishes case in the second and third person singular alone: every other referential category has one form for all three columns of Table 3.

theorem Allotey2021.paradigm_nonempty (c : Person.Category) : (Ga.Pronouns.paradigm c).Nonempty

Every referential category has a form: the one form of first person plural wɔ covers clusivity and the number of others alike.

theorem Allotey2021.card_subjectForms (q : PersonalPronoun) : q ∈ Ga.Pronouns.pronouns → ∀ p ∈ q.person, ∀ n ∈ q.number, (Ga.Pronouns.subjectForms p n).card = 1

Each cell of Table 3 has one subject form.

Subject pronouns are not agreement (§4.4, §6.1)

theorem Allotey2021.no_agreement_rows : (∀ row ∈ Examples.all, row.feature? "diagnostic" = some "agreement" → (row.feature? "person").isSome = true → ("tee", "went") ∈ row.glossedTokens) ∧ ∃ r₁ ∈ Examples.all, ∃ r₂ ∈ Examples.all, r₁.feature? "diagnostic" = some "agreement" ∧ r₂.feature? "diagnostic" = some "agreement" ∧ r₁.feature? "person" ≠ r₂.feature? "person"

The verb of exx 79–81 is the one form tee 'went' whatever the person of its subject: Gã marks no subject agreement on the verb.

def Allotey2021.pronominalSubjects : Data.WALS.F101A.ExpressionOfPronominalSubjects

The paper's cell of [DH13b]'s 101A: subject pronouns are obligatory and object pronouns omissible (§4.2).

Equations

• Allotey2021.pronominalSubjects = Data.WALS.F101A.ExpressionOfPronominalSubjects.obligatoryPronounsInSubjectPosition

theorem Allotey2021.wals_codes_affixes : List.lookup "ga" Data.WALS.F101A.allData = some Data.WALS.F101A.ExpressionOfPronominalSubjects.subjectAffixesOnVerb

[DH13b] codes the same markers as subject affixes on the verb, not pronominalSubjects: the analysis of [Cam17] too, against which an affix would co-occur with a lexical subject (ex 123) and could not be separated from its verb by negation (ex 125). Gã's WALS code is ga; gaa is Gaagudju.

Complementizer selection (§5.5.1)

theorem Allotey2021.frame_takes_iff (c d : Ga.EmbeddedClauseType) : c.frame.Takes d.complementizer ↔ c = d

The three-way clause typology is the selection relation: each clause type's frame takes exactly its own complementizer.

theorem Allotey2021.takes_ni_iff_control (v : Verb) : v ∈ Ga.verbs → (v.Takes Ga.ni ↔ ∃ r ∈ v.readings, r.control.isSome = true)

A verb takes ni exactly when some frame of it is controlled.

theorem Allotey2021.proposition_iff_finite (v : Verb) : v ∈ Ga.verbs → ∀ r ∈ v.readings, ∀ s ∈ r.size, s = Clause.Size.proposition ↔ ∃ z ∈ Ga.complementizers, r.frame.Takes z ∧ z.IsFinite

[WL23]'s hierarchy at Gã's granularity: a proposition complement is exactly one whose frame takes a finite complementizer; situations and events share the infinitival ni-frame.

theorem Allotey2021.control_rows : (∃ v ∈ Ga.verbs, ∃ r ∈ v.readings, r.control = some ControlType.subjectControl) ∧ ∃ v ∈ Ga.verbs, ∃ r ∈ v.readings, r.control = some ControlType.objectControl

Subject and object control are both in the inventory (Table 2).

Rows

def Allotey2021.gaInventory : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form

Gã has no context-specific vocabulary item for minimal pronouns, so the elsewhere pronoun realizes every context.

Equations

• Allotey2021.gaInventory = { items := [], elsewhere := Binding.MinimalPronoun.Form.pronoun }

def Allotey2021.verbOf (row : Datum) : Option Verb

The Fragment entry for a row's matrix verb.

Equations

• Allotey2021.verbOf row = (row.feature? "verb").bind fun (x : String) => Verb.find? Ga.verbs x

def Allotey2021.clauseOf : String → Option Ga.EmbeddedClauseType

The clause type a complementizer feature names.

Equations

• Allotey2021.clauseOf "ni" = some Ga.EmbeddedClauseType.ni
• Allotey2021.clauseOf "ake" = some Ga.EmbeddedClauseType.ake
• Allotey2021.clauseOf "keji" = some Ga.EmbeddedClauseType.keji
• Allotey2021.clauseOf x✝ = none

def Allotey2021.clauseTypeOf (row : Datum) : Option Ga.EmbeddedClauseType

A row's clause type is its complement's, or the finite type for a matrix clause the paper labels finite.

Equations

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

def Allotey2021.reads (row : Datum) (r : String) (j : Judgment) : Prop

A row records reading r with judgment j.

Equations

• Allotey2021.reads row r j = ∃ x ∈ row.readings, x = (r, j)

@[instance_reducible]

instance Allotey2021.instDecidableReads (row : Datum) (r : String) (j : Judgment) : Decidable (reads row r j)

Equations

• Allotey2021.instDecidableReads row r j = Allotey2021.instDecidableReads._aux_1 row r j

def Allotey2021.formOf (row : Datum) : Option Binding.MinimalPronoun.Form

The realized form of a row's embedded subject.

Equations

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

theorem Allotey2021.controlled_subject_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" ∈ [none, some "nullSubject"] → ∀ f ∈ formOf row, row.judgment = Judgment.acceptable ↔ f = gaInventory.controlForm

In the rows whose only point is the shape of the controlled subject, the control frame is grammatical exactly with the inventory's control form (exx 2–3, 34–44, 54–59 vs 40–41).

theorem Allotey2021.lexical_subject_rows (row : Datum) : row ∈ Examples.all → row.feature? "embeddedSubject" = some "lexical" → row.feature? "clauseContext" = none → row.judgment = Judgment.ungrammatical

A lexical subject in the control frame is out (exx 42b–c, 64) — the copy the Movement Theory of Control ([Hor99]) would pronounce.

theorem Allotey2021.c_selection_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "cSelection" → ∀ v ∈ verbOf row, ∀ c ∈ clauseTypeOf row, row.judgment = Judgment.acceptable ↔ v.Takes c.complementizer

A complementizer is grammatical exactly when the verb takes it (exx 104–106).

theorem Allotey2021.tam_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ clauseTypeOf row, ∀ t ∈ row.feature? "embeddedTAM", t ≠ "none" → (row.judgment = Judgment.acceptable ↔ c.complementizer.IsFinite)

Overt tense or aspect in the complement is grammatical exactly in the finite clause types (exx 101, 111).

theorem Allotey2021.focus_npi_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ clauseTypeOf row, (row.feature? "diagnostic" = some "focus" → (row.judgment = Judgment.acceptable ↔ c.complementizer.IsFinite)) ∧ (row.feature? "diagnostic" = some "npi" → row.feature? "negation" = some "matrix" → (row.judgment = Judgment.acceptable ↔ ¬c.complementizer.IsFinite))

Focus fronting, [Riz97]'s strong-CP diagnostic, is available exactly in the finite clauses (exx 107–108); matrix negation licenses an embedded NPI exactly across the non-finite one (exx 116–117).

theorem Allotey2021.negation_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ clauseTypeOf row, ∀ p ∈ row.feature? "negationPosition", p = "preverbal" ↔ ¬c.complementizer.IsFinite

Negation precedes the verb exactly in the non-finite clause (exx 121–122, 124).

theorem Allotey2021.subject_tone_rows (row : Datum) : row ∈ Examples.all → row.judgment = Judgment.acceptable → ∀ c ∈ clauseTypeOf row, ∀ t ∈ row.feature? "subjectTone", (t = "high") = (c = Ga.EmbeddedClauseType.ni)

The embedded subject bears the irrealis high tone exactly in the ni-clause (exx 110–112, 118).

The irrealis marker

theorem Allotey2021.marker_rows (row : Datum) : row ∈ Examples.all → row.feature? "clauseContext" ∈ [none, some "control"] → ∀ m ∈ row.feature? "irrealisMarker", m = "present" ↔ (row.feature? "control").isSome = true

The marker appears on the subject of the control frame and nowhere else in the complement data (exx 34, 88–89, 92, 100–103, 106, 109, 112, 117–119, 122); it tracks the frame, not the verb — kai 'remember' takes it in its ni-frame (exx 43, 117a) and lacks it in its realis akɛ-frame (ex 89a).

theorem Allotey2021.implicative_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "implicative" → ∀ v ∈ verbOf row, row.feature? "irrealisMarker" = some "absent" ↔ v.implicative.positive = ↑Polarity.positive

In the paper's implicative contrast (ex 89) the marker is absent exactly under the verbs of the Fragment whose affirmed use entails the complement realized ([Kar71a]).

The OC signature (Table 2)

theorem Allotey2021.cCommand_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "cCommand" → (row.judgment = Judgment.acceptable ↔ row.feature? "antecedent" = some "cCommanding")

The antecedent must c-command the controlled pronoun (exx 45–46): grammatical exactly under the paper's c-commanding coindexation.

theorem Allotey2021.longDistance_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "longDistance" → (row.judgment = Judgment.acceptable ↔ row.feature? "antecedent" = some "local")

No long-distance antecedent (exx 47–49): grammatical exactly under the local coindexation.

theorem Allotey2021.sloppy_only : ∃ row ∈ Examples.all, row.feature? "diagnostic" = some "ellipsis" ∧ reads row "sloppy" Judgment.acceptable ∧ reads row "strict" Judgment.unacceptable

Under ellipsis the controlled pronoun has the sloppy reading only (ex 52).

theorem Allotey2021.free_reading_rows (row : Datum) : row ∈ Examples.all → ∀ c ∈ clauseTypeOf row, ∀ (j : Judgment), reads row "free" j → (j = Judgment.acceptable ↔ c.complementizer.IsFinite)

A free reading of the embedded subject is available exactly in the finite complement (exx 110–111 vs 92, 112).

theorem Allotey2021.deSe_witness : ∃ row ∈ Examples.all, row.feature? "diagnostic" = some "deSe" ∧ row.judgment = Judgment.unacceptable ∧ row.context ≠ ""

Ex 53 witnesses the de se row: infelicitous in its context.

theorem Allotey2021.controlled_form_covaries : Ga.Pronouns.subjectForms Person.second Number.singular ≠ Ga.Pronouns.subjectForms Person.second Number.plural

The controlled form φ-covaries with its controller (exx 37–39), unlike [Sat19]'s form-invariant Ewe yè.

def Allotey2021.attests (row : Datum) : Control.Diagnostic → Prop

An acceptable row attests one control diagnostic, a non-c-commanding or long-distance antecedent by the paper's coindexation, a free reading of the embedded subject, or a strict reading under ellipsis.

Equations

• Allotey2021.attests row Control.Diagnostic.nonCCommandingControl = (row.feature? "antecedent" = some "nonCCommanding" ∧ row.judgment = Judgment.acceptable)
• Allotey2021.attests row Control.Diagnostic.longDistanceControl = (row.feature? "antecedent" = some "longDistance" ∧ row.judgment = Judgment.acceptable)
• Allotey2021.attests row Control.Diagnostic.arbitraryControl = Allotey2021.reads row "free" Judgment.acceptable
• Allotey2021.attests row Control.Diagnostic.strictEllipsis = Allotey2021.reads row "strict" Judgment.acceptable
• Allotey2021.attests row Control.Diagnostic.strictUnderOnly = False

@[instance_reducible]

instance Allotey2021.instDecidablePredDiagnosticAttests (row : Datum) : DecidablePred (attests row)

Equations

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

def Allotey2021.attested (c : Ga.EmbeddedClauseType) : Set Control.Diagnostic

The diagnostics the rows attest for a clause type.

Equations

• Allotey2021.attested c = {d : Control.Diagnostic | ∃ row ∈ Allotey2021.Examples.all, Allotey2021.clauseTypeOf row = some c ∧ Allotey2021.attests row d}

@[instance_reducible]

instance Allotey2021.instDecidablePredDiagnosticMemSetAttested (c : Ga.EmbeddedClauseType) : DecidablePred fun (x : Control.Diagnostic) => x ∈ attested c

Equations

• Allotey2021.instDecidablePredDiagnosticMemSetAttested c d = id inferInstance

def Allotey2021.gaProfile (c : Ga.EmbeddedClauseType) : Set Landau2013.Clause74

The control profile of a clause type in [Lan13]'s signature: the clauses no attested diagnostic refutes.

Equations

• Allotey2021.gaProfile c = Control.ofAttested (Allotey2021.attested c)

theorem Allotey2021.attested_ni : attested Ga.EmbeddedClauseType.ni = ∅

No row attests a criterial configuration of the ni-clause.

theorem Allotey2021.ni_obligatory : gaProfile Ga.EmbeddedClauseType.ni = Set.univ

The ni-clause is obligatory control: every clause of the signature holds, so it admits no criterial configuration. [Sza09]'s long-distance Agree reaches the embedded subject across this weak CP.

theorem Allotey2021.admits_ni : Control.admits (gaProfile Ga.EmbeddedClauseType.ni) = ∅

theorem Allotey2021.arbitrary_mem_attested_ake : Control.Diagnostic.arbitraryControl ∈ attested Ga.EmbeddedClauseType.ake

The finite akɛ-clause attests a free reading (exx 110–111).

theorem Allotey2021.ake_not_obligatory : gaProfile Ga.EmbeddedClauseType.ake ≠ Set.univ

So it is not obligatory control.

Landau's scale

def Allotey2021.gaToLandau (c : Ga.EmbeddedClauseType) : Control.ClauseClass

Gã clause types on [Lan04a]'s finiteness scale — a scale position, not a mood claim. Unrestricted TAM and independent tense both coincide with the complementizer's finiteness (exx 109–111, 118–119).

Equations

• Allotey2021.gaToLandau c = Control.ClauseClass.ofFiniteness (decide c.complementizer.IsFinite) (decide c.complementizer.IsFinite)

theorem Allotey2021.ga_no_fSubjunctive (c : Ga.EmbeddedClauseType) : gaToLandau c ≠ Control.ClauseClass.fSubjunctive

No Gã clause type is a tensed-but-controlled F-subjunctive.

theorem Allotey2021.landau_predicts_control (c : Ga.EmbeddedClauseType) (hc : c ≠ Ga.EmbeddedClauseType.keji) (agr : Bool) : gaProfile c = Set.univ ↔ (gaToLandau c).HasOC agr

The scale agrees with the rows where the paper tests reference: OC exactly on the C-subjunctive, at any Agr value — Gã has no φ-agreement (exx 79–81, 123).

theorem Allotey2021.reduced_iff_not_finite (c : Ga.EmbeddedClauseType) : (∀ cd ∈ c.frame.codings, cd.isReduced = true) ↔ ¬c.complementizer.IsFinite

In [Noo07]'s typology the non-finite clause is the reduced one: .infinitive, the paper's own term for the bare-root ni-complement.

Table 4

inductive Allotey2021.IrrealisContext : Type

The five irrealis contexts of Table 4.

• subjunctive : IrrealisContext
• imperative : IrrealisContext
• conditional : IrrealisContext
• future : IrrealisContext
• embeddedControl : IrrealisContext

@[instance_reducible]

instance Allotey2021.instDecidableEqIrrealisContext : DecidableEq IrrealisContext

Equations

• Allotey2021.instDecidableEqIrrealisContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Allotey2021.instReprIrrealisContext.repr : IrrealisContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Allotey2021.instReprIrrealisContext : Repr IrrealisContext

Equations

• Allotey2021.instReprIrrealisContext = { reprPrec := Allotey2021.instReprIrrealisContext.repr }

def Allotey2021.contextOf : String → Option IrrealisContext

The context a row's clauseContext names.

Equations

• Allotey2021.contextOf "subjunctive" = some Allotey2021.IrrealisContext.subjunctive
• Allotey2021.contextOf "imperative" = some Allotey2021.IrrealisContext.imperative
• Allotey2021.contextOf "conditional" = some Allotey2021.IrrealisContext.conditional
• Allotey2021.contextOf "future" = some Allotey2021.IrrealisContext.future
• Allotey2021.contextOf "control" = some Allotey2021.IrrealisContext.embeddedControl
• Allotey2021.contextOf x✝ = none

inductive Allotey2021.Exponent : Type

The irrealis marker has three exponents, high tone on the subject, high tone on the verb, and the vowel segment a.

• subjectTone : Exponent
• verbTone : Exponent
• vowel : Exponent

@[instance_reducible]

instance Allotey2021.instDecidableEqExponent : DecidableEq Exponent

Equations

• Allotey2021.instDecidableEqExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Allotey2021.instReprExponent.repr : Exponent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Allotey2021.instReprExponent : Repr Exponent

Equations

• Allotey2021.instReprExponent = { reprPrec := Allotey2021.instReprExponent.repr }

@[instance_reducible]

instance Allotey2021.instFintypeExponent : Fintype Exponent

Equations

• Allotey2021.instFintypeExponent = { elems := { val := ↑Allotey2021.Exponent.enumList, nodup := Allotey2021.Exponent.enumList_nodup }, complete := Allotey2021.instFintypeExponent._proof_1 }

def Allotey2021.shows (row : Datum) : Exponent → Prop

A row shows an exponent.

Equations

• Allotey2021.shows row Allotey2021.Exponent.subjectTone = (row.feature? "subjectTone" = some "high")
• Allotey2021.shows row Allotey2021.Exponent.verbTone = (row.feature? "verbTone" = some "high")
• Allotey2021.shows row Allotey2021.Exponent.vowel = (row.feature? "irrealisVowel" = some "present")

@[instance_reducible]

instance Allotey2021.instDecidablePredExponentShows (row : Datum) : DecidablePred (shows row)

Equations

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

def Allotey2021.rowsIn (ctx : IrrealisContext) (j : Judgment) : List Datum

The rows in an irrealis context with judgment j.

Equations

• Allotey2021.rowsIn ctx j = List.filter (fun (row : Datum) => decide ((row.feature? "clauseContext").bind Allotey2021.contextOf = some ctx ∧ row.judgment = j)) Allotey2021.Examples.all

def Allotey2021.realization (ctx : IrrealisContext) : Finset Exponent

Table 4 is read off the rows, as the exponents some grammatical row shows in the context (exx 85–86, 93–97, 100–103).

Equations

• Allotey2021.realization ctx = {e : Allotey2021.Exponent | ∃ row ∈ Allotey2021.rowsIn ctx Judgment.acceptable, Allotey2021.shows row e}

theorem Allotey2021.realization_control : realization IrrealisContext.embeddedControl = {Exponent.subjectTone}

Embedded control realizes the marker as the subject's high tone alone.

theorem Allotey2021.control_realization_unique (c : IrrealisContext) : realization c = realization IrrealisContext.embeddedControl → c = IrrealisContext.embeddedControl

The embedded-control realization is unique among the five contexts; in particular it lacks the subjunctive's doubled high tone (ex 88).

theorem Allotey2021.realization_exact : (∃ row ∈ rowsIn IrrealisContext.embeddedControl Judgment.ungrammatical, shows row Exponent.verbTone) ∧ (∃ row ∈ rowsIn IrrealisContext.future Judgment.ungrammatical, shows row Exponent.subjectTone) ∧ ∃ row ∈ rowsIn IrrealisContext.subjunctive Judgment.ungrammatical, ¬shows row Exponent.verbTone

The realizations are exact: adding the verb's tone to the control clause (ex 88) or the subject's to the future (ex 96), or dropping the verb's from the subjunctive (ex 87), is ungrammatical.

Deriving the overt pronoun

def Allotey2021.HostsTone (f : Binding.MinimalPronoun.Form) : Prop

A tonal exponent needs a segmental host; the null form has none.

Equations

• Allotey2021.HostsTone f = (f ≠ Binding.MinimalPronoun.Form.null)

def Allotey2021.HostsControlTone (inv : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form) : Prop

The controlled-subject form must host the irrealis tone Table 4 places on the embedded-control subject.

Equations

• Allotey2021.HostsControlTone inv = (Allotey2021.Exponent.subjectTone ∈ Allotey2021.realization Allotey2021.IrrealisContext.embeddedControl → Allotey2021.HostsTone inv.controlForm)

theorem Allotey2021.null_pro_impossible (inv : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form) (h : inv.controlForm = Binding.MinimalPronoun.Form.null) : ¬HostsControlTone inv

Null PRO is impossible in Gã: a null controlled-subject form cannot host the irrealis tone.

theorem Allotey2021.ga_hostsControlTone : HostsControlTone gaInventory

The Gã inventory meets the tone-hosting requirement.

theorem Allotey2021.ga_overt_pro : gaInventory.controlForm = Binding.MinimalPronoun.Form.pronoun

Controlled subjects surface as overt pronouns.