Linglib.Phenomena.Control.Studies.Landau2015

source

inductive Phenomena.Control.Studies.Landau2015.ControlTier :

Type

The two tiers of obligatory control (table (119) of @cite{landau-2015}).

Predicative control (EC complements):

Selected by nonattitude predicates (implicative, aspectual, modal, evaluative)
PRO moves to Spec,Fin → control via syntactic predication
Forces exhaustive control (EC)
Complement head: transitive Fin_{[uD]}

Logophoric control (PC complements):

Selected by attitude predicates (factive, propositional, desiderative, interrogative)
C^OC projects a perspectival coordinate → control via predication + variable binding
Allows partial control (PC)
Complement head: transitive C^OC_{[uD]}
Associated with obligatory de se interpretation

predicative : ControlTier
Predicative control: nonattitude, predication only
logophoric : ControlTier
Logophoric control: attitude, predication + variable binding

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqControlTier :

DecidableEq ControlTier

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqControlTier x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Control.Studies.Landau2015.instBEqControlTier :

BEq ControlTier

Equations

Phenomena.Control.Studies.Landau2015.instBEqControlTier = { beq := Phenomena.Control.Studies.Landau2015.instBEqControlTier.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqControlTier.beq :

ControlTier → ControlTier → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqControlTier.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprControlTier :

Repr ControlTier

Equations

Phenomena.Control.Studies.Landau2015.instReprControlTier = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprControlTier.repr }

source

def Phenomena.Control.Studies.Landau2015.instReprControlTier.repr :

ControlTier → ℕ → Std.Format

Equations

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

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.isAttitude :

ControlTier → Bool

Logophoric control corresponds to attitude complements.

Equations

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.requiresSyntacticController :

ControlTier → Bool

Condition on syntactic predication ((90) in @cite{landau-2015}): "The argument predicated of must be syntactically represented."

In predicative control, the controller must be syntactically present because predication is a syntactic relation requiring two syntactically represented terms (the referential argument and the predicate).

In logophoric control, the AUTHOR/ADDRESSEE coordinate is discourse-anchored, not predication-dependent, so the controller may remain implicit.

Equations

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.allowsNonhumanPRO :

ControlTier → Bool

[−human] PRO is compatible with predicative control but incompatible with logophoric control ((81) in @cite{landau-2015}).

In predicative control, PRO is bound by a simple λ-operator; neither the binder nor the bindee carries any inherent semantic feature. In logophoric control, PRO is bound by pro_x/pro_y, which is mapped to the AUTHOR/ADDRESSEE function; since the latter is only defined for humans, the former will be too.

This is the negation of isAttitude: only logophoric control (attitude contexts) imposes a humanness requirement.

Equations

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.allowsPartialControl :

ControlTier → Bool

Partial control is available only under logophoric control. Predicative control forces exhaustive control (EC). @cite{landau-2015} Ch 5, §5.1

Equations

Phenomena.Control.Studies.Landau2015.ControlTier.allowsPartialControl = Phenomena.Control.Studies.Landau2015.ControlTier.isAttitude

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.obligatoryDeSe :

ControlTier → Bool

Obligatory de se arises only under logophoric control. Predicative contexts are free of the de se entailment. @cite{landau-2015} §3.4

Equations

Phenomena.Control.Studies.Landau2015.ControlTier.obligatoryDeSe = Phenomena.Control.Studies.Landau2015.ControlTier.isAttitude

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.allowsControlShift :

ControlTier → Bool

Control shift (from subject to object controller) is available only under logophoric control. Predicative control enters a biunique predication relation that no other DP can saturate. @cite{landau-2015} §4.3

Equations

Phenomena.Control.Studies.Landau2015.ControlTier.allowsControlShift = Phenomena.Control.Studies.Landau2015.ControlTier.isAttitude

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.allowsImplicitControl :

ControlTier → Bool

Implicit control is the complement of requiring a syntactic controller. Derived from the condition on syntactic predication (90).

Equations

Phenomena.Control.Studies.Landau2015.ControlTier.allowsImplicitControl = Phenomena.Control.Studies.Landau2015.ControlTier.isAttitude

Instances For

source

def Phenomena.Control.Studies.Landau2015.ControlTier.allowsSplitControl :

ControlTier → Bool

Split control (two arguments jointly control PRO) is available only under logophoric control. @cite{landau-2015} Ch 5, §5.2

Equations

Phenomena.Control.Studies.Landau2015.ControlTier.allowsSplitControl = Phenomena.Control.Studies.Landau2015.ControlTier.isAttitude

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.implicit_control_from_predication_condition (tier : ControlTier) :

tier.allowsImplicitControl = !tier.requiresSyntacticController

Implicit control derives from condition (90): predicative control requires a syntactically present controller, so allowsImplicitControl is the negation of requiresSyntacticController.

source

theorem Phenomena.Control.Studies.Landau2015.nonhuman_pro_from_attitude (tier : ControlTier) :

