Documentation

Linglib.Phenomena.NullSubject.Defs

Subject-Context Vocabulary #

Framework-agnostic vocabulary for the loci where a language makes a null-vs-overt subject decision. The four orthogonal axes here suffice to distinguish the empirical cases that 2026-era pro-drop literature actually engages with:

Person — partial pro-drop (Hebrew: 1/2 only; Brazilian Portuguese: 3rd-person dependent).
Finiteness — non-finite control vs finite matrix subject.
ClauseRole — matrix vs embedded-finite vs control-subject locus.
ABarStatus — anti-agreement effect (Tarifit, Fiorentino, Wolof: null subjects only available under Ā-extraction; @cite{baier-2018}).

A SubjectContext is a 4-tuple (one cell of the cross-classification) and a SubjectAssignment : SubjectContext → Exponent (defined in Universals.lean) is the abstract interface a syntactic theory must provide to be evaluated against the universals in this directory.

Convenience constructors (matrixFinite, embeddedFinite, controlled) cover the canonical 3rd-person in-situ loci that study files reach for. matrixExtracted is the locus for anti-agreement diagnostics.

@[reducible, inline]

abbrev Phenomena.NullSubject.Person :

Grammatical person. Aliased to UD.Person for cross-linguistic compatibility with the rest of linglib's morphological feature system; constructors are .first, .second, .third, .zero.

Equations

Phenomena.NullSubject.Person = UD.Person

Instances For

def Phenomena.NullSubject.thematicPersons :

The thematic persons (1st, 2nd, 3rd). .zero (impersonal) is excluded because the typological universals here are about thematic-subject realization; impersonal subjects are governed by a separate parameter (cf. expletive vs null-expletive).

Equations

Phenomena.NullSubject.thematicPersons = [UD.Person.first, UD.Person.second, UD.Person.third]

Instances For

inductive Phenomena.NullSubject.Finiteness :

Finiteness of the clause hosting the subject locus. Coarser than @cite{landau-2004}'s scale — that finer-grained version belongs in a syntactic theory file, not here.

finite : Finiteness
Finite clause (independent T, agreement morphology).
nonfinite : Finiteness
Non-finite clause (control, raising, ECM, gerundive, ...).

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instDecidableEqFiniteness :

DecidableEq Finiteness

Equations

Phenomena.NullSubject.instDecidableEqFiniteness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.NullSubject.instReprFiniteness.repr :

Finiteness → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instReprFiniteness :

Repr Finiteness

Equations

Phenomena.NullSubject.instReprFiniteness = { reprPrec := Phenomena.NullSubject.instReprFiniteness.repr }

@[implicit_reducible]

instance Phenomena.NullSubject.instInhabitedFiniteness :

Inhabited Finiteness

Equations

Phenomena.NullSubject.instInhabitedFiniteness = { default := Phenomena.NullSubject.instInhabitedFiniteness.default }

def Phenomena.NullSubject.instInhabitedFiniteness.default :

Equations

Phenomena.NullSubject.instInhabitedFiniteness.default = Phenomena.NullSubject.Finiteness.finite

Instances For

inductive Phenomena.NullSubject.ClauseRole :

The structural role of the clause hosting the subject locus. The three values exhaust the loci where the pro-drop / overt-PRO typology actually distinguishes languages.

matrix : ClauseRole
Matrix clause subject.
embeddedFinite : ClauseRole
Subject of a finite embedded clause (relevant for embedded-pro-drop diagnostics).
controlSubject : ClauseRole
Subject of an obligatory-control clause (PRO position).

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instDecidableEqClauseRole :

DecidableEq ClauseRole

Equations

Phenomena.NullSubject.instDecidableEqClauseRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.NullSubject.instReprClauseRole :

Repr ClauseRole

Equations

Phenomena.NullSubject.instReprClauseRole = { reprPrec := Phenomena.NullSubject.instReprClauseRole.repr }

def Phenomena.NullSubject.instReprClauseRole.repr :

ClauseRole → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instInhabitedClauseRole :

Inhabited ClauseRole

Equations

Phenomena.NullSubject.instInhabitedClauseRole = { default := Phenomena.NullSubject.instInhabitedClauseRole.default }

def Phenomena.NullSubject.instInhabitedClauseRole.default :

Equations

Phenomena.NullSubject.instInhabitedClauseRole.default = Phenomena.NullSubject.ClauseRole.matrix

Instances For

