Verb–complementizer selection

The selection relation between the Verb and Complementizer entry APIs: which clause-typers a predicate takes. A complement position and a clause-typer each record a bundle of partial axis values (ArgumentFrame.Position.Axes) in the flat order, and a position takes a typer when the two bundles are consistent (Compat) and overlap (Overlap): some axis both record. One relation, lifted twice: a frame or verb takes a typer when some complement or frame does. All decidable. A typer records only the [Noo07] coding and the sentence types it types, so the relation lives on those two axes (takes_iff_coding_types): matching needs positive evidence on one of them, a non-clausal position takes nothing, and the subject-requirement axis is position-side and never matched.

Main definitions

• Complementizer.axes — the typer's bundle
• ArgumentFrame.Position.typedBy, ArgumentFrame.typedBy — the clausal position and the frame a typer types, given the subject requirement the predicate adds
• ArgumentFrame.Position.Takes, ArgumentFrame.Takes, Verb.Takes — the relation and its lifts
• Verb.typers — the typers of a verb within an inventory

Main results

• ArgumentFrame.Position.takes_iff — the relation axis by axis
• ArgumentFrame.Position.takes_iff_coding_types — the relation on the two axes a typer records
• Complementizer.compat_axes_iff, Complementizer.overlap_axes_iff — a bundle meets a typer's on the coding and types axes alone
• ArgumentFrame.Position.typedBy_takes_iff, ArgumentFrame.typedBy_takes_iff — the position or frame one typer types takes another exactly when the two bundles are consistent and overlap; typedBy_takes_self_iff for the typer itself
• ArgumentFrame.Position.not_takes_of_blank_left, ArgumentFrame.Position.not_takes_of_blank_right, ArgumentFrame.Position.not_takes_of_not_isClausal — matching needs positive evidence on both sides
• ArgumentFrame.Position.exists_takes_iff, Verb.not_takes_of_blank — a typer some position takes records a coding or a sentence type, and no verb takes one that records neither
• ArgumentFrame.Position.takes_of_le — the positive witness in general
• ArgumentFrame.Position.Takes.mono_of_compat, ArgumentFrame.Position.Takes.of_le_of_overlap — guarded monotonicity under refinement, in both directions
• ArgumentFrame.Position.Takes.isClausal, ArgumentFrame.Takes.hasClausal, Verb.Takes.takesClausal — taking a typer entails the clausal shape predicates
• ArgumentFrame.not_takes_smallClause — small clauses take no typer
• ArgumentFrame.finiteClause_takes — the positive witness
• ArgumentFrame.Takes.mono — monotone under complement extension
• Verb.mem_typers — membership in the typer list

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

References

• [Noo07]

def ArgumentFrame.Position.Overlap (f g : Axes) : Prop

Two bundles overlap when some axis is recorded on both.

Equations

• ArgumentFrame.Position.Overlap f g = ∃ (a : ArgumentFrame.Position.Axis), f a ≠ ⊥ ∧ g a ≠ ⊥

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableOverlap (f g : Axes) : Decidable (Overlap f g)

Equations

• ArgumentFrame.Position.instDecidableOverlap f g = { decide := decide (∃ a ∈ Finset.univ, (fun (_a : ArgumentFrame.Position.Axis) => f _a ≠ ⊥ ∧ g _a ≠ ⊥) a), reflects_decide := ⋯ }

theorem ArgumentFrame.Position.overlap_self_iff {f : Axes} : Overlap f f ↔ f ≠ ⊥

A bundle overlaps itself exactly when it records something.

def Complementizer.axes (z : Complementizer) : ArgumentFrame.Position.Axes

The axes a clause-typer records: its coding and the sentence types it types; the other axes are a complement position's alone.

Equations

• z.axes ArgumentFrame.Position.Axis.coding = z.coding
• z.axes ArgumentFrame.Position.Axis.types = z.types
• z.axes ArgumentFrame.Position.Axis.embeddedSubject = ⊥
• z.axes ArgumentFrame.Position.Axis.relation = ⊥
• z.axes ArgumentFrame.Position.Axis.adposition = ⊥
• z.axes ArgumentFrame.Position.Axis.interp = ⊥

theorem Complementizer.compat_axes_iff {z : Complementizer} (f : ArgumentFrame.Position.Axes) : Compat f z.axes ↔ Compat (f ArgumentFrame.Position.Axis.coding) z.coding ∧ Compat (f ArgumentFrame.Position.Axis.types) z.types