tier.allowsNonhumanPRO = !tier.isAttitude

[−human] PRO derives from the logophoric mechanism: allowsNonhumanPRO is the negation of isAttitude.

source

inductive Phenomena.Control.Studies.Landau2015.LandauPredicateClass :

Type

@cite{landau-2015}'s predicate classification by complement type.

(4) Predicates selecting untensed complements [−T] → nonattitude: (a) Implicative: avoid, dare, manage, remember, ... (b) Aspectual: begin, continue, finish, start, stop (c) Modal: have, is able, may, must, need, should (d) Evaluative: bold, crazy, kind, rude, silly, smart

(5) Predicates selecting tensed complements [+T] → attitude: (a) Factive: dislike, glad, hate, regret, sorry, ... (b) Propositional: affirm, believe, claim, declare, say, think (c) Desiderative: agree, choose, decide, hope, intend, want, ... (d) Interrogative: ask, guess, inquire, know, wonder

Under the TTC, (4) maps to predicative control and (5) to logophoric.

Note: (4d) evaluative predicates are adjectives, not verbs. No evaluative verbs exist in the English Fragment; this class is currently unreachable via derivedLandauClass.

implicative : LandauPredicateClass
aspectual : LandauPredicateClass
modal : LandauPredicateClass
evaluative : LandauPredicateClass
factive : LandauPredicateClass
propositional : LandauPredicateClass
desiderative : LandauPredicateClass
interrogative : LandauPredicateClass

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqLandauPredicateClass :

DecidableEq LandauPredicateClass

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqLandauPredicateClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Control.Studies.Landau2015.instBEqLandauPredicateClass.beq :

LandauPredicateClass → LandauPredicateClass → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqLandauPredicateClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instBEqLandauPredicateClass :

BEq LandauPredicateClass

Equations

Phenomena.Control.Studies.Landau2015.instBEqLandauPredicateClass = { beq := Phenomena.Control.Studies.Landau2015.instBEqLandauPredicateClass.beq }

source

def Phenomena.Control.Studies.Landau2015.instReprLandauPredicateClass.repr :

LandauPredicateClass → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprLandauPredicateClass :

Repr LandauPredicateClass

Equations

Phenomena.Control.Studies.Landau2015.instReprLandauPredicateClass = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprLandauPredicateClass.repr }

source

def Phenomena.Control.Studies.Landau2015.LandauPredicateClass.controlTier :

LandauPredicateClass → ControlTier

Map predicate class to control tier.

Equations

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.implicative_ec :

LandauPredicateClass.implicative.controlTier.allowsPartialControl = false

Nonattitude predicates force exhaustive control.

source

theorem Phenomena.Control.Studies.Landau2015.aspectual_ec :

LandauPredicateClass.aspectual.controlTier.allowsPartialControl = false

source

theorem Phenomena.Control.Studies.Landau2015.desiderative_pc :

LandauPredicateClass.desiderative.controlTier.allowsPartialControl = true

Attitude predicates allow partial control.

source

theorem Phenomena.Control.Studies.Landau2015.propositional_pc :

LandauPredicateClass.propositional.controlTier.allowsPartialControl = true

source

structure Phenomena.Control.Studies.Landau2015.FeatureTransmissionAsymmetry :

Type

The Feature Transmission asymmetry ((60) in @cite{landau-2015}).

This is the single most important mechanism in the TTC. It is the reason why [+Agr] blocks logophoric control but not predicative control (the OC-NC generalization).

(60a) The formation of a predication relation is not contingent on feature matching between the subject and the predicate. (60b) The formation of a variable binding relation is contingent on feature matching between the binder and the pronominal variable.

The asymmetry is independently motivated: predication tolerates φ-feature mismatches (Icelandic quirky constructions, (63)), while variable binding requires φ-agreement between binder and bindee (@cite{heim-2008}, @cite{kratzer-2009}).

predicationContingentOnFeatureMatch : Bool
(60a): Predication does NOT require feature matching.
variableBindingContingentOnFeatureMatch : Bool
(60b): Variable binding DOES require feature matching.

Instances For

source

def Phenomena.Control.Studies.Landau2015.ftAsymmetry :

FeatureTransmissionAsymmetry

The empirically motivated Feature Transmission asymmetry.

Equations

Phenomena.Control.Studies.Landau2015.ftAsymmetry = { predicationContingentOnFeatureMatch := false, variableBindingContingentOnFeatureMatch := true }

Instances For

source

def Phenomena.Control.Studies.Landau2015.agrBlocksControl :

ControlTier → Bool

The OC-NC generalization ((70) in @cite{landau-2015}):

"[+Agr] blocks logophoric control but not predicative control."

This is now DERIVED from the Feature Transmission asymmetry (60):

Predicative control uses predication → not contingent on feature matching (60a) → [+Agr] cannot block it
Logophoric control uses variable binding → contingent on feature matching (60b) → [+Agr] preempts Feature Transmission → blocks it