inductive Phenomena.NullSubject.ABarStatus :

Whether the subject is in situ or has undergone Ā-extraction. Distinguished here because anti-agreement effects (Tarifit, Fiorentino, Wolof; @cite{baier-2018}) license null subjects only under Ā-extraction.

insitu : ABarStatus
Subject in situ (no Ā-extraction).
aBarExtracted : ABarStatus
Subject has undergone Ā-extraction (relativized, wh-fronted, focus-fronted, topicalized).

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instDecidableEqABarStatus :

DecidableEq ABarStatus

Equations

Phenomena.NullSubject.instDecidableEqABarStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.NullSubject.instReprABarStatus :

Repr ABarStatus

Equations

Phenomena.NullSubject.instReprABarStatus = { reprPrec := Phenomena.NullSubject.instReprABarStatus.repr }

def Phenomena.NullSubject.instReprABarStatus.repr :

ABarStatus → ℕ → Std.Format

Equations

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

Instances For

def Phenomena.NullSubject.instInhabitedABarStatus.default :

Equations

Phenomena.NullSubject.instInhabitedABarStatus.default = Phenomena.NullSubject.ABarStatus.insitu

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instInhabitedABarStatus :

Inhabited ABarStatus

Equations

Phenomena.NullSubject.instInhabitedABarStatus = { default := Phenomena.NullSubject.instInhabitedABarStatus.default }

structure Phenomena.NullSubject.SubjectContext :

A cell of the four-way cross-classification: a single locus at which a language must decide between a null and an overt subject exponent.

person : Person
finiteness : Finiteness
clauseRole : ClauseRole
aBarStatus : ABarStatus

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instDecidableEqSubjectContext :

DecidableEq SubjectContext

Equations

Phenomena.NullSubject.instDecidableEqSubjectContext = Phenomena.NullSubject.instDecidableEqSubjectContext.decEq

def Phenomena.NullSubject.instDecidableEqSubjectContext.decEq (x✝ x✝¹ : SubjectContext) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instReprSubjectContext :

Repr SubjectContext

Equations

Phenomena.NullSubject.instReprSubjectContext = { reprPrec := Phenomena.NullSubject.instReprSubjectContext.repr }

def Phenomena.NullSubject.instReprSubjectContext.repr :

SubjectContext → ℕ → Std.Format

Equations

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

Instances For

inductive Phenomena.NullSubject.Exponent :

The exponent decision at a SubjectContext: null vs overt. The typology this directory tracks reduces to a function SubjectContext → Exponent.

null : Exponent
Silent subject (pro / null PRO / dropped subject).
overt : Exponent
Overt subject (full pronoun, clitic, agreement-doubled pronoun, overt PRO).

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instDecidableEqExponent :

DecidableEq Exponent

Equations

Phenomena.NullSubject.instDecidableEqExponent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.NullSubject.instReprExponent.repr :

Exponent → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.NullSubject.instReprExponent :

Equations

Phenomena.NullSubject.instReprExponent = { reprPrec := Phenomena.NullSubject.instReprExponent.repr }

@[implicit_reducible]

instance Phenomena.NullSubject.instInhabitedExponent :

Inhabited Exponent

Equations

Phenomena.NullSubject.instInhabitedExponent = { default := Phenomena.NullSubject.instInhabitedExponent.default }

def Phenomena.NullSubject.instInhabitedExponent.default :

Equations

Phenomena.NullSubject.instInhabitedExponent.default = Phenomena.NullSubject.Exponent.null

Instances For

def Phenomena.NullSubject.SubjectContext.matrixFinite (p : Person) :

Matrix finite subject of person p (in situ). The canonical locus for "is this language pro-drop?".

Equations

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

Instances For

def Phenomena.NullSubject.SubjectContext.embeddedFinite (p : Person) :

Embedded finite subject of person p (in situ). Distinguished from matrixFinite so that embedded-pro-drop asymmetries (some languages drop only embedded subjects) can be stated.

Equations

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

Instances For

def Phenomena.NullSubject.SubjectContext.controlled (p : Person) :

Subject of an obligatory-control clause (PRO position) of person p. The canonical locus for "does this language have overt PRO?".

Equations

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

Instances For

def Phenomena.NullSubject.SubjectContext.matrixExtracted (p : Person) :

Ā-extracted matrix finite subject of person p. The canonical locus for the anti-agreement effect (@cite{baier-2018}).

Equations

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

Instances For