Complementizer

The lexical core of the complementizer (clause-typing morpheme) as a grammatical object, modeled on Syntax/Category/Pronoun/: its exponent as morphs plus the consensus clause-typing axes, each drawn from existing substrate. Per-language fragments instantiate it — free subordinators like that and oti, affixal clause-typers like Buryat -žA and Tigrinya zɨ-, grammaticalized say-roots like Buryat gɘ and Uyghur de.

Main declarations

• Complementizer — the general complementizer object
• Complementizer.Licenser — adnominal vs adverbal licensing category
• Complementizer.form — the surface form with boundary notation
• Complementizer.IsBound — affixal status, read off the morphs
• Complementizer.IsFinite — finiteness of the typed clause, read off the verb form
• Complementizer.toWord — the SCONJ word a free complementizer projects

Implementation notes

Framework-specific head assignments (a cartographic Force/Fin split, a ContP-exponence claim, an [n]-feature) are not fields; they live as Studies-local projections over these entries, and the schema carries no denotation (cf. Adjective's deferred degree semantics). Field conventions:

• morphs lists the exponent in surface order: a free word (that), a bound root that never surfaces bare (Buryat gɘ, Uyghur de), or the affixes of a prefix or suffix complex (Tigrinya kɛm-zɨ-). Attachment is read off the morphs' kinds rather than stored.
• force: only .declarative and .interrogative are attested on embedded-clause typers.
• licenser names the licensing projection, not the morphological host stem (which for a suffixal clause-typer is the verb it attaches to).
• factive records only a lexical factive presupposition carried by the morpheme itself (Greek pu); leave none when factivity tracks the verb or the construction — derived in Studies, never stored.

inductive Complementizer.Licenser : Type

Category of the adjacent projection licensing an affixal clause-typer: adnominal (Buryat -Aːša) vs adverbal (Buryat -žA).

• nominal : Licenser
• verbal : Licenser

@[instance_reducible]

instance Complementizer.instDecidableEqLicenser : DecidableEq Licenser

Equations

• Complementizer.instDecidableEqLicenser x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Complementizer.instFintypeLicenser : Fintype Licenser

Equations

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

@[instance_reducible]

instance Complementizer.instReprLicenser : Repr Licenser

Equations

• Complementizer.instReprLicenser = { reprPrec := Complementizer.instReprLicenser.repr }

def Complementizer.instReprLicenser.repr : Licenser → ℕ → Std.Format

Equations

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

structure Complementizer : Type

A complementizer: its exponent as morphs plus the consensus clause-typing axes.

• morphs : List Morphology.Morph

  The exponent, in surface order.

• script : Option String

  Native script form, when distinct.

• coding : Option Complement.Coding

  [noonan-2007] coding of the clause this morpheme types.

• force : Option Mood.Illocutionary

  Illocutionary force of the clause this morpheme types.

• verbForm : Option UD.VerbForm

  Verb form derived on the host (UD).

• licenser : Option Licenser

  Category of the adjacent licensing projection.

• factive : Option Bool

  Lexical factive presupposition.

@[instance_reducible]

instance instReprComplementizer : Repr Complementizer

Equations

• instReprComplementizer = { reprPrec := instReprComplementizer.repr }

def instReprComplementizer.repr : Complementizer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance instDecidableEqComplementizer : DecidableEq Complementizer

Equations

• instDecidableEqComplementizer = instDecidableEqComplementizer.decEq

def instDecidableEqComplementizer.decEq (x✝ x✝¹ : Complementizer) : Decidable (x✝ = x✝¹)

Equations

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

def Complementizer.form (c : Complementizer) : String

The surface form: the morphs' forms with their boundary notation.

Equations

• c.form = String.join (List.map toString c.morphs)

def Complementizer.IsBound (c : Complementizer) : Prop

Bound: no morph of the exponent is a free form.

Equations

• c.IsBound = ∀ m ∈ c.morphs, m.kind ≠ Morphology.Morph.Kind.free

@[instance_reducible]

instance Complementizer.instDecidablePredIsBound : DecidablePred IsBound

Equations

• c.instDecidablePredIsBound = id inferInstance

def Complementizer.IsFinite (c : Complementizer) : Prop

Finite: the clause the morpheme types has a finite verb form.

Equations

• c.IsFinite = (c.verbForm = some UD.VerbForm.Fin)

@[instance_reducible]

instance Complementizer.instDecidablePredIsFinite : DecidablePred IsFinite

Equations

• c.instDecidablePredIsFinite = Complementizer.instDecidablePredIsFinite._aux_1 c

def Complementizer.toWord (c : Complementizer) : Option Morphology.Word

The SCONJ word a free complementizer projects; none for bound clause-typers.

Equations

• c.toWord = match c.morphs with | [{ kind := Morphology.Morph.Kind.free, form := s }] => some { form := s, cat := UD.UPOS.SCONJ } | x => none