Sag et al. (2020): the Aux-Initial (Subject-Auxiliary Inversion) construction

[SCA+20b] [Sag10]

The second paper-anchored consumer of the SBCG construct type hierarchy (Syntax/HPSG/Construction.lean). [SCA+20b] analyzes the English auxiliary system in Sign-Based Construction Grammar; its Aux-Initial Construction ((39)) is a headed-cxt subtype — a sibling of the filler-gap supertype filler-head-cxt — whose head daughter is an inverted [INV +] word (an invertible finite auxiliary).

Following Fillmore (1999), aux-initial constructions share no semantics ([SCA+20b] fn. 34); a particular SAI's clausal meaning comes only from cross-classification with the clausal dimension. So the interrogative SAI ("Has Lee eaten apples?") is aux-initial-cxt ⊓ interrogative-cl, and a worked construct inherits the inverted head (from aux-initial-cxt) and the question semantics (from interrogative-cl) from one sort — by the same multiple-inheritance machinery as [Sag10]'s filler-gap constructions.

That two paper-anchored studies (this and Studies/Sag2010.lean) consume one construct hierarchy is the justification for its theory-layer home. The aux-initial / inversion sort nodes and the INV feature live in the substrate; the construction's own principle and worked constructs are here.

Scope

The single distinguishing constraint modeled is the head's [INV +] value. The richer apparatus of the paper — the MTR/DTRS SYN token-sharing of (39), the valence list VAL/⊕ amalgamation, the AUX/GRAM features, and the ellipsis interactions — is deferred, as are the other SAI subtypes (polar-interrogative, exclamative, conditional inversion).

def SagEtAl2020.auxInitialPrinciple : HPSG.RSRL.Desc HPSG.Construction.sig

The Aux-Initial Construction ([SCA+20b] (39)): the head daughter is an inverted ([INV +]) word — an invertible finite auxiliary. Unlike the filler-gap constructions it carries no shared semantics (Fillmore 1999, [SCA+20b] fn. 34); its clausal meaning comes only from cross-classification.

Equations

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

def SagEtAl2020.saiGrammar : HPSG.RSRL.Grammar HPSG.Construction.sig

The filler-gap grammar of Construction.lean extended with the inversion construction.

Equations

• SagEtAl2020.saiGrammar = HPSG.Construction.grammar ++ [SagEtAl2020.auxInitialPrinciple]

theorem SagEtAl2020.sai_cross_classify : (HPSG.Construction.Srt.auxInitialCxt ≤ HPSG.Construction.Srt.headedCxt ∧ HPSG.Construction.Srt.fillerHeadCxt ≤ HPSG.Construction.Srt.headedCxt) ∧ HPSG.Construction.Srt.interrogativeSAI ≤ HPSG.Construction.Srt.auxInitialCxt ∧ HPSG.Construction.Srt.interrogativeSAI ≤ HPSG.Construction.Srt.interrogativeCl

aux-initial-cxt is a sibling of filler-head-cxt under headed-cxt, and the interrogative SAI cross-classifies it with interrogative-cl — the same machinery as [Sag10]'s filler-gap constructions, now for the second paper's construction.

A worked interrogative SAI

inductive SagEtAl2020.SAIEnt : Type

Entities of a worked aux-initial construct: the construct, its mother and (inverted) head daughter, and the inversion- and semantic-value objects. (Aux-initial constructs have no filler daughter.)

• cxt : SAIEnt
• mtr : SAIEnt
• hd : SAIEnt
• invE : SAIEnt
• semE : SAIEnt

@[implicit_reducible]

instance SagEtAl2020.instDecidableEqSAIEnt : DecidableEq SAIEnt

Equations

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

@[implicit_reducible]

instance SagEtAl2020.instFintypeSAIEnt : Fintype SAIEnt

Equations

• SagEtAl2020.instFintypeSAIEnt = { elems := { val := ↑SagEtAl2020.SAIEnt.enumList, nodup := SagEtAl2020.SAIEnt.enumList_nodup }, complete := SagEtAl2020.instFintypeSAIEnt._proof_1 }

@[implicit_reducible]

instance SagEtAl2020.instReprSAIEnt : Repr SAIEnt

Equations

• SagEtAl2020.instReprSAIEnt = { reprPrec := SagEtAl2020.instReprSAIEnt.repr }

def SagEtAl2020.instReprSAIEnt.repr : SAIEnt → ℕ → Std.Format

Equations

• SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.cxt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.cxt")).group prec✝
• SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.mtr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.mtr")).group prec✝
• SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.hd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.hd")).group prec✝
• SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.invE prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.invE")).group prec✝
• SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.semE prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.semE")).group prec✝

@[reducible]

def SagEtAl2020.goodInterrogativeSAI : HPSG.RSRL.Interpretation HPSG.Construction.sig

A well-formed interrogative SAI (sort interrogative-SAI): inverted head, interrogative mother.

Equations

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

@[implicit_reducible]

instance SagEtAl2020.instFintypeUSrtGoodInterrogativeSAI : Fintype goodInterrogativeSAI.U

Equations

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

@[implicit_reducible]

instance SagEtAl2020.instDecidableEqUSrtGoodInterrogativeSAI : DecidableEq goodInterrogativeSAI.U

Equations

• SagEtAl2020.instDecidableEqUSrtGoodInterrogativeSAI = SagEtAl2020.instDecidableEqSAIEnt

@[reducible]

def SagEtAl2020.saiUninverted : HPSG.RSRL.Interpretation HPSG.Construction.sig

The inverted-head restriction binds: an aux-initial construct with an [INV −] head violates the aux-initial principle.

Equations

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

@[implicit_reducible]

instance SagEtAl2020.instFintypeUSrtSaiUninverted : Fintype saiUninverted.U

Equations

• SagEtAl2020.instFintypeUSrtSaiUninverted = { elems := { val := ↑SagEtAl2020.SAIEnt.enumList, nodup := SagEtAl2020.SAIEnt.enumList_nodup }, complete := SagEtAl2020.instFintypeSAIEnt._proof_1 }

@[implicit_reducible]

instance SagEtAl2020.instDecidableEqUSrtSaiUninverted : DecidableEq saiUninverted.U

Equations

• SagEtAl2020.instDecidableEqUSrtSaiUninverted = SagEtAl2020.instDecidableEqUSrtGoodInterrogativeSAI