Equations

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

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.predicative_survives_agr :

agrBlocksControl ControlTier.predicative = false

Predicative control survives in inflected complements.

source

theorem Phenomena.Control.Studies.Landau2015.logophoric_blocked_by_agr :

agrBlocksControl ControlTier.logophoric = true

Logophoric control is blocked by inflected complements.

source

theorem Phenomena.Control.Studies.Landau2015.agr_blocks_derived_from_ft :

agrBlocksControl ControlTier.predicative = ftAsymmetry.predicationContingentOnFeatureMatch ∧ agrBlocksControl ControlTier.logophoric = ftAsymmetry.variableBindingContingentOnFeatureMatch

The OC-NC generalization is derived from the Feature Transmission asymmetry, not stipulated.

source

inductive Phenomena.Control.Studies.Landau2015.LandauClauseClass :

Type

@cite{landau-2004}'s finiteness scale, as recast in @cite{landau-2015}.

The [±T] distinction is subsumed by the attitude/nonattitude distinction:

C-subjunctives (untensed, [−T]) → nonattitude → predicative control
F-subjunctives (tensed, [+T,−Agr]) → attitude → logophoric control
Fully finite ([+T,+Agr]) → no control (OC-NC generalization)

F-subjunctives DO permit OC (logophoric). Whether OC is realized depends on [±Agr]: [+Agr] blocks logophoric control per the OC-NC generalization. Greek controlled subjunctives ([+T,−Agr]) show OC; Greek indicatives ([+T,+Agr]) do not.

cSubjunctive : LandauClauseClass
fSubjunctive : LandauClauseClass
finite : LandauClauseClass

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqLandauClauseClass :

DecidableEq LandauClauseClass

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqLandauClauseClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Control.Studies.Landau2015.instBEqLandauClauseClass.beq :

LandauClauseClass → LandauClauseClass → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqLandauClauseClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instBEqLandauClauseClass :

BEq LandauClauseClass

Equations

Phenomena.Control.Studies.Landau2015.instBEqLandauClauseClass = { beq := Phenomena.Control.Studies.Landau2015.instBEqLandauClauseClass.beq }

source

def Phenomena.Control.Studies.Landau2015.instReprLandauClauseClass.repr :

LandauClauseClass → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprLandauClauseClass :

Repr LandauClauseClass

Equations

Phenomena.Control.Studies.Landau2015.instReprLandauClauseClass = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprLandauClauseClass.repr }

source

def Phenomena.Control.Studies.Landau2015.LandauClauseClass.controlTier :

LandauClauseClass → Option ControlTier

Map clause class to control tier (when control obtains).

Equations

Instances For

source

def Phenomena.Control.Studies.Landau2015.LandauClauseClass.permitsOC :

LandauClauseClass → Bool

Whether a clause class structurally permits OC.

Both C-subjunctives and F-subjunctives permit OC. F-subjunctives permit logophoric OC when [−Agr]; this OC is blocked by [+Agr] per the OC-NC generalization. Fully finite clauses ([+T,+Agr]) never permit OC.

See hasOCWithAgr for the Agr-sensitive version.

Equations

Instances For

source

def Phenomena.Control.Studies.Landau2015.LandauClauseClass.hasOCWithAgr (c : LandauClauseClass) (hasAgr : Bool) :

Bool

Whether OC is realized given Agr status.

Composes the clause class with the OC-NC generalization:

C-subjunctives: always OC (predicative, Agr-independent)
F-subjunctives [−Agr]: OC (logophoric)
F-subjunctives [+Agr]: no OC (logophoric blocked by Agr)
Fully finite: no OC

Equations

c.hasOCWithAgr hasAgr = match c.controlTier with | none => false | some tier => c.permitsOC && (!hasAgr || !Phenomena.Control.Studies.Landau2015.agrBlocksControl tier)

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.cSubjunctive_oc_any_agr (agr : Bool) :

LandauClauseClass.cSubjunctive.hasOCWithAgr agr = true

C-subjunctives have OC regardless of Agr.

source

theorem Phenomena.Control.Studies.Landau2015.fSubjunctive_oc_without_agr :

LandauClauseClass.fSubjunctive.hasOCWithAgr false = true

F-subjunctives have OC when [−Agr].

source

theorem Phenomena.Control.Studies.Landau2015.fSubjunctive_no_oc_with_agr :

LandauClauseClass.fSubjunctive.hasOCWithAgr true = false

F-subjunctives lose OC when [+Agr] (the OC-NC generalization).

source

theorem Phenomena.Control.Studies.Landau2015.finite_no_oc (agr : Bool) :

LandauClauseClass.finite.hasOCWithAgr agr = false

Fully finite clauses never have OC.

source

structure Phenomena.Control.Studies.Landau2015.TTCContrast :

Type

The six empirical contrasts between the two types of control (table (80) in @cite{landau-2015}).

Each contrast shows a property that aligns with exactly one control tier. The "✓" entries indicate the tier where the property is available; the "*" entries indicate the tier where it is blocked.

