Clause axes

This file defines the axes of a clause by which the lexicon and the studies index their facts. A sentence type is the grammatical kind of a clause: Sadock and Zwicky's declarative, interrogative, imperative and exclamative, with the interrogative subtyped as polar, alternative or constituent, and the promissive that Korean grammaticalizes beside the imperative. A sentence type is a form; the speech act it conventionally performs is its force, Discourse.SpeechAct.Force, read off by Clause.SentenceType.force. An embedding context is where a clause token occurs, Bhatt and Dayal's four contexts together with Evans's insubordination, the conventionalized root use of a subordinate form. A cell is a sentence type in an embedding context, and a distribution records for each cell whether some element or process is obligatory, optional or excluded there, or nothing where the source is silent; the cells where it is possible and where it is required are the two relations a distribution determines. A particle's licensing and a language's verb-second grammar are distributions. A selection is the set of sentence types a complementizer types or a clausal argument position selects, so that whether selects polar and alternative questions and wonder any question; selections are ordered by information, a smaller set being the more specific, and two of them unify to their intersection when it is nonempty. The subject requirement and the semantic size of a complement clause are the remaining axes.

Main definitions

• Clause.SentenceType, Clause.SentenceType.IsInterrogative: the sentence types.
• Clause.EmbeddingContext, Clause.root, Clause.embedded: the embedding contexts and the cells of root and subordinated clauses.
• Clause.Occurrence, Clause.Distribution: the value of a cell and a table of cells.
• Clause.Distribution.recorded, possible, required: the relations a distribution determines.
• Clause.Selection: the sentence types a clause-typer types or a clausal position selects, unified by intersection.
• Clause.EmbeddedSubject, Clause.Size: the subject requirement and the size of a complement clause.

References

• [SZ85]
• [ZPP12]
• [BD20]
• [Day25]
• [Noo07]
• [Bon22]
• [WL23]
• [Wur24]
• [Eva07]

Sentence types

inductive Clause.SentenceType : Type

The sentence types, the grammatical kinds of clause a language distinguishes.

• declarative : SentenceType
• polar : SentenceType

  The polar, or yes/no, interrogative.

• alternative : SentenceType

  The alternative interrogative, p or q?.

• constituent : SentenceType

  The constituent, or wh, interrogative.

• imperative : SentenceType
• exclamative : SentenceType
• promissive : SentenceType

  The promissive, which Korean grammaticalizes beside the imperative.

@[instance_reducible]

instance Clause.instDecidableEqSentenceType : DecidableEq SentenceType

Equations

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

@[instance_reducible]

instance Clause.instReprSentenceType : Repr SentenceType

Equations

• Clause.instReprSentenceType = { reprPrec := Clause.instReprSentenceType.repr }

def Clause.instReprSentenceType.repr : SentenceType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Clause.instReprSentenceType.repr Clause.SentenceType.polar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.SentenceType.polar")).group prec✝

@[instance_reducible]

instance Clause.instFintypeSentenceType : Fintype SentenceType

Equations

• Clause.instFintypeSentenceType = { elems := { val := ↑Clause.SentenceType.enumList, nodup := Clause.SentenceType.enumList_nodup }, complete := Clause.instFintypeSentenceType._proof_1 }

def Clause.SentenceType.IsInterrogative (t : SentenceType) : Prop

A sentence type is interrogative when it is polar, alternative or constituent.

Equations

• t.IsInterrogative = (t = Clause.SentenceType.polar ∨ t = Clause.SentenceType.alternative ∨ t = Clause.SentenceType.constituent)

@[instance_reducible]

instance Clause.instDecidablePredSentenceTypeIsInterrogative : DecidablePred SentenceType.IsInterrogative

Equations

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

Embedding contexts and cells

inductive Clause.EmbeddingContext : Type

Where a clause token occurs, the interrogative-embedding contexts of Bhatt and Dayal and of Dayal together with Evans's insubordination, a property of the token, not of the clause.

• matrix : EmbeddingContext
• subordinated : EmbeddingContext
• quasiSubordinated : EmbeddingContext

  Embedded root-like clauses, as Hindi-Urdu kya: and Belfast English embedded inversion have them.

• quotation : EmbeddingContext
• insubordinated : EmbeddingContext

  A formally subordinate clause used as a root utterance, as the German command Dass du nicht wieder die Schlüssel vergisst! and the deliberative question Ob er immer noch kubanische Zigarren mag?.

