Argument frames

A predicate's argument frame is its external argument, if any, and its complement positions in order. A position is nominal, adpositional, clausal, implicit or expletive, and carries the axes the predicate selects for: the type of case, in Blake's sense, and the adposition of an adpositional position, Noonan's coding, the sentence types and the subject requirement of a clausal one, and the interpretation of an implicit one. Positions and frames are partially ordered by refinement, so a schematic frame lies below every frame instantiating it.

Main definitions

• ImplicitInterp — the interpretation of an unexpressed argument
• ArgumentFrame.Position — one argument position, with its selectional axes
• ArgumentFrame.Position.Kind, Position.kind, IsNominal, IsAdpositional, IsClausal, IsExpressed — the category of a position
• ArgumentFrame.Position.Axis, Axes, Position.axes — the axes a position records, as a bundle of partial values in the flat order
• ArgumentFrame — external argument and complements, with the refinement order
• ArgumentFrame.Slot, ArgumentFrame.get?, ArgumentFrame.slots, ArgumentFrame.coreSlots, ArgumentFrame.valency, ArgumentFrame.IsTransitive, ArgumentFrame.argumentRole — the argument slots of a frame and their comparative S/A/P/R/T classification
• ArgumentFrame.IsIntransitive, ArgumentFrame.HasNominal, ArgumentFrame.HasAdpositional, ArgumentFrame.HasClausal, ArgumentFrame.HasFinite, ArgumentFrame.HasImplicit — shape predicates
• ArgumentFrame.leaveImplicit — a frame with one complement left unexpressed
• ArgumentFrame.intransitive, ArgumentFrame.np, ArgumentFrame.finiteClause, … — smart constructors

Main results

• ArgumentFrame.Position.le_def, ArgumentFrame.le_def — the refinement orders

Implementation notes

A position refines another within its kind: p ≤ q when the two are of one kind and every axis p records, q records with the same value. A frame's order fixes the external argument and refines the complements pointwise (List.Forall₂). A frame is the surface clause, its external argument the subject position, none for a predicate that selects no subject, as an impersonal passive and a raising predicate; an unaccusative verb's sole argument is its subject, unaccusativity being read off the verb's diatheses (Verb.IsUnaccusative). The comparative role labels S, A, P, R and T are read off the frame's coding (ArgumentFrame.argumentRole), never stored. The interpretations of an implicit argument are Fillmore's and Bruening's, with Levin's understood-object alternations. Complement-taking is cross-categorial, Noonan's complement-taking predicates including adjectives and nouns, so ArgumentFrame is not under Verb. Frame-conditioned readings (attitude, opacity, control) live on Verb.Reading (Syntax/Category/Verb/Defs.lean); the selection relation between frames and clause-typers (Verb.Takes) in Syntax/Category/Verb/ArgumentFrame/Takes.lean. Deal's CP-external shell inventory lives with its consumer in Studies/Deal2026.lean.

References

• [Bla01]
• [Bru21]
• [Com78]
• [Dea26]
• [Fil86]
• [Lev93]
• [Noo07]

inductive ImplicitInterp : Type

The interpretation of an unexpressed argument.

• indef : ImplicitInterp

  An existentially bound argument, an unspecified someone or something.

• def : ImplicitInterp

  A pragmatically recoverable definite.

• reflexive : ImplicitInterp

  Understood as the subject itself (Mary dressed).

• reciprocal : ImplicitInterp

  Understood as the subject's members, each of the other (Anne and Cathy met).

• bodyPart : ImplicitInterp

  Understood as a body part of the subject (Mary waved).

@[instance_reducible]

instance instDecidableEqImplicitInterp : DecidableEq ImplicitInterp

Equations

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

@[instance_reducible]

instance instFintypeImplicitInterp : Fintype ImplicitInterp

Equations

• instFintypeImplicitInterp = { elems := { val := ↑ImplicitInterp.enumList, nodup := ImplicitInterp.enumList_nodup }, complete := instFintypeImplicitInterp._proof_1 }

def instReprImplicitInterp.repr : ImplicitInterp → ℕ → Std.Format