Property	Predicative	Logophoric
Inflected complement	✓	*
[−human] PRO	✓	*
Implicit control	*	✓
Control shift	*	✓
Partial control	*	✓
Split control	*	✓

name : String
predicative : Bool
Available under predicative control?
logophoric : Bool
Available under logophoric control?

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqTTCContrast :

DecidableEq TTCContrast

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqTTCContrast = Phenomena.Control.Studies.Landau2015.instDecidableEqTTCContrast.decEq

source

def Phenomena.Control.Studies.Landau2015.instDecidableEqTTCContrast.decEq (x✝ x✝¹ : TTCContrast) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

def Phenomena.Control.Studies.Landau2015.instBEqTTCContrast.beq :

TTCContrast → TTCContrast → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Control.Studies.Landau2015.instBEqTTCContrast.beq x✝¹ x✝ = false

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instBEqTTCContrast :

BEq TTCContrast

Equations

Phenomena.Control.Studies.Landau2015.instBEqTTCContrast = { beq := Phenomena.Control.Studies.Landau2015.instBEqTTCContrast.beq }

source

instance Phenomena.Control.Studies.Landau2015.instReprTTCContrast :

Repr TTCContrast

Equations

Phenomena.Control.Studies.Landau2015.instReprTTCContrast = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprTTCContrast.repr }

source

def Phenomena.Control.Studies.Landau2015.instReprTTCContrast.repr :

TTCContrast → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instInhabitedTTCContrast :

Inhabited TTCContrast

Equations

Phenomena.Control.Studies.Landau2015.instInhabitedTTCContrast = { default := Phenomena.Control.Studies.Landau2015.instInhabitedTTCContrast.default }

source

def Phenomena.Control.Studies.Landau2015.instInhabitedTTCContrast.default :

TTCContrast

Equations

Phenomena.Control.Studies.Landau2015.instInhabitedTTCContrast.default = { name := default, predicative := default, logophoric := default }

Instances For

source

def Phenomena.Control.Studies.Landau2015.ttcContrasts :

List TTCContrast

The six contrasts from table (80), encoded as data.

Equations

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

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.inflected_complement_predicative :

agrBlocksControl ControlTier.predicative = false ∧ agrBlocksControl ControlTier.logophoric = true

Every contrast in table (80) is derived from ControlTier properties.

source

theorem Phenomena.Control.Studies.Landau2015.nonhuman_pro_predicative :

ControlTier.predicative.allowsNonhumanPRO = true ∧ ControlTier.logophoric.allowsNonhumanPRO = false

source

theorem Phenomena.Control.Studies.Landau2015.implicit_control_logophoric :

ControlTier.predicative.allowsImplicitControl = false ∧ ControlTier.logophoric.allowsImplicitControl = true

source

theorem Phenomena.Control.Studies.Landau2015.control_shift_logophoric :

ControlTier.predicative.allowsControlShift = false ∧ ControlTier.logophoric.allowsControlShift = true

source

theorem Phenomena.Control.Studies.Landau2015.partial_control_logophoric :

ControlTier.predicative.allowsPartialControl = false ∧ ControlTier.logophoric.allowsPartialControl = true

source

theorem Phenomena.Control.Studies.Landau2015.split_control_logophoric :

ControlTier.predicative.allowsSplitControl = false ∧ ControlTier.logophoric.allowsSplitControl = true

source

theorem Phenomena.Control.Studies.Landau2015.ttcContrasts_consistent :

(!agrBlocksControl ControlTier.predicative) = ttcContrasts [0]!.predicative ∧ (!agrBlocksControl ControlTier.logophoric) = ttcContrasts [0]!.logophoric ∧ ControlTier.predicative.allowsNonhumanPRO = ttcContrasts [1]!.predicative ∧ ControlTier.logophoric.allowsNonhumanPRO = ttcContrasts [1]!.logophoric ∧ ControlTier.predicative.allowsImplicitControl = ttcContrasts [2]!.predicative ∧ ControlTier.logophoric.allowsImplicitControl = ttcContrasts [2]!.logophoric ∧ ControlTier.predicative.allowsControlShift = ttcContrasts [3]!.predicative ∧ ControlTier.logophoric.allowsControlShift = ttcContrasts [3]!.logophoric ∧ ControlTier.predicative.allowsPartialControl = ttcContrasts [4]!.predicative ∧ ControlTier.logophoric.allowsPartialControl = ttcContrasts [4]!.logophoric ∧ ControlTier.predicative.allowsSplitControl = ttcContrasts [5]!.predicative ∧ ControlTier.logophoric.allowsSplitControl = ttcContrasts [5]!.logophoric

The ttcContrasts data agrees with the derived ControlTier properties. Each contrast's Bool pair matches the corresponding tier function.

source

All six contrasts are systematically derived from the TTC: the first two are predicative-only, the last four are logophoric-only. This is the central empirical prediction of the book.