@[instance_reducible]

instance Clause.instDecidableEqEmbeddingContext : DecidableEq EmbeddingContext

Equations

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

def Clause.instReprEmbeddingContext.repr : EmbeddingContext → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.instReprEmbeddingContext : Repr EmbeddingContext

Equations

• Clause.instReprEmbeddingContext = { reprPrec := Clause.instReprEmbeddingContext.repr }

@[instance_reducible]

instance Clause.instFintypeEmbeddingContext : Fintype EmbeddingContext

Equations

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

@[reducible, inline]

abbrev Clause.root (t : SentenceType) : SentenceType × EmbeddingContext

The cell of a root clause of sentence type t.

Equations

• Clause.root t = (t, Clause.EmbeddingContext.matrix)

@[reducible, inline]

abbrev Clause.embedded (t : SentenceType) : SentenceType × EmbeddingContext

The cell of a subordinated clause of sentence type t.

Equations

• Clause.embedded t = (t, Clause.EmbeddingContext.subordinated)

Distributions

inductive Clause.Occurrence : Type

An occurrence says whether an element or process is obligatory, optional or excluded in a cell.

• obligatory : Occurrence
• optional : Occurrence
• excluded : Occurrence

@[instance_reducible]

instance Clause.instDecidableEqOccurrence : DecidableEq Occurrence

Equations

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

@[instance_reducible]

instance Clause.instReprOccurrence : Repr Occurrence

Equations

• Clause.instReprOccurrence = { reprPrec := Clause.instReprOccurrence.repr }

def Clause.instReprOccurrence.repr : Occurrence → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Clause.instReprOccurrence.repr Clause.Occurrence.optional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Occurrence.optional")).group prec✝
• Clause.instReprOccurrence.repr Clause.Occurrence.excluded prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Occurrence.excluded")).group prec✝

@[instance_reducible]

instance Clause.instFintypeOccurrence : Fintype Occurrence

Equations

• Clause.instFintypeOccurrence = { elems := { val := ↑Clause.Occurrence.enumList, nodup := Clause.Occurrence.enumList_nodup }, complete := Clause.instFintypeOccurrence._proof_1 }

@[reducible, inline]

abbrev Clause.Distribution : Type

A distribution records the occurrence of an element or process in each cell; none means that the source records nothing for the cell, not that it is excluded.

Equations

• Clause.Distribution = (Clause.SentenceType → Clause.EmbeddingContext → Option Clause.Occurrence)

def Clause.Distribution.recorded (d : Distribution) : SetRel SentenceType EmbeddingContext

The cells the source records.

Equations

• d.recorded = {c : Clause.SentenceType × Clause.EmbeddingContext | (d c.1 c.2).isSome = true}

def Clause.Distribution.possible (d : Distribution) : SetRel SentenceType EmbeddingContext

The cells where the element or process is possible, recorded as obligatory or optional.

Equations

• d.possible = {c : Clause.SentenceType × Clause.EmbeddingContext | d c.1 c.2 = some Clause.Occurrence.obligatory ∨ d c.1 c.2 = some Clause.Occurrence.optional}

def Clause.Distribution.required (d : Distribution) : SetRel SentenceType EmbeddingContext

The cells where the element or process is required.

Equations

• d.required = {c : Clause.SentenceType × Clause.EmbeddingContext | d c.1 c.2 = some Clause.Occurrence.obligatory}

@[instance_reducible]

instance Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelRecorded {d : Distribution} (c : SentenceType × EmbeddingContext) : Decidable (c ∈ d.recorded)

Equations

• Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelRecorded c = Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelRecorded._aux_1 c

@[instance_reducible]

instance Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelPossible {d : Distribution} (c : SentenceType × EmbeddingContext) : Decidable (c ∈ d.possible)

Equations

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

@[instance_reducible]

instance Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelRequired {d : Distribution} (c : SentenceType × EmbeddingContext) : Decidable (c ∈ d.required)

Equations

• Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelRequired c = Clause.Distribution.instDecidableMemProdSentenceTypeEmbeddingContextSetRelRequired._aux_1 c

@[instance_reducible]

instance Clause.Distribution.instDecidableMemSentenceTypeSetDomEmbeddingContextPossible {d : Distribution} (t : SentenceType) : Decidable (t ∈ d.possible.dom)

Equations

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

@[instance_reducible]

