Complementizer

The lexical core of the complementizer (clause-typing morpheme) as a grammatical object, modeled on Syntax/Pronoun/: surface form 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.IsBound — affixal status, derived from position
• 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:

• position = none: unrecorded, or a bound root with no fixed attachment of its own (Buryat gɘ surfaces only suffixed).
• clauseForm: only .declarative and .embeddedQuestion are sensible values for an embedded-clause typer.
• licenser names the licensing projection, not the morphological host stem (which for a postfixed clause-typer is the verb it attaches to).
• agrees: φ-agreement with a clause-internal argument (Tigrinya kɨ- and ʔay-…-n; West Germanic complementizer agreement).
• factive records only a lexical factive presupposition carried by the morpheme itself (Greek pu, Tigrinya kəmzi-); 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

@[implicit_reducible]

instance Complementizer.instDecidableEqLicenser : DecidableEq Licenser

Equations

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

@[implicit_reducible]

instance Complementizer.instFintypeLicenser : Fintype Licenser

Equations

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

@[implicit_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: surface form plus the consensus clause-typing axes.

• form : String

  Surface form (romanization; affixes hyphenated).

• script : Option String

  Native script form, when distinct.

• position : Option Morphology.FormativePosition

  Morphological attachment.

• noonanType : Option NoonanCompType

  [Noo07] type of the clause this morpheme types.

• clauseForm : Option Features.ClauseForm

  Surface clause form typed.

• verbForm : Option UD.VerbForm

  Verb form derived on the host (UD).

• licenser : Option Licenser

  Category of the adjacent licensing projection.

• agrees : Option Bool

  Carries φ-agreement with a clause-internal argument?

• factive : Option Bool

  Lexical factive presupposition.

@[implicit_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.

def instBEqComplementizer.beq : Complementizer → Complementizer → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqComplementizer.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqComplementizer : BEq Complementizer

Equations

• instBEqComplementizer = { beq := instBEqComplementizer.beq }

@[implicit_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.IsBound (c : Complementizer) : Prop

Bound (affixal): recorded attachment other than .detached.

Equations

• c.IsBound = (c.position ≠ none ∧ c.position ≠ some Morphology.FormativePosition.detached)

@[implicit_reducible]

instance Complementizer.instDecidablePredIsBound : DecidablePred IsBound

Equations

• c.instDecidablePredIsBound = id inferInstance

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

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

Equations

• c.toWord = if c.position = some Morphology.FormativePosition.detached then some { form := c.form, cat := UD.UPOS.SCONJ } else none