source

theorem Phenomena.Control.Studies.Landau2015.ec_resists_impersonal_passives :

ControlTier.predicative.requiresSyntacticController = true ∧ ControlTier.logophoric.requiresSyntacticController = false

EC verbs resist impersonal passives ((98) in @cite{landau-2015}).

This is a direct consequence of (90): predicative control requires a syntactically present controller, and impersonal passives suppress the external argument. PC verbs allow impersonal passives because logophoric control does not require a syntactically present controller.

Cross-linguistic evidence: Hebrew (99), German (96a, 100), Dutch (101), Russian (102).

source

structure Phenomena.Control.Studies.Landau2015.BVASyncretism :

Type

Cross-linguistic syncretism among BVA forms.

Records whether each BVA context uses the same form as the referential (free) pronoun. "=" means syncretic with the referential pronoun; "×" means a distinct form is used.

Used by @cite{ostrove-2026} (table 92) and grounded in the minimal pronoun approach of @cite{kratzer-2009} and @cite{safir-2014}.

language : String
reflexiveEqReferential : Bool
Is the reflexive form identical to the referential pronoun?
controlledEqReferential : Bool
Is the controlled subject form identical to the referential pronoun?
boundVarEqReferential : Bool
Is the bound variable pronoun identical to the referential pronoun?

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqBVASyncretism :

DecidableEq BVASyncretism

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqBVASyncretism = Phenomena.Control.Studies.Landau2015.instDecidableEqBVASyncretism.decEq

source

def Phenomena.Control.Studies.Landau2015.instDecidableEqBVASyncretism.decEq (x✝ x✝¹ : BVASyncretism) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instBEqBVASyncretism :

BEq BVASyncretism

Equations

Phenomena.Control.Studies.Landau2015.instBEqBVASyncretism = { beq := Phenomena.Control.Studies.Landau2015.instBEqBVASyncretism.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqBVASyncretism.beq :

BVASyncretism → BVASyncretism → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Control.Studies.Landau2015.instBEqBVASyncretism.beq x✝¹ x✝ = false

Instances For

source

def Phenomena.Control.Studies.Landau2015.instReprBVASyncretism.repr :

BVASyncretism → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprBVASyncretism :

Repr BVASyncretism

Equations

Phenomena.Control.Studies.Landau2015.instReprBVASyncretism = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprBVASyncretism.repr }

source

def Phenomena.Control.Studies.Landau2015.syncretismFromInventory {Form : Type} [BEq Form] (inv : Syntax.Minimalism.MinimalPronoun.MinPronInventory Form) (lang : String := "") :

BVASyncretism

Derive syncretism from a vocabulary item inventory.

A context is syncretic with the referential pronoun iff its realized form equals the elsewhere (pronoun) form — i.e., no context-specific vocabulary item overrides the default.

Equations

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

Instances For

source

inductive Phenomena.Control.Studies.Landau2015.CopyControlType :

Type

Types of copy control (@cite{polinsky-potsdam-2006}).

Copy control: the subject of a control clause is a phonologically overt copy of its controller. Four subtypes are distinguished by the nature of the copy and its distribution.

fullCopy : CopyControlType
Full copy: PRO is a full DP copy of the controller. Attested in San Lucas Quievaní Zapotec, Copala Triqui.
logophoricPronominal : CopyControlType
Logophoric pronominal: PRO is a pronoun, occurs only in attitude reports. Attested in Gengbe, Mandarin.
scopeSensitivePronominal : CopyControlType
Scope-sensitive pronominal: PRO is a pronoun, triggered by scope-taking operators (focus). Attested in Italian, Hungarian, European Portuguese.
obligatoryPronominal : CopyControlType
Obligatory pronominal: PRO is an overt clitic pronoun in all control contexts, showing the full OC signature. Attested in SMPM, Gã, Büli.

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqCopyControlType :

DecidableEq CopyControlType

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqCopyControlType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Control.Studies.Landau2015.instBEqCopyControlType :

BEq CopyControlType

Equations

Phenomena.Control.Studies.Landau2015.instBEqCopyControlType = { beq := Phenomena.Control.Studies.Landau2015.instBEqCopyControlType.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqCopyControlType.beq :

CopyControlType → CopyControlType → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqCopyControlType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprCopyControlType :

Repr CopyControlType

Equations

Phenomena.Control.Studies.Landau2015.instReprCopyControlType = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprCopyControlType.repr }

source

def Phenomena.Control.Studies.Landau2015.instReprCopyControlType.repr :

CopyControlType → ℕ → Std.Format

Equations

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

Instances For

source

structure Phenomena.Control.Studies.Landau2015.CopyControlProfile :

Type

Properties distinguishing copy control types.

controlType : CopyControlType
showsOC : Bool
Does the copy show the full OC signature (bound variable, exhaustive)?
attitudeOnly : Bool
Is the copy restricted to attitude report contexts?
requiresScopeOperator : Bool
Does the copy require a scope-taking operator (focus, only)?
copyCanBearFocus : Bool
Can the copy bear focus?