Equations

• instReprImplicitInterp.repr ImplicitInterp.indef prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.indef")).group prec✝
• instReprImplicitInterp.repr ImplicitInterp.def prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.def")).group prec✝
• instReprImplicitInterp.repr ImplicitInterp.reflexive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.reflexive")).group prec✝
• instReprImplicitInterp.repr ImplicitInterp.reciprocal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.reciprocal")).group prec✝
• instReprImplicitInterp.repr ImplicitInterp.bodyPart prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ImplicitInterp.bodyPart")).group prec✝

@[instance_reducible]

instance instReprImplicitInterp : Repr ImplicitInterp

Equations

• instReprImplicitInterp = { reprPrec := instReprImplicitInterp.repr }

inductive ArgumentFrame.Position : Type

An argument position of a frame is nominal; adpositional, recording the type of case marked and the adposition selected; clausal, recording the coding, the sentence types and the subject requirement selected; implicit, an unexpressed argument with its interpretation; or expletive. Every axis is optional, and none or ⊥ is unselective.

• nominal : Position
• adpositional (relation : Option Case.Kind := none) (adposition : Option Adposition := none) : Position
• clausal (coding : Option Complement.Coding := none) (types : Clause.Selection := ⊥) (embeddedSubject : Option Clause.EmbeddedSubject := none) : Position
• implicit (interp : Option ImplicitInterp := none) : Position
• expletive : Position

@[instance_reducible]

instance ArgumentFrame.instDecidableEqPosition : DecidableEq Position

Equations

• ArgumentFrame.instDecidableEqPosition = ArgumentFrame.instDecidableEqPosition.decEq