A bundle is consistent with a typer's exactly on the coding and types axes.

theorem Complementizer.overlap_axes_iff {z : Complementizer} (f : ArgumentFrame.Position.Axes) : ArgumentFrame.Position.Overlap f z.axes ↔ f ArgumentFrame.Position.Axis.coding ≠ ⊥ ∧ z.coding ≠ none ∨ f ArgumentFrame.Position.Axis.types ≠ ⊥ ∧ z.types ≠ ⊥

A bundle overlaps a typer's exactly on the coding and types axes.

def ArgumentFrame.Position.typedBy (z : Complementizer) (s : Option Clause.EmbeddedSubject := none) : Position

The clausal position z types carries z's coding and sentence types, with the subject requirement s the selecting predicate adds.

Equations

• ArgumentFrame.Position.typedBy z s = ArgumentFrame.Position.clausal z.coding z.types s

@[simp]

theorem ArgumentFrame.Position.kind_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).kind = Kind.clausal

@[simp]

theorem ArgumentFrame.Position.coding?_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).coding? = z.coding

@[simp]

theorem ArgumentFrame.Position.types_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).types = z.types

@[simp]

theorem ArgumentFrame.Position.embeddedSubject?_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).embeddedSubject? = s

@[simp]

theorem ArgumentFrame.Position.relation?_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).relation? = none

@[simp]

theorem ArgumentFrame.Position.adposition?_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).adposition? = none

@[simp]

theorem ArgumentFrame.Position.interp?_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).interp? = none

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

The position takes clause-typer z: the two bundles are consistent and overlap, some axis recorded on both sides. Matching needs positive evidence, so a typer or position recording nothing — in particular any non-clausal position — takes nothing.

Equations

• p.Takes z = (Compat p.axes z.axes ∧ ArgumentFrame.Position.Overlap p.axes z.axes)

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableTakes {p : Position} {z : Complementizer} : Decidable (p.Takes z)

Equations

• ArgumentFrame.Position.instDecidableTakes = { decide := decide (Compat p.axes z.axes) && decide (ArgumentFrame.Position.Overlap p.axes z.axes), reflects_decide := ⋯ }

theorem ArgumentFrame.Position.takes_iff {p : Position} {z : Complementizer} : p.Takes z ↔ (∀ (a : Axis), Compat (p.axes a) (z.axes a)) ∧ ∃ (a : Axis), p.axes a ≠ ⊥ ∧ z.axes a ≠ ⊥

Axis by axis, every axis is consistent and some axis is recorded on both sides.

theorem ArgumentFrame.Position.takes_iff_coding_types {p : Position} {z : Complementizer} : p.Takes z ↔ (Compat (p.axes Axis.coding) z.coding ∧ Compat (p.axes Axis.types) z.types) ∧ (p.axes Axis.coding ≠ ⊥ ∧ z.coding ≠ none ∨ p.axes Axis.types ≠ ⊥ ∧ z.types ≠ ⊥)

On the two axes a typer records, coding and types are consistent and one of them is recorded on both sides.