Instances For

source

def Phenomena.Control.Studies.Landau2015.instDecidableEqCopyControlProfile.decEq (x✝ x✝¹ : CopyControlProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqCopyControlProfile :

DecidableEq CopyControlProfile

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqCopyControlProfile = Phenomena.Control.Studies.Landau2015.instDecidableEqCopyControlProfile.decEq

source

def Phenomena.Control.Studies.Landau2015.instBEqCopyControlProfile.beq :

CopyControlProfile → CopyControlProfile → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Control.Studies.Landau2015.instBEqCopyControlProfile.beq x✝¹ x✝ = false

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instBEqCopyControlProfile :

BEq CopyControlProfile

Equations

Phenomena.Control.Studies.Landau2015.instBEqCopyControlProfile = { beq := Phenomena.Control.Studies.Landau2015.instBEqCopyControlProfile.beq }

source

instance Phenomena.Control.Studies.Landau2015.instReprCopyControlProfile :

Repr CopyControlProfile

Equations

Phenomena.Control.Studies.Landau2015.instReprCopyControlProfile = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprCopyControlProfile.repr }

source

def Phenomena.Control.Studies.Landau2015.instReprCopyControlProfile.repr :

CopyControlProfile → ℕ → Std.Format

Equations

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

Instances For

source

def Phenomena.Control.Studies.Landau2015.copyControlProfile :

CopyControlType → CopyControlProfile

Profile for each copy control type.

Equations

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

Instances For

source

structure Phenomena.Control.Studies.Landau2015.ExemptAnaphorProfile :

Type

Exempt anaphors (@cite{pollard-sag-1992}): reflexive forms used outside their canonical binding domain (Condition A domain).

Key constraint: exempt anaphors cannot have quantified antecedents.

hasExemptAnaphors : Bool
Exempt anaphors available in this language
allowsQuantifiedAntecedent : Bool
Can exempt anaphors have quantified antecedents?

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqExemptAnaphorProfile :

DecidableEq ExemptAnaphorProfile

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqExemptAnaphorProfile = Phenomena.Control.Studies.Landau2015.instDecidableEqExemptAnaphorProfile.decEq

source

