Sag et al. (2020): Lessons from the English Auxiliary System #
This file formalizes the paper's constructional analysis of subject-auxiliary inversion. The
aux-initial construction requires the head daughter of a clause to be an invertible finite
auxiliary, a word marked [INV +], and says nothing about meaning: following Fillmore, the
aux-initial clauses share no semantics, and each kind of aux-initial clause gets its meaning
from the clausal type it cross-classifies with, the polar interrogative from the
interrogative clauses and the aux-initial exclamative from the exclamative clauses. So the
construction is one principle over the RSRL construct hierarchy of
Syntax/HPSG/Construction (auxInitialPrinciple), the two clauses are sorts below both the
aux-initial construction and a clausal type (sai_cross_classify), and a worked construct of
either sort satisfies the grammar exactly when its head is inverted and its mother carries the
clausal type's semantics (polarInterrogative_models, auxInitialExclamative_models). A
polar interrogative is built directly by its construction rather than derived from an
uninverted clause, which is why the auxiliary puzzle of structure dependence never arises.
Implementation notes #
The construction's valence conditions, that the head daughter's valents are its sisters and
the mother is valence-saturated, are not in the RSRL signature and are not modelled; only the
[INV +] head is. The remaining constructions of the paper, the inflectional and negation
constructions and contraction, are not formalized.
References #
The aux-initial construction requires the head daughter to be an inverted verb.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The filler-gap grammar extended with the aux-initial construction.
Equations
Instances For
The aux-initial construction is a headed construction beside the filler-head construction, and the polar interrogative and aux-initial exclamative clauses cross-classify it with the interrogative and exclamative clausal types.
Worked aux-initial constructs #
The entities of a worked aux-initial construct are the construct, its mother and head daughter, the verbal category they share with its inversion value and finite verb form, and the mother's semantic object. An aux-initial construct has no filler daughter.
Instances For
Equations
- SagEtAl2020.instDecidableEqSAIEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- SagEtAl2020.instFintypeSAIEnt = { elems := { val := ↑SagEtAl2020.SAIEnt.enumList, nodup := SagEtAl2020.SAIEnt.enumList_nodup }, complete := SagEtAl2020.instFintypeSAIEnt._proof_1 }
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.cat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.cat")).group prec✝
- SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.inv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.inv")).group prec✝
- SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.vform prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.vform")).group prec✝
- SagEtAl2020.instReprSAIEnt.repr SagEtAl2020.SAIEnt.sem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "SagEtAl2020.SAIEnt.sem")).group prec✝
Instances For
Equations
- SagEtAl2020.instReprSAIEnt = { reprPrec := SagEtAl2020.instReprSAIEnt.repr }
A finite aux-initial construct of sort cxtSort whose head daughter has inversion value
invSort and whose mother has semantic type semSort.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The worked constructs are well-typed whenever the inversion value and the semantic type have sorts of the right kind.
A polar interrogative satisfies the grammar exactly when its head is inverted and its mother is a question: the inversion comes from the aux-initial construction and the semantics from the interrogative clausal type, neither stated on the polar interrogative itself.
An aux-initial exclamative satisfies the grammar exactly when its head is inverted and its mother is a fact: the same inverted head with the exclamative type's semantics.