def ArgumentFrame.instDecidableEqPosition.decEq (x✝ x✝¹ : Position) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.nominal ArgumentFrame.Position.nominal = isTrue ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.nominal (ArgumentFrame.Position.adpositional relation adposition) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.nominal (ArgumentFrame.Position.clausal coding types embeddedSubject) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.nominal (ArgumentFrame.Position.implicit interp) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.nominal ArgumentFrame.Position.expletive = isFalse ArgumentFrame.instDecidableEqPosition.decEq._proof_6
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.adpositional relation adposition) ArgumentFrame.Position.nominal = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.adpositional relation adposition) (ArgumentFrame.Position.clausal coding types embeddedSubject) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.adpositional relation adposition) (ArgumentFrame.Position.implicit interp) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.adpositional relation adposition) ArgumentFrame.Position.expletive = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.clausal coding types embeddedSubject) ArgumentFrame.Position.nominal = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.clausal coding types embeddedSubject) (ArgumentFrame.Position.adpositional relation adposition) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.clausal coding types embeddedSubject) (ArgumentFrame.Position.implicit interp) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.clausal coding types embeddedSubject) ArgumentFrame.Position.expletive = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.implicit interp) ArgumentFrame.Position.nominal = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.implicit interp) (ArgumentFrame.Position.adpositional relation adposition) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.implicit interp) (ArgumentFrame.Position.clausal coding types embeddedSubject) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.implicit a) (ArgumentFrame.Position.implicit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq (ArgumentFrame.Position.implicit interp) ArgumentFrame.Position.expletive = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.expletive ArgumentFrame.Position.nominal = isFalse ArgumentFrame.instDecidableEqPosition.decEq._proof_25
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.expletive (ArgumentFrame.Position.adpositional relation adposition) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.expletive (ArgumentFrame.Position.clausal coding types embeddedSubject) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.expletive (ArgumentFrame.Position.implicit interp) = isFalse ⋯
• ArgumentFrame.instDecidableEqPosition.decEq ArgumentFrame.Position.expletive ArgumentFrame.Position.expletive = isTrue ⋯

def ArgumentFrame.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentFrame.instReprPosition : Repr Position

Equations

• ArgumentFrame.instReprPosition = { reprPrec := ArgumentFrame.instReprPosition.repr }

def ArgumentFrame.Position.adposition (p : Adposition) : Position

The adpositional position selecting p, with the type of case p marks when it marks one type.

Equations

• ArgumentFrame.Position.adposition p = ArgumentFrame.Position.adpositional p.kind? (some p)

def ArgumentFrame.Position.coding? : Position → Option Complement.Coding

The position's recorded coding, if clausal.

Equations

• (ArgumentFrame.Position.clausal c types embeddedSubject).coding? = c
• x✝.coding? = none

def ArgumentFrame.Position.types : Position → Clause.Selection

The sentence types the position selects, if clausal; nothing otherwise.

Equations

• (ArgumentFrame.Position.clausal c types embeddedSubject).types = types
• x✝.types = ⊥

def ArgumentFrame.Position.embeddedSubject? : Position → Option Clause.EmbeddedSubject

The position's recorded subject requirement, if clausal.

Equations

• (ArgumentFrame.Position.clausal c types embeddedSubject).embeddedSubject? = embeddedSubject
• x✝.embeddedSubject? = none

def ArgumentFrame.Position.relation? : Position → Option Case.Kind

The position's recorded relation, if adpositional.

Equations

• (ArgumentFrame.Position.adpositional r adposition).relation? = r
• x✝.relation? = none

def ArgumentFrame.Position.adposition? : Position → Option Adposition

The position's recorded adposition, if adpositional.

Equations

• (ArgumentFrame.Position.adpositional r adposition).adposition? = adposition
• x✝.adposition? = none

def ArgumentFrame.Position.interp? : Position → Option ImplicitInterp

The position's recorded interpretation, if implicit.

Equations

• (ArgumentFrame.Position.implicit i).interp? = i
• x✝.interp? = none

Kind

inductive ArgumentFrame.Position.Kind : Type

The category of a position.

• nominal : Kind
• adpositional : Kind
• clausal : Kind
• implicit : Kind
• expletive : Kind

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableEqKind : DecidableEq Kind

Equations

• ArgumentFrame.Position.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ArgumentFrame.Position.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentFrame.Position.instReprKind : Repr Kind

Equations

• ArgumentFrame.Position.instReprKind = { reprPrec := ArgumentFrame.Position.instReprKind.repr }

def ArgumentFrame.Position.kind : Position → Kind

The category of the position.

Equations

• ArgumentFrame.Position.nominal.kind = ArgumentFrame.Position.Kind.nominal
• (ArgumentFrame.Position.adpositional relation adposition).kind = ArgumentFrame.Position.Kind.adpositional
• (ArgumentFrame.Position.clausal coding types embeddedSubject).kind = ArgumentFrame.Position.Kind.clausal
• (ArgumentFrame.Position.implicit interp).kind = ArgumentFrame.Position.Kind.implicit
• ArgumentFrame.Position.expletive.kind = ArgumentFrame.Position.Kind.expletive

@[reducible, inline]

abbrev ArgumentFrame.Position.IsNominal (p : Position) : Prop

The position is nominal, the core case.

Equations

• p.IsNominal = (p.kind = ArgumentFrame.Position.Kind.nominal)

@[reducible, inline]

abbrev ArgumentFrame.Position.IsAdpositional (p : Position) : Prop

The position is adpositional.

Equations

• p.IsAdpositional = (p.kind = ArgumentFrame.Position.Kind.adpositional)

@[reducible, inline]

abbrev ArgumentFrame.Position.IsClausal (p : Position) : Prop

The position is clausal.

Equations

• p.IsClausal = (p.kind = ArgumentFrame.Position.Kind.clausal)

@[reducible, inline]

abbrev ArgumentFrame.Position.IsExpressed (p : Position) : Prop

The position is expressed when it is nominal, adpositional or clausal.

Equations

• p.IsExpressed = (p.IsNominal ∨ p.IsAdpositional ∨ p.IsClausal)

def ArgumentFrame.Position.IsFinite (p : Position) : Prop

The position is a finite clause when its coding is finite.

Equations

• p.IsFinite = ∃ c ∈ p.coding?, c.IsFinite

@[instance_reducible]

instance ArgumentFrame.Position.instDecidablePredIsFinite : DecidablePred IsFinite

Equations

• p.instDecidablePredIsFinite = ArgumentFrame.Position.instDecidablePredIsFinite._aux_1 p

Axes and the refinement order

inductive ArgumentFrame.Position.Axis : Type

The selectional axes a position records. A clausal position and a clause-typer share coding and types (Complementizer.axes).

• coding : Axis
• types : Axis
• embeddedSubject : Axis
• relation : Axis
• adposition : Axis
• interp : Axis

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableEqAxis : DecidableEq Axis

Equations

• ArgumentFrame.Position.instDecidableEqAxis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ArgumentFrame.Position.instFintypeAxis : Fintype Axis

Equations

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

def ArgumentFrame.Position.instReprAxis.repr : Axis → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentFrame.Position.instReprAxis : Repr Axis

Equations

• ArgumentFrame.Position.instReprAxis = { reprPrec := ArgumentFrame.Position.instReprAxis.repr }

def ArgumentFrame.Position.Axis.Carrier : Axis → Type

The carrier of an axis is a flat slot over the values of an enumerated axis, and a selection of sentence types for the types axis.

Equations

• ArgumentFrame.Position.Axis.coding.Carrier = Flat Complement.Coding
• ArgumentFrame.Position.Axis.types.Carrier = Clause.Selection
• ArgumentFrame.Position.Axis.embeddedSubject.Carrier = Flat Clause.EmbeddedSubject
• ArgumentFrame.Position.Axis.relation.Carrier = Flat Case.Kind
• ArgumentFrame.Position.Axis.adposition.Carrier = Flat Adposition
• ArgumentFrame.Position.Axis.interp.Carrier = Flat ImplicitInterp

@[instance_reducible]

instance ArgumentFrame.Position.instPartialOrderCarrier (a : Axis) : PartialOrder a.Carrier

Equations

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

@[instance_reducible]

instance ArgumentFrame.Position.instOrderBotCarrier (a : Axis) : OrderBot a.Carrier

Equations

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

@[instance_reducible]

instance ArgumentFrame.Position.instPartialUnifyCarrier (a : Axis) : PartialUnify a.Carrier

Equations

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

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableEqCarrier (a : Axis) : DecidableEq a.Carrier

Equations

• ArgumentFrame.Position.instDecidableEqCarrier ArgumentFrame.Position.Axis.coding = ArgumentFrame.Position.instDecidableEqCarrier._aux_1
• ArgumentFrame.Position.instDecidableEqCarrier ArgumentFrame.Position.Axis.types = ArgumentFrame.Position.instDecidableEqCarrier._aux_3
• ArgumentFrame.Position.instDecidableEqCarrier ArgumentFrame.Position.Axis.embeddedSubject = ArgumentFrame.Position.instDecidableEqCarrier._aux_5
• ArgumentFrame.Position.instDecidableEqCarrier ArgumentFrame.Position.Axis.relation = ArgumentFrame.Position.instDecidableEqCarrier._aux_7
• ArgumentFrame.Position.instDecidableEqCarrier ArgumentFrame.Position.Axis.adposition = ArgumentFrame.Position.instDecidableEqCarrier._aux_9
• ArgumentFrame.Position.instDecidableEqCarrier ArgumentFrame.Position.Axis.interp = ArgumentFrame.Position.instDecidableEqCarrier._aux_11

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableLECarrier (a : Axis) : DecidableLE a.Carrier

Equations

• ArgumentFrame.Position.instDecidableLECarrier ArgumentFrame.Position.Axis.coding = ArgumentFrame.Position.instDecidableLECarrier._aux_1
• ArgumentFrame.Position.instDecidableLECarrier ArgumentFrame.Position.Axis.types = ArgumentFrame.Position.instDecidableLECarrier._aux_3
• ArgumentFrame.Position.instDecidableLECarrier ArgumentFrame.Position.Axis.embeddedSubject = ArgumentFrame.Position.instDecidableLECarrier._aux_5
• ArgumentFrame.Position.instDecidableLECarrier ArgumentFrame.Position.Axis.relation = ArgumentFrame.Position.instDecidableLECarrier._aux_7
• ArgumentFrame.Position.instDecidableLECarrier ArgumentFrame.Position.Axis.adposition = ArgumentFrame.Position.instDecidableLECarrier._aux_9
• ArgumentFrame.Position.instDecidableLECarrier ArgumentFrame.Position.Axis.interp = ArgumentFrame.Position.instDecidableLECarrier._aux_11

@[reducible, inline]

abbrev ArgumentFrame.Position.Axes : Type

A bundle of partial axis values, ordered pointwise by extension, so that unification is PartialUnify.unify and consistency is Compat.

Equations

• ArgumentFrame.Position.Axes = ((a : ArgumentFrame.Position.Axis) → a.Carrier)

def ArgumentFrame.Position.axes (p : Position) : Axes

The axes the position records.

Equations

• p.axes ArgumentFrame.Position.Axis.coding = p.coding?
• p.axes ArgumentFrame.Position.Axis.types = p.types
• p.axes ArgumentFrame.Position.Axis.embeddedSubject = p.embeddedSubject?
• p.axes ArgumentFrame.Position.Axis.relation = p.relation?
• p.axes ArgumentFrame.Position.Axis.adposition = p.adposition?
• p.axes ArgumentFrame.Position.Axis.interp = p.interp?

theorem ArgumentFrame.Position.eq_of_kind_eq_of_axes_eq {p q : Position} (hk : p.kind = q.kind) (ha : p.axes = q.axes) : p = q

A position is its kind and its axes.

@[instance_reducible]

instance ArgumentFrame.Position.instPartialOrder : PartialOrder Position

A position refines another, p ≤ q, when the two are of one kind and every axis p records, q records with the same value.

Equations

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

theorem ArgumentFrame.Position.le_def {p q : Position} : p ≤ q ↔ p.kind = q.kind ∧ p.axes ≤ q.axes

@[instance_reducible]

instance ArgumentFrame.Position.instDecidableLE : DecidableLE Position

Equations

• p.instDecidableLE q = { decide := decide (p.kind = q.kind) && decide (∀ (a : ArgumentFrame.Position.Axis), p.axes a ≤ q.axes a), reflects_decide := ⋯ }

structure ArgumentFrame : Type

An argument frame is the external argument, if any, and the complement positions in order.

• external : Option Position

  The external argument; none for an unaccusative or impersonal frame.

• complements : List Position

  The complement positions in order.

theorem ArgumentFrame.ext_iff {x y : ArgumentFrame} : x = y ↔ x.external = y.external ∧ x.complements = y.complements

theorem ArgumentFrame.ext {x y : ArgumentFrame} (external : x.external = y.external) (complements : x.complements = y.complements) : x = y

def instDecidableEqArgumentFrame.decEq (x✝ x✝¹ : ArgumentFrame) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqArgumentFrame : DecidableEq ArgumentFrame

Equations

• instDecidableEqArgumentFrame = instDecidableEqArgumentFrame.decEq

@[instance_reducible]

instance instReprArgumentFrame : Repr ArgumentFrame

Equations

• instReprArgumentFrame = { reprPrec := instReprArgumentFrame.repr }

def instReprArgumentFrame.repr : ArgumentFrame → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentFrame.instPartialOrder : PartialOrder ArgumentFrame

A frame refines another when it has the same external argument and complements refined pointwise.

Equations

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

theorem ArgumentFrame.le_def {f g : ArgumentFrame} : f ≤ g ↔ f.external = g.external ∧ List.Forall₂ (fun (x1 x2 : Position) => x1 ≤ x2) f.complements g.complements

@[instance_reducible]

instance ArgumentFrame.instDecidableLE : DecidableLE ArgumentFrame

Equations

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

Slots

inductive ArgumentFrame.Slot : Type

An argument slot of a frame is the external argument or the i-th complement.

• external : Slot
• complement (i : ℕ) : Slot

@[instance_reducible]

instance ArgumentFrame.instDecidableEqSlot : DecidableEq Slot

Equations

• ArgumentFrame.instDecidableEqSlot = ArgumentFrame.instDecidableEqSlot.decEq

def ArgumentFrame.instDecidableEqSlot.decEq (x✝ x✝¹ : Slot) : Decidable (x✝ = x✝¹)

Equations

• ArgumentFrame.instDecidableEqSlot.decEq ArgumentFrame.Slot.external ArgumentFrame.Slot.external = isTrue ⋯
• ArgumentFrame.instDecidableEqSlot.decEq ArgumentFrame.Slot.external (ArgumentFrame.Slot.complement i) = isFalse ⋯
• ArgumentFrame.instDecidableEqSlot.decEq (ArgumentFrame.Slot.complement i) ArgumentFrame.Slot.external = isFalse ⋯
• ArgumentFrame.instDecidableEqSlot.decEq (ArgumentFrame.Slot.complement a) (ArgumentFrame.Slot.complement b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def ArgumentFrame.instReprSlot.repr : Slot → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentFrame.instReprSlot : Repr Slot

Equations

• ArgumentFrame.instReprSlot = { reprPrec := ArgumentFrame.instReprSlot.repr }

def ArgumentFrame.get? (fr : ArgumentFrame) : Slot → Option Position

The position at a slot.

Equations

• fr.get? ArgumentFrame.Slot.external = fr.external
• fr.get? (ArgumentFrame.Slot.complement i) = fr.complements[i]?

def ArgumentFrame.slots (fr : ArgumentFrame) : List Slot

The filled slots, external first.

Equations

• fr.slots = (Option.map (fun (x : ArgumentFrame.Position) => ArgumentFrame.Slot.external) fr.external).toList ++ List.map ArgumentFrame.Slot.complement (List.range fr.complements.length)

def ArgumentFrame.coreSlots (fr : ArgumentFrame) : List Slot

The core argument slots are those realized as nominals.

Equations

• fr.coreSlots = List.filter (fun (s : ArgumentFrame.Slot) => Option.any (fun (p : ArgumentFrame.Position) => decide p.IsNominal) (fr.get? s)) fr.slots

def ArgumentFrame.valency (fr : ArgumentFrame) : ℕ

The number of core arguments.

Equations

• fr.valency = fr.coreSlots.length

def ArgumentFrame.IsTransitive (fr : ArgumentFrame) : Prop

A frame is transitive when it has two or more core arguments.

Equations

• fr.IsTransitive = (2 ≤ fr.valency)

@[instance_reducible]

instance ArgumentFrame.instDecidableIsTransitive (fr : ArgumentFrame) : Decidable fr.IsTransitive

Equations

• fr.instDecidableIsTransitive = { decide := Nat.ble 2 fr.valency, reflects_decide := ⋯ }

def ArgumentFrame.coreObjects (fr : ArgumentFrame) : List Slot

The core objects are the core complements.

Equations

• fr.coreObjects = List.filter (fun (x : ArgumentFrame.Slot) => x != ArgumentFrame.Slot.external) fr.coreSlots

def ArgumentFrame.argumentRole (fr : ArgumentFrame) : Slot → Option ArgumentRole

The comparative argument role of a core slot is read off its coding. A nominal subject is S without a core object and A with one, a sole core object is P, and of two core objects the first is R and the second T.

Equations

• One or more equations did not get rendered due to their size.
• fr.argumentRole ArgumentFrame.Slot.external = if ArgumentFrame.Slot.external ∈ fr.coreSlots then some (if fr.coreObjects = [] then ArgumentRole.S else ArgumentRole.A) else none

def ArgumentFrame.objectSlot? (fr : ArgumentFrame) : Option Slot

The slot object entailments sit on is the last core object, the sole object of a monotransitive and the second object of a double-object frame.

Equations

• fr.objectSlot? = fr.coreObjects.getLast?

Shape predicates

def ArgumentFrame.IsIntransitive (fr : ArgumentFrame) : Prop

The frame has no complement.

Equations

• fr.IsIntransitive = (fr.complements = [])

@[instance_reducible]

instance ArgumentFrame.instDecidableIsIntransitive (fr : ArgumentFrame) : Decidable fr.IsIntransitive

Equations

• fr.instDecidableIsIntransitive = ArgumentFrame.instDecidableIsIntransitive._aux_1 fr

def ArgumentFrame.HasNominal (fr : ArgumentFrame) : Prop

Some complement of the frame is nominal.

Equations

• fr.HasNominal = ∃ p ∈ fr.complements, p.IsNominal

@[instance_reducible]

instance ArgumentFrame.instDecidableHasNominal (fr : ArgumentFrame) : Decidable fr.HasNominal

Equations

• fr.instDecidableHasNominal = ArgumentFrame.instDecidableHasNominal._aux_1 fr

def ArgumentFrame.HasAdpositional (fr : ArgumentFrame) : Prop

Some complement of the frame is adpositional.

Equations

• fr.HasAdpositional = ∃ p ∈ fr.complements, p.IsAdpositional

@[instance_reducible]

instance ArgumentFrame.instDecidableHasAdpositional (fr : ArgumentFrame) : Decidable fr.HasAdpositional

Equations

• fr.instDecidableHasAdpositional = ArgumentFrame.instDecidableHasAdpositional._aux_1 fr

def ArgumentFrame.HasClausal (fr : ArgumentFrame) : Prop

Some complement of the frame is clausal.

Equations

• fr.HasClausal = ∃ p ∈ fr.complements, p.IsClausal

@[instance_reducible]

instance ArgumentFrame.instDecidableHasClausal (fr : ArgumentFrame) : Decidable fr.HasClausal

Equations

• fr.instDecidableHasClausal = ArgumentFrame.instDecidableHasClausal._aux_1 fr

def ArgumentFrame.HasFinite (fr : ArgumentFrame) : Prop

Some complement of the frame is a finite clause.

Equations

• fr.HasFinite = ∃ p ∈ fr.complements, p.IsFinite

@[instance_reducible]

instance ArgumentFrame.instDecidableHasFinite (fr : ArgumentFrame) : Decidable fr.HasFinite

Equations

• fr.instDecidableHasFinite = ArgumentFrame.instDecidableHasFinite._aux_1 fr

def ArgumentFrame.HasImplicit (fr : ArgumentFrame) : Prop

Some complement of the frame is implicit, an argument left unexpressed.

Equations

• fr.HasImplicit = ∃ p ∈ fr.complements, p.kind = ArgumentFrame.Position.Kind.implicit

@[instance_reducible]

instance ArgumentFrame.instDecidableHasImplicit (fr : ArgumentFrame) : Decidable fr.HasImplicit

Equations

• fr.instDecidableHasImplicit = ArgumentFrame.instDecidableHasImplicit._aux_1 fr

def ArgumentFrame.leaveImplicit (fr : ArgumentFrame) (i : ℕ) (a : Option ImplicitInterp := none) : ArgumentFrame

The frame with its i-th complement left unexpressed, interpreted as a.

Equations

• fr.leaveImplicit i a = { external := fr.external, complements := fr.complements.set i (ArgumentFrame.Position.implicit a) }

def ArgumentFrame.codings (fr : ArgumentFrame) : List Complement.Coding

The [Noo07] codings recorded across the frame's complements.

Equations

• fr.codings = List.filterMap (fun (x : ArgumentFrame.Position) => x.coding?) fr.complements

def ArgumentFrame.hasType (fr : ArgumentFrame) (t : Clause.SentenceType) : Prop

Some complement of the frame selects the sentence type t.

Equations

• fr.hasType t = ∃ p ∈ fr.complements, t ∈ p.types

@[instance_reducible]

instance ArgumentFrame.instDecidableHasType (fr : ArgumentFrame) (t : Clause.SentenceType) : Decidable (fr.hasType t)

Equations

• fr.instDecidableHasType t = ArgumentFrame.instDecidableHasType._aux_1 fr t

Smart constructors

def ArgumentFrame.intransitive : ArgumentFrame

The intransitive frame has an external argument and no complement.

Equations

• ArgumentFrame.intransitive = { complements := [] }

def ArgumentFrame.impersonal : ArgumentFrame

The impersonal frame has an expletive subject and no complement.

Equations

• ArgumentFrame.impersonal = { external := some ArgumentFrame.Position.expletive, complements := [] }

def ArgumentFrame.np : ArgumentFrame

The transitive frame has one nominal complement.

Equations

• ArgumentFrame.np = { complements := [ArgumentFrame.Position.nominal] }

def ArgumentFrame.objectDrop (a : Option ImplicitInterp := none) : ArgumentFrame

The object-drop frame is the transitive frame with its object left unexpressed, with interpretation a.

Equations

• ArgumentFrame.objectDrop a = ArgumentFrame.np.leaveImplicit 0 a

def ArgumentFrame.np_np : ArgumentFrame

The double-object frame has two nominal complements.

Equations

• ArgumentFrame.np_np = { complements := [ArgumentFrame.Position.nominal, ArgumentFrame.Position.nominal] }

def ArgumentFrame.pp (p : Option Adposition := none) : ArgumentFrame

The PP frame has one adpositional complement, selecting p when given, with the type of case p marks when it marks one type.

Equations

• ArgumentFrame.pp p = { complements := [ArgumentFrame.Position.adpositional (p.bind Adposition.kind?) p] }

def ArgumentFrame.spatialPP : ArgumentFrame

The spatial PP frame has one spatial adpositional complement, whatever its adposition, as the locative or directional phrase a verb of motion selects.

Equations

• ArgumentFrame.spatialPP = { complements := [ArgumentFrame.Position.adpositional (some Case.Kind.spatial)] }

def ArgumentFrame.np_pp (p : Option Adposition := none) : ArgumentFrame

The NP + PP frame has a nominal plus an adpositional complement, selecting p when given, with the type of case p marks when it marks one type.

Equations

• ArgumentFrame.np_pp p = { complements := [ArgumentFrame.Position.nominal, ArgumentFrame.Position.adpositional (p.bind Adposition.kind?) p] }

def ArgumentFrame.finiteClause : ArgumentFrame

Finite declarative clause.

Equations

• ArgumentFrame.finiteClause = { complements := [ArgumentFrame.Position.clausal (some Complement.Coding.indicative) (Clause.Selection.only Clause.SentenceType.declarative)] }

def ArgumentFrame.subjunctiveClause : ArgumentFrame

Finite declarative clause in the subjunctive.

Equations

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

def ArgumentFrame.infinitival : ArgumentFrame

Infinitival clause. The embedded-subject requirement varies by verb (equi-deletion, raising, or adposition-marked overt subjects, [Noo07] §1.3.4), so it lives on the verb's reading, not here.

Equations

• ArgumentFrame.infinitival = { complements := [ArgumentFrame.Position.clausal (some Complement.Coding.infinitive)] }

def ArgumentFrame.raising : ArgumentFrame

The raising frame has an infinitival clause and no external argument.

Equations

• ArgumentFrame.raising = { external := none, complements := [ArgumentFrame.Position.clausal (some Complement.Coding.infinitive)] }

def ArgumentFrame.gerund : ArgumentFrame

Gerund / nominalized clause.

Equations

• ArgumentFrame.gerund = { complements := [ArgumentFrame.Position.clausal (some Complement.Coding.nominalized)] }

def ArgumentFrame.smallClause : ArgumentFrame

Small clause (consider X happy; causative make X leave). Outside [Noo07]'s coding inventory, which classifies complements by the part of speech of their predicate, so the position records nothing.

Equations

• ArgumentFrame.smallClause = { complements := [ArgumentFrame.Position.clausal] }

def ArgumentFrame.question : ArgumentFrame

The frame of an embedded question. The sentence type is orthogonal to the [Noo07] coding, so coding stays none.

Equations

• ArgumentFrame.question = { complements := [ArgumentFrame.Position.clausal none Clause.Selection.interrogatives] }