def Phenomena.Control.Studies.Landau2015.instDecidableEqExemptAnaphorProfile.decEq (x✝ x✝¹ : ExemptAnaphorProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instBEqExemptAnaphorProfile :

BEq ExemptAnaphorProfile

Equations

Phenomena.Control.Studies.Landau2015.instBEqExemptAnaphorProfile = { beq := Phenomena.Control.Studies.Landau2015.instBEqExemptAnaphorProfile.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqExemptAnaphorProfile.beq :

ExemptAnaphorProfile → ExemptAnaphorProfile → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Control.Studies.Landau2015.instBEqExemptAnaphorProfile.beq x✝¹ x✝ = false

Instances For

source

def Phenomena.Control.Studies.Landau2015.instReprExemptAnaphorProfile.repr :

ExemptAnaphorProfile → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprExemptAnaphorProfile :

Repr ExemptAnaphorProfile

Equations

Phenomena.Control.Studies.Landau2015.instReprExemptAnaphorProfile = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprExemptAnaphorProfile.repr }

source

inductive Phenomena.Control.Studies.Landau2015.ControlDerivation :

Type

The two analyses of obligatory control derivation.

baseGeneration : ControlDerivation
Controller base-generated in matrix; PRO base-generated in embedded clause. Two distinct syntactic positions, linked by variable binding.
movement : ControlDerivation
Controller enters derivation in embedded subject position and moves to matrix position. One DP, two copies.

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqControlDerivation :

DecidableEq ControlDerivation

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqControlDerivation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Control.Studies.Landau2015.instBEqControlDerivation :

BEq ControlDerivation

Equations

Phenomena.Control.Studies.Landau2015.instBEqControlDerivation = { beq := Phenomena.Control.Studies.Landau2015.instBEqControlDerivation.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqControlDerivation.beq :

ControlDerivation → ControlDerivation → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqControlDerivation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprControlDerivation :

Repr ControlDerivation

Equations

Phenomena.Control.Studies.Landau2015.instReprControlDerivation = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprControlDerivation.repr }

source

def Phenomena.Control.Studies.Landau2015.instReprControlDerivation.repr :

ControlDerivation → ℕ → Std.Format

Equations

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

Instances For

source

def Phenomena.Control.Studies.Landau2015.predictsExemptWithQuantifiedController :

ControlDerivation → Bool

Movement predicts exempt anaphors are UNAVAILABLE with quantified controllers. Base-generation predicts they ARE available.

Equations

Instances For

source

inductive Phenomena.Control.Studies.Landau2015.DeSeReading :

Type

The two logophoric readings of OC PRO under attitude predicates (table (36) in @cite{landau-2015}).

Under logophoric control, PRO is bound by a projected coordinate of the embedded context of evaluation. Which coordinate is projected depends on the object control verb subclass:

Psychological verbs (convince, persuade, tempt) project the AUTHOR coordinate → obligatory de se
Communicative verbs (tell, ask, recommend) project the ADDRESSEE coordinate → obligatory de te

deSe : DeSeReading
PRO = AUTHOR(i'): attitude holder's identification of self
deTe : DeSeReading
PRO = ADDRESSEE(i'): attitude holder's identification of addressee

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqDeSeReading :

DecidableEq DeSeReading

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqDeSeReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Control.Studies.Landau2015.instBEqDeSeReading :

BEq DeSeReading

Equations

Phenomena.Control.Studies.Landau2015.instBEqDeSeReading = { beq := Phenomena.Control.Studies.Landau2015.instBEqDeSeReading.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqDeSeReading.beq :

DeSeReading → DeSeReading → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqDeSeReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprDeSeReading :

Repr DeSeReading

Equations

Phenomena.Control.Studies.Landau2015.instReprDeSeReading = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprDeSeReading.repr }

source

def Phenomena.Control.Studies.Landau2015.instReprDeSeReading.repr :

DeSeReading → ℕ → Std.Format

Equations

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

Instances For

source

inductive Phenomena.Control.Studies.Landau2015.ObjectControlSubclass :

Type

Object control verb subclasses (table (36)).

psychological : ObjectControlSubclass
Psychological verbs: convince, persuade, dissuade, tempt
communicative : ObjectControlSubclass
Communicative verbs: tell, ask, urge, recommend

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instDecidableEqObjectControlSubclass :

DecidableEq ObjectControlSubclass

Equations

Phenomena.Control.Studies.Landau2015.instDecidableEqObjectControlSubclass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

instance Phenomena.Control.Studies.Landau2015.instBEqObjectControlSubclass :

BEq ObjectControlSubclass

Equations

Phenomena.Control.Studies.Landau2015.instBEqObjectControlSubclass = { beq := Phenomena.Control.Studies.Landau2015.instBEqObjectControlSubclass.beq }

source

def Phenomena.Control.Studies.Landau2015.instBEqObjectControlSubclass.beq :

ObjectControlSubclass → ObjectControlSubclass → Bool

Equations

Phenomena.Control.Studies.Landau2015.instBEqObjectControlSubclass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

def Phenomena.Control.Studies.Landau2015.instReprObjectControlSubclass.repr :

ObjectControlSubclass → ℕ → Std.Format

Equations

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

Instances For

source

instance Phenomena.Control.Studies.Landau2015.instReprObjectControlSubclass :

Repr ObjectControlSubclass

Equations

Phenomena.Control.Studies.Landau2015.instReprObjectControlSubclass = { reprPrec := Phenomena.Control.Studies.Landau2015.instReprObjectControlSubclass.repr }

source

def Phenomena.Control.Studies.Landau2015.objectControlReading :

ObjectControlSubclass → DeSeReading

Map object control subclass to its logophoric reading. Psychological verbs bind the AUTHOR coordinate (de se); communicative verbs bind the ADDRESSEE coordinate (de te).

Equations

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.psychological_deSe :

objectControlReading ObjectControlSubclass.psychological = DeSeReading.deSe

source

theorem Phenomena.Control.Studies.Landau2015.communicative_deTe :

objectControlReading ObjectControlSubclass.communicative = DeSeReading.deTe

source

def Phenomena.Control.Studies.Landau2015.derivedLandauClass (v : Core.Verbs.VerbCore) :

Option LandauPredicateClass

Derive @cite{landau-2015}'s predicate class from VerbCore fields.

This creates a bridge from Fragment verb entries to the TTC by deriving the predicate classification from existing semantic fields rather than storing it independently.

Returns none when the classification cannot be determined from the available fields (e.g., try has no implicativeBuilder, attitudeBuilder, or cosType).

Mapping:

cosType present → .aspectual (begin, stop, continue, ...)
implicativeBuilder present → .implicative (manage, fail, ...)
causativeBuilder present → .implicative (force, cause — implicative causatives in Landau's (4a))
factivePresup and attitude → .factive (regret, know, ...)
attitudeBuilder.doxastic → .propositional (believe, think, ...)
attitudeBuilder.preferential → .desiderative (want, hope, ...)
takesQuestionBase without attitude → .interrogative (wonder, ask)

Equations

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

Instances For

source

def Phenomena.Control.Studies.Landau2015.derivedControlTier (v : Core.Verbs.VerbCore) :

Option ControlTier

Derive control tier from VerbCore fields.

A verb induces logophoric control iff it selects an attitude complement — detected by the presence of attitudeBuilder, factivePresup, or takesQuestionBase. Otherwise it induces predicative control.

Returns none for verbs that are not control verbs.

Equations

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

Instances For

source

theorem Phenomena.Control.Studies.Landau2015.stop_aspectual :

derivedLandauClass Fragments.English.Predicates.Verbal.stop.toVerbCore = some LandauPredicateClass.aspectual

"stop" (CoS cessation) → aspectual → predicative

source

theorem Phenomena.Control.Studies.Landau2015.start_aspectual :

derivedLandauClass Fragments.English.Predicates.Verbal.start.toVerbCore = some LandauPredicateClass.aspectual

"start" (CoS inception) → aspectual → predicative

source

theorem Phenomena.Control.Studies.Landau2015.begin_aspectual :

derivedLandauClass Fragments.English.Predicates.Verbal.begin_.toVerbCore = some LandauPredicateClass.aspectual

"begin" (CoS inception) → aspectual → predicative

source

theorem Phenomena.Control.Studies.Landau2015.continue_aspectual :

derivedLandauClass Fragments.English.Predicates.Verbal.continue_.toVerbCore = some LandauPredicateClass.aspectual

"continue" (CoS continuation) → aspectual → predicative

source

theorem Phenomena.Control.Studies.Landau2015.manage_implicative :

derivedLandauClass Fragments.English.Predicates.Verbal.manage.toVerbCore = some LandauPredicateClass.implicative

"manage" (positive implicative) → implicative → predicative

source

theorem Phenomena.Control.Studies.Landau2015.fail_implicative :

derivedLandauClass Fragments.English.Predicates.Verbal.fail.toVerbCore = some LandauPredicateClass.implicative

"fail" (negative implicative) → implicative → predicative

source

theorem Phenomena.Control.Studies.Landau2015.remember_implicative :

derivedLandauClass Fragments.English.Predicates.Verbal.remember.toVerbCore = some LandauPredicateClass.implicative

"remember" (positive implicative) → implicative → predicative

source

theorem Phenomena.Control.Studies.Landau2015.forget_implicative :

derivedLandauClass Fragments.English.Predicates.Verbal.forget.toVerbCore = some LandauPredicateClass.implicative

"forget" (negative implicative) → implicative → predicative

source

theorem Phenomena.Control.Studies.Landau2015.force_implicative :

derivedLandauClass Fragments.English.Predicates.Verbal.force.toVerbCore = some LandauPredicateClass.implicative

"force" (coercive causative) → implicative → predicative

source

theorem Phenomena.Control.Studies.Landau2015.want_desiderative :

derivedLandauClass Fragments.English.Predicates.Verbal.want.toVerbCore = some LandauPredicateClass.desiderative

"want" (preferential attitude) → desiderative → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.hope_desiderative :

derivedLandauClass Fragments.English.Predicates.Verbal.hope.toVerbCore = some LandauPredicateClass.desiderative

"hope" (preferential attitude) → desiderative → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.promise_desiderative :

derivedLandauClass Fragments.English.Predicates.Verbal.promise.toVerbCore = some LandauPredicateClass.desiderative

"promise" (preferential attitude) → desiderative → logophoric. Previously unclassified; fixed by adding attitudeBuilder to the Fragment entry per @cite{landau-2015} (5c).

source

theorem Phenomena.Control.Studies.Landau2015.persuade_desiderative :

derivedLandauClass Fragments.English.Predicates.Verbal.persuade.toVerbCore = some LandauPredicateClass.desiderative

"persuade" (preferential attitude, object control) → desiderative → logophoric. Previously unclassified; fixed by adding attitudeBuilder per @cite{landau-2015} table (36).

source

theorem Phenomena.Control.Studies.Landau2015.regret_factive :

derivedLandauClass Fragments.English.Predicates.Verbal.regret.toVerbCore = some LandauPredicateClass.factive

"regret" (factive) → factive → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.know_factive :

derivedLandauClass Fragments.English.Predicates.Verbal.know.toVerbCore = some LandauPredicateClass.factive

"know" (factive + question) → factive → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.believe_propositional :

derivedLandauClass Fragments.English.Predicates.Verbal.believe.toVerbCore = some LandauPredicateClass.propositional

"believe" (doxastic attitude) → propositional → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.think_propositional :

derivedLandauClass Fragments.English.Predicates.Verbal.think.toVerbCore = some LandauPredicateClass.propositional

"think" (doxastic attitude) → propositional → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.wonder_interrogative :

derivedLandauClass Fragments.English.Predicates.Verbal.wonder.toVerbCore = some LandauPredicateClass.interrogative

"wonder" (question-embedding, non-attitude) → interrogative → logophoric

source

theorem Phenomena.Control.Studies.Landau2015.try_unclassifiable :

derivedLandauClass Fragments.English.Predicates.Verbal.try_.toVerbCore = none

"try" has no cosType, implicativeBuilder, causativeBuilder, factivePresup, takesQuestionBase, or attitudeBuilder. It cannot be classified by derivedLandauClass. This is correct: "try" is not implicative (trying doesn't entail succeeding) and not clearly attitudinal.

source

theorem Phenomena.Control.Studies.Landau2015.stop_predicative_tier :