instance Clause.Distribution.instDecidableMemEmbeddingContextSetCodSentenceTypePossible {d : Distribution} (e : EmbeddingContext) : Decidable (e ∈ d.possible.cod)

Equations

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

@[instance_reducible]

instance Clause.Distribution.instDecidableNonemptyProdSentenceTypeEmbeddingContextRecorded {d : Distribution} : Decidable (Set.Nonempty d.recorded)

Equations

• Clause.Distribution.instDecidableNonemptyProdSentenceTypeEmbeddingContextRecorded = { decide := decide (∃ a ∈ Finset.univ, a ∈ d.recorded), reflects_decide := ⋯ }

theorem Clause.Distribution.required_subset_possible {d : Distribution} : d.required ⊆ d.possible

theorem Clause.Distribution.possible_subset_recorded {d : Distribution} : d.possible ⊆ d.recorded

Selections

@[reducible, inline]

abbrev Clause.Selection.Types : Type

A nonempty set of sentence types, the more specific selection being the smaller set.

Equations

• Clause.Selection.Types = { s : Finset Clause.SentenceType // s.Nonempty }ᵒᵈ

@[reducible, inline]

abbrev Clause.Selection : Type

The sentence types a clause-typer types or a clausal position selects: nothing recorded, the bottom, or a nonempty set of types.

Equations

• Clause.Selection = WithBot Clause.Selection.Types

def Clause.Selection.of (s : Finset SentenceType) (h : s.Nonempty := by decide) : Selection

The selection of a nonempty set of types.

Equations

• Clause.Selection.of s h = ↑(OrderDual.toDual ⟨s, h⟩)

def Clause.Selection.only (t : SentenceType) : Selection

The selection of one type.

Equations

• Clause.Selection.only t = Clause.Selection.of {t} ⋯

def Clause.Selection.interrogatives : Selection

The selection of the three interrogative types.

Equations

• Clause.Selection.interrogatives = Clause.Selection.of {Clause.SentenceType.polar, Clause.SentenceType.alternative, Clause.SentenceType.constituent} Clause.Selection.interrogatives._proof_1

def Clause.Selection.types : Selection → Finset SentenceType

The types a selection records; none when nothing is recorded.

Equations

• Clause.Selection.types none = ∅
• Clause.Selection.types (some s) = ↑(OrderDual.ofDual s)

@[instance_reducible]

instance Clause.Selection.instMembershipSentenceType : Membership SentenceType Selection

Equations

• Clause.Selection.instMembershipSentenceType = { mem := fun (sel : Clause.Selection) (t : Clause.SentenceType) => t ∈ sel.types }

@[instance_reducible]

instance Clause.Selection.instRepr : Repr Selection

Equations

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

theorem Clause.Selection.mem_iff {sel : Selection} {t : SentenceType} : t ∈ sel ↔ t ∈ sel.types

@[instance_reducible]

instance Clause.Selection.instDecidableMemSentenceType (sel : Selection) (t : SentenceType) : Decidable (t ∈ sel)

Equations

• sel.instDecidableMemSentenceType t = Finset.decidableMem t sel.types

@[simp]

theorem Clause.Selection.types_bot : ⊥.types = ∅

@[simp]

theorem Clause.Selection.types_of (s : Finset SentenceType) (h : s.Nonempty) : (of s h).types = s

@[simp]

theorem Clause.Selection.types_only (t : SentenceType) : (only t).types = {t}

def Clause.Selection.IsInterrogative (sel : Selection) : Prop

A selection records some interrogative type.

Equations

• sel.IsInterrogative = ∃ t ∈ sel, t.IsInterrogative

@[instance_reducible]

instance Clause.Selection.instDecidableIsInterrogative (sel : Selection) : Decidable sel.IsInterrogative

Equations

• sel.instDecidableIsInterrogative = { decide := decide (∃ (a : Clause.SentenceType) (_ : a ∈ sel.types), a.IsInterrogative), reflects_decide := ⋯ }

def Clause.Selection.unifyTypes (a b : Types) : WithTop Types

Two nonempty sets of types unify to their intersection when it is nonempty.

Equations

• Clause.Selection.unifyTypes a b = if h : (↑(OrderDual.ofDual a) ∩ ↑(OrderDual.ofDual b)).Nonempty then ↑(OrderDual.toDual ⟨↑(OrderDual.ofDual a) ∩ ↑(OrderDual.ofDual b), h⟩) else ⊤

theorem Clause.Selection.le_iff {a b : Types} : a ≤ b ↔ ↑(OrderDual.ofDual b) ⊆ ↑(OrderDual.ofDual a)

@[instance_reducible]

instance Clause.Selection.instPartialUnifyTypes : PartialUnify Types

Equations

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

def Clause.Selection.unify : Selection → Selection → WithTop Selection

The bottom unifies with anything, and two recorded selections unify to their intersection when it is nonempty.

Equations

• Clause.Selection.unify none x✝ = ↑x✝
• Clause.Selection.unify (some a) none = ↑↑a
• Clause.Selection.unify (some a) (some b) = WithTop.map WithBot.some (PartialUnify.unify a b)

@[instance_reducible]

instance Clause.Selection.instPartialUnify : PartialUnify Selection

Equations

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

Complement clauses

inductive Clause.EmbeddedSubject : Type

The subject of an embedded clause is obligatorily null, as in control complements, or overt, optionally with a fixed case. Genitive marking on the subject is Noonan's criterion for the nominalization coding; Bondarenko's Buryat genitive subjects of nominalized clauses are the modern instance.

• obligatorilyNull : EmbeddedSubject
• overt (subjCase : Option Case) : EmbeddedSubject

@[instance_reducible]

instance Clause.instDecidableEqEmbeddedSubject : DecidableEq EmbeddedSubject

Equations

• Clause.instDecidableEqEmbeddedSubject = Clause.instDecidableEqEmbeddedSubject.decEq

def Clause.instDecidableEqEmbeddedSubject.decEq (x✝ x✝¹ : EmbeddedSubject) : Decidable (x✝ = x✝¹)

Equations

• Clause.instDecidableEqEmbeddedSubject.decEq Clause.EmbeddedSubject.obligatorilyNull Clause.EmbeddedSubject.obligatorilyNull = isTrue ⋯
• Clause.instDecidableEqEmbeddedSubject.decEq Clause.EmbeddedSubject.obligatorilyNull (Clause.EmbeddedSubject.overt subjCase) = isFalse ⋯
• Clause.instDecidableEqEmbeddedSubject.decEq (Clause.EmbeddedSubject.overt subjCase) Clause.EmbeddedSubject.obligatorilyNull = isFalse ⋯
• Clause.instDecidableEqEmbeddedSubject.decEq (Clause.EmbeddedSubject.overt a) (Clause.EmbeddedSubject.overt b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Clause.instReprEmbeddedSubject.repr : EmbeddedSubject → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Clause.instReprEmbeddedSubject : Repr EmbeddedSubject

Equations

• Clause.instReprEmbeddedSubject = { reprPrec := Clause.instReprEmbeddedSubject.repr }

inductive Clause.Size : Type

The semantic sort of a complement clause, which fixes the minimal structure it needs, the implicational complementation hierarchy of Wurmbrand and Lohninger: an event needs only the thematic domain, a situation adds the tense–mood–aspect domain, a proposition adds the operator domain. Ordered by containment.

• event : Size
• situation : Size
• proposition : Size

@[instance_reducible]

instance Clause.instDecidableEqSize : DecidableEq Size

Equations

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

def Clause.instReprSize.repr : Size → ℕ → Std.Format

Equations

• Clause.instReprSize.repr Clause.Size.event prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Size.event")).group prec✝
• Clause.instReprSize.repr Clause.Size.situation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Size.situation")).group prec✝
• Clause.instReprSize.repr Clause.Size.proposition prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Clause.Size.proposition")).group prec✝

@[instance_reducible]

instance Clause.instReprSize : Repr Size

Equations

• Clause.instReprSize = { reprPrec := Clause.instReprSize.repr }

@[instance_reducible]

instance Clause.instFintypeSize : Fintype Size

Equations

• Clause.instFintypeSize = { elems := { val := ↑Clause.Size.enumList, nodup := Clause.Size.enumList_nodup }, complete := Clause.instFintypeSize._proof_1 }

def Clause.Size.rank : Size → ℕ

Position on the containment order.

Equations

• Clause.Size.event.rank = 0
• Clause.Size.situation.rank = 1
• Clause.Size.proposition.rank = 2

@[instance_reducible]

instance Clause.instLinearOrderSize : LinearOrder Size

Equations

• Clause.instLinearOrderSize = LinearOrder.lift' Clause.Size.rank ⋯