Verb–complementizer compatibility

The hom between the Verb and Complementizer entry APIs: which clause-typers a predicate takes. One relation, lifted twice: a position takes a typer when their recorded axes — [Noo07]'s coding axis and the force axis — are Option.Compatible throughout and Option.Agrees somewhere; a frame or verb takes a typer when some position or frame does. All decidable. Non-clausal positions record no axes, so positive evidence already excludes them; the subject-requirement axis (Complement.Position.embeddedSubject?) is object-side and not matched: typers record no subject requirement.

Main definitions

• Complement.Position.Takes, Frame.Takes, Verb.takes — the relation and its lifts
• Verb.typers — the typers of a verb within an inventory

Main results

• Complement.Position.not_takes_of_blank, Complement.Position.blank_not_takes — matching needs positive evidence on both sides
• Frame.smallClause_not_takes — small clauses take no typer
• Frame.finiteClause_takes — the positive witness
• Frame.Takes.mono — monotone under frame extension

Consistency checks against Fragment data live in Studies (e.g. Bondarenko2022.hanaxa_typers).

def Complement.Position.Takes (p : Position) (z : Complementizer) : Prop

The position takes clause-typer z: every recorded axis compatible, some axis agreeing. Matching needs positive evidence, so a typer or position recording nothing — in particular any non-clausal position — takes nothing.

Equations

• p.Takes z = (p.coding?.Compatible z.coding ∧ p.force?.Compatible z.force ∧ (p.coding?.Agrees z.coding ∨ p.force?.Agrees z.force))

@[instance_reducible]

instance instDecidableTakes (p : Complement.Position) (z : Complementizer) : Decidable (p.Takes z)

Equations

• instDecidableTakes p z = instDecidableTakes._aux_1 p z

theorem Complement.Position.not_takes_of_blank {p : Position} {z : Complementizer} (hc : z.coding = none) (hf : z.force = none) : ¬p.Takes z

A typer recording neither axis takes nothing.

theorem Complement.Position.blank_not_takes {z : Complementizer} {e : Option Clause.EmbeddedSubject} : ¬(clausal none none e).Takes z

A position recording neither axis takes nothing: matching needs positive evidence.

def Frame.Takes (fr : Frame) (z : Complementizer) : Prop

The frame takes z: some position does.

Equations

• fr.Takes z = ∃ p ∈ fr, p.Takes z

@[instance_reducible]

instance instDecidableTakes_1 (fr : Frame) (z : Complementizer) : Decidable (fr.Takes z)

Equations

• instDecidableTakes_1 fr z = instDecidableTakes_1._aux_1 fr z

theorem Frame.Takes.mono {fr fr' : Frame} {z : Complementizer} (h : fr.Takes z) (hsub : fr ⊆ fr') : fr'.Takes z

Taking is monotone under frame extension.

theorem Frame.smallClause_not_takes (z : Complementizer) : ¬smallClause.Takes z

Small clauses take no clause-typer.

theorem Frame.finiteClause_takes {z : Complementizer} (hc : z.coding = some Complement.Coding.indicative) (hf : z.force = none ∨ z.force = some Mood.Illocutionary.declarative) : finiteClause.Takes z

An indicative typer with declarative or unrecorded force takes the finite-clause frame.

def Verb.takes (v : Verb) (z : Complementizer) : Prop

The verb takes z: some frame does.

Equations

• v.takes z = ∃ fr ∈ v.frames, fr.Takes z

@[instance_reducible]

instance instDecidableTakes_2 (v : Verb) (z : Complementizer) : Decidable (v.takes z)

Equations

• instDecidableTakes_2 v z = instDecidableTakes_2._aux_1 v z

def Verb.typers (v : Verb) (inv : List Complementizer) : List Complementizer

The typers of v within a language's complementizer inventory.

Equations

• v.typers inv = List.filter (fun (c : Complementizer) => decide (v.takes c)) inv