theorem ArgumentFrame.Position.typedBy_takes_iff {z z' : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).Takes z' ↔ Compat z.axes z'.axes ∧ Overlap z.axes z'.axes

The position z types takes z' exactly when the two typers' bundles are consistent and overlap; the subject requirement plays no part.

theorem ArgumentFrame.Position.typedBy_takes_self_iff {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).Takes z ↔ z.axes ≠ ⊥

The position z types takes z itself exactly when z records something; the ← direction is takes_of_le.

theorem ArgumentFrame.Position.not_takes_of_blank_left {p : Position} {z : Complementizer} (hc : p.coding? = none) (ht : p.types = ⊥) : ¬p.Takes z

A position recording neither shared axis takes nothing.

theorem ArgumentFrame.Position.not_takes_of_blank_right {p : Position} {z : Complementizer} (hc : z.coding = none) (ht : z.types = ⊥) : ¬p.Takes z

A typer recording neither axis takes nothing.

theorem ArgumentFrame.Position.not_takes_of_not_isClausal {p : Position} {z : Complementizer} (h : ¬p.IsClausal) : ¬p.Takes z

A non-clausal position takes nothing: it records no axis a typer does.

theorem ArgumentFrame.Position.Takes.isClausal {p : Position} {z : Complementizer} (h : p.Takes z) : p.IsClausal

A position taking a typer is clausal.

theorem ArgumentFrame.Position.exists_takes_iff {z : Complementizer} : (∃ (p : Position), p.Takes z) ↔ z.coding ≠ none ∨ z.types ≠ ⊥

Some position takes a typer exactly when the typer records a coding or a sentence type.

theorem ArgumentFrame.Position.takes_of_le {p : Position} {z : Complementizer} (h : z.axes ≤ p.axes) (hz : z.axes ≠ ⊥) : p.Takes z

A typer whose bundle lies below the position's, and records something, is taken: the positive witness in general.

theorem ArgumentFrame.Position.Takes.mono_of_compat {p q : Position} {z : Complementizer} (hpq : p ≤ q) (hc : Compat q.axes z.axes) (h : p.Takes z) : q.Takes z

Refining a position keeps a typer it takes, as long as the refinement stays consistent with the typer.

theorem ArgumentFrame.Position.Takes.of_le_of_overlap {p q : Position} {z : Complementizer} (hpq : p ≤ q) (ho : Overlap p.axes z.axes) (h : q.Takes z) : p.Takes z

Coarsening a position keeps a typer it takes, as long as the coarsening still overlaps the typer.

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

The frame takes z when some complement does.

Equations

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

@[instance_reducible]

instance ArgumentFrame.instDecidableTakes {fr : ArgumentFrame} {z : Complementizer} : Decidable (fr.Takes z)

Equations

• ArgumentFrame.instDecidableTakes = ArgumentFrame.instDecidableTakes._aux_1

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

Taking is monotone under complement extension.

theorem ArgumentFrame.Takes.hasClausal {fr : ArgumentFrame} {z : Complementizer} (h : fr.Takes z) : fr.HasClausal

A frame taking a typer has a clausal complement.

theorem ArgumentFrame.not_takes_of_blank {fr : ArgumentFrame} {z : Complementizer} (hc : z.coding = none) (ht : z.types = ⊥) : ¬fr.Takes z

No frame takes a typer recording neither axis.

theorem ArgumentFrame.not_takes_smallClause (z : Complementizer) : ¬smallClause.Takes z

Small clauses take no clause-typer.

theorem ArgumentFrame.finiteClause_takes {z : Complementizer} (hc : z.coding = some Complement.Coding.indicative) (ht : z.types = ⊥ ∨ z.types = Clause.Selection.only Clause.SentenceType.declarative) : finiteClause.Takes z

An indicative typer typing declaratives or nothing recorded takes the finite-clause frame.

The frame a typer types

def ArgumentFrame.typedBy (z : Complementizer) (s : Option Clause.EmbeddedSubject := none) : ArgumentFrame

The frame whose one complement is the clause z types, with the subject requirement s: the frame a fragment derives from its complementizer entry rather than retyping the typer's axes.

Equations

• ArgumentFrame.typedBy z s = { complements := [ArgumentFrame.Position.typedBy z s] }

@[simp]

theorem ArgumentFrame.complements_typedBy {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).complements = [Position.typedBy z s]

theorem ArgumentFrame.typedBy_takes_iff {z z' : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).Takes z' ↔ Compat z.axes z'.axes ∧ Position.Overlap z.axes z'.axes

The frame z types takes z' exactly when the two typers' bundles are consistent and overlap.

theorem ArgumentFrame.typedBy_takes_self_iff {z : Complementizer} {s : Option Clause.EmbeddedSubject} : (typedBy z s).Takes z ↔ z.axes ≠ ⊥

The frame z types takes z exactly when z records something.

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

The verb takes z when some frame does.

Equations

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

@[instance_reducible]

instance Verb.instDecidableTakes {v : Verb} {z : Complementizer} : Decidable (v.Takes z)

Equations

• Verb.instDecidableTakes = Verb.instDecidableTakes._aux_1

theorem Verb.Takes.takesClausal {v : Verb} {z : Complementizer} (h : v.Takes z) : v.TakesClausal

A verb taking a typer takes a clausal complement.

theorem Verb.not_takes_of_blank {v : Verb} {z : Complementizer} (hc : z.coding = none) (ht : z.types = ⊥) : ¬v.Takes z

No verb takes a typer recording neither axis, as a converb suffix records none.

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 (x : Complementizer) => decide (v.Takes x)) inv

@[simp]

theorem Verb.mem_typers {v : Verb} {z : Complementizer} {inv : List Complementizer} : z ∈ v.typers inv ↔ z ∈ inv ∧ v.Takes z