Sag (2010): English Filler-Gap Constructions

This file formalizes the paper's account of the five English filler-gap clauses, topicalized, wh-exclamative, nonsubject wh-interrogative, wh-relative and the-clauses, as constructions of Sign-Based Construction Grammar. The clauses share the filler-head construction, which binds a nonverbal filler to a gap in a verbal head daughter, and each cross-classifies with a clausal type that fixes its semantic type; what remains to each is a short list of constraints, from which the paper's parameters of variation follow: which distinguished element the filler must contain, which categories the filler and head daughters may have, whether the head may or must be inverted or infinitival, whether the clause is an island, and whether it must be independent.

The constructions are those of the paper's appendix, stated in RSRL over the construct hierarchy of Syntax/HPSG/Construction. A row of the paper's examples describes a construct, the categories of its daughters and the inversion, independence and finiteness of its head, and the row is acceptable exactly when that construct is a model of the grammar (judgments). The parameters of variation hold in every model of the grammar: the filler is nonverbal (satisfies_filler_nonverbal), the head of every clause but the the-clause is a projection of a verb, since only a verb is inverted or uninverted (satisfies_head_verb), and the head's inversion, finiteness and independence follow from the constructions, a wh-relative's through its mother (satisfies_head_uninverted, satisfies_head_fin, satisfies_head_ic). A clause is an absolute island when every construct of its sort, in every model of the grammar, has a mother with an empty GAP list (FGClause.IsIsland). Topicalized clauses, wh-exclamatives and the-clauses are islands, since their constructions give the head daughter a single gap, which the filler discharges (isIsland_iff). The distinguished element is lexical: the wh-word inventory is read off the paper's judgment triples (occurs), and no wh-form of any category occurs in all three wh-constructions (no_universal_wh_word).

Implementation notes

The WH, REL and VAL features are not in the RSRL signature, so the distinguished element is checked against the wh-word inventory rather than by the model theory, and S and VP, both projections of a verb, are not told apart. Independence is identified with the absence of embedding, so the embedded topicalizations the paper licenses under predicates that admit main-clause phenomena are not among the rows. The inventory is derived from the judgment triples rather than transcribed from the paper's table of wh-words, which prints two cells differently: bare what in exclamatives and determiner which in relatives are marked as accepted by some speakers in the table but starred in the triples. The island rows are checked in one direction, since the paper attributes the graded degradation of extraction from finite wh-interrogatives to processing. The-clauses come out as islands because the the-clause construction gives the head daughter a single gap, as the topicalization and wh-exclamative constructions do. The text discusses islandhood only for the latter two, and no row tests a the-clause.

TODO

• The paper stars its example of a the-clause with a complementizer head although its text admits an S or CP head; the row is omitted.

References

• [Sag10]
• [GS00]
• [BMS01]
• [HS10]

The five constructions

inductive Sag2010.FGClause : Type

The five English filler-gap clauses.

• topicalized : FGClause
• whExclamative : FGClause
• whInterrogative : FGClause
• whRelative : FGClause
• theClause : FGClause

@[instance_reducible]

instance Sag2010.instDecidableEqFGClause : DecidableEq FGClause

Equations

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

def Sag2010.instReprFGClause.repr : FGClause → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sag2010.instReprFGClause.repr Sag2010.FGClause.whRelative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.FGClause.whRelative")).group prec✝
• Sag2010.instReprFGClause.repr Sag2010.FGClause.theClause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.FGClause.theClause")).group prec✝

@[instance_reducible]

instance Sag2010.instReprFGClause : Repr FGClause

Equations

• Sag2010.instReprFGClause = { reprPrec := Sag2010.instReprFGClause.repr }

@[instance_reducible]

instance Sag2010.instFintypeFGClause : Fintype FGClause

Equations

• Sag2010.instFintypeFGClause = { elems := { val := ↑Sag2010.FGClause.enumList, nodup := Sag2010.FGClause.enumList_nodup }, complete := Sag2010.instFintypeFGClause._proof_1 }

def Sag2010.FGClause.sort : FGClause → HPSG.Construction.Srt

The construct sort of a clause in the RSRL hierarchy.

Equations

• Sag2010.FGClause.topicalized.sort = HPSG.Construction.Srt.topCl
• Sag2010.FGClause.whExclamative.sort = HPSG.Construction.Srt.whExclCl
• Sag2010.FGClause.whInterrogative.sort = HPSG.Construction.Srt.nsWhIntCl
• Sag2010.FGClause.whRelative.sort = HPSG.Construction.Srt.whRelCl
• Sag2010.FGClause.theClause.sort = HPSG.Construction.Srt.theCl

def Sag2010.FGClause.sem : FGClause → HPSG.Construction.Srt

The semantic type of a clause is a question, a fact, a modifier, or an austinean object.

Equations

• Sag2010.FGClause.whInterrogative.sem = HPSG.Construction.Srt.question
• Sag2010.FGClause.whExclamative.sem = HPSG.Construction.Srt.fact
• Sag2010.FGClause.whRelative.sem = HPSG.Construction.Srt.modifier
• Sag2010.FGClause.topicalized.sem = HPSG.Construction.Srt.austinean
• Sag2010.FGClause.theClause.sem = HPSG.Construction.Srt.austinean

Constructs

inductive Sag2010.Cat : Type

The syntactic categories of filler and head daughters.

• NP : Cat
• PP : Cat
• AP : Cat
• AdvP : Cat
• VP : Cat
• S : Cat
• CP : Cat

@[instance_reducible]

instance Sag2010.instDecidableEqCat : DecidableEq Cat

Equations

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

@[instance_reducible]

instance Sag2010.instReprCat : Repr Cat

Equations

• Sag2010.instReprCat = { reprPrec := Sag2010.instReprCat.repr }

def Sag2010.instReprCat.repr : Cat → ℕ → Std.Format

Equations

• Sag2010.instReprCat.repr Sag2010.Cat.NP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.NP")).group prec✝
• Sag2010.instReprCat.repr Sag2010.Cat.PP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.PP")).group prec✝
• Sag2010.instReprCat.repr Sag2010.Cat.AP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.AP")).group prec✝
• Sag2010.instReprCat.repr Sag2010.Cat.AdvP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.AdvP")).group prec✝
• Sag2010.instReprCat.repr Sag2010.Cat.VP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.VP")).group prec✝
• Sag2010.instReprCat.repr Sag2010.Cat.S prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.S")).group prec✝
• Sag2010.instReprCat.repr Sag2010.Cat.CP prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Cat.CP")).group prec✝

@[instance_reducible]

instance Sag2010.instFintypeCat : Fintype Cat

Equations

• Sag2010.instFintypeCat = { elems := { val := ↑Sag2010.Cat.enumList, nodup := Sag2010.Cat.enumList_nodup }, complete := Sag2010.instFintypeCat._proof_1 }

def Sag2010.Cat.sort : Cat → HPSG.Construction.Srt

The category sort of the RSRL hierarchy; S and VP are both projections of a verb.

Equations

• Sag2010.Cat.NP.sort = HPSG.Construction.Srt.noun
• Sag2010.Cat.PP.sort = HPSG.Construction.Srt.prep
• Sag2010.Cat.AP.sort = HPSG.Construction.Srt.adj
• Sag2010.Cat.AdvP.sort = HPSG.Construction.Srt.adv
• Sag2010.Cat.VP.sort = HPSG.Construction.Srt.verb
• Sag2010.Cat.S.sort = HPSG.Construction.Srt.verb
• Sag2010.Cat.CP.sort = HPSG.Construction.Srt.comp

inductive Sag2010.Ent : Type

The entities of a worked construct are the construct, its mother, head daughter and filler daughter, their categories, two list cells and the empty list, two gaps with their indices and the second gap's category, the mother's semantic object, and the values of the head's features.

• cxt : Ent
• mtr : Ent
• hd : Ent
• fl : Ent
• flCat : Ent
• hdCat : Ent
• g1 : Ent
• g2 : Ent
• nil : Ent
• gp1 : Ent
• gp2 : Ent
• gp2Cat : Ent
• ix1 : Ent
• ix2 : Ent
• sem : Ent
• plus : Ent
• minus : Ent
• fin : Ent
• inf : Ent

@[instance_reducible]

instance Sag2010.instDecidableEqEnt : DecidableEq Ent

Equations

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

@[instance_reducible]

instance Sag2010.instFintypeEnt : Fintype Ent

Equations

• Sag2010.instFintypeEnt = { elems := { val := ↑Sag2010.Ent.enumList, nodup := Sag2010.Ent.enumList_nodup }, complete := Sag2010.instFintypeEnt._proof_1 }

def Sag2010.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

• Sag2010.instReprEnt.repr Sag2010.Ent.cxt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.cxt")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.mtr prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.mtr")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.hd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.hd")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.fl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.fl")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.flCat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.flCat")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.hdCat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.hdCat")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.g1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.g1")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.g2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.g2")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.nil prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.nil")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.gp1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.gp1")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.gp2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.gp2")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.gp2Cat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.gp2Cat")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.ix1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.ix1")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.ix2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.ix2")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.sem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.sem")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.plus")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.minus")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.fin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.fin")).group prec✝
• Sag2010.instReprEnt.repr Sag2010.Ent.inf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Ent.inf")).group prec✝

@[instance_reducible]

instance Sag2010.instReprEnt : Repr Ent

Equations

• Sag2010.instReprEnt = { reprPrec := Sag2010.instReprEnt.repr }

@[reducible]

def Sag2010.construct (σ : HPSG.Construction.Srt) (filler head : Cat) (inv ic vform : Ent) (semSort : HPSG.Construction.Srt) (rest : Ent) : HPSG.RSRL.Interpretation HPSG.Construction.sig Ent

The construct of sort σ whose filler and head daughters have the categories filler and head, whose head has the inversion, independence and verb-form values inv, ic and vform, whose mother has the semantic type semSort, and whose mother's GAP list is rest, either the empty list nil or the list g2 of a second gap. The filler shares its category and index with the first gap, and the mother its category with the head daughter. As the signature requires, only a verb has an inversion value and only a verbal category an independence value and a verb form.

Equations

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

def Sag2010.FGClause.cxtSort : FGClause → Ent → HPSG.Construction.Srt

The construct sort of a clause whose head has the verb form vform. A wh-relative is finite or infinitival.

Equations

• Sag2010.FGClause.whRelative.cxtSort Sag2010.Ent.inf = HPSG.Construction.Srt.infWhRelCl
• Sag2010.FGClause.whRelative.cxtSort x✝ = HPSG.Construction.Srt.finWhRelCl
• x✝¹.cxtSort x✝ = x✝¹.sort

@[reducible, inline]

abbrev Sag2010.FGClause.construct (c : FGClause) (semSort : HPSG.Construction.Srt) (rest : Ent) : HPSG.RSRL.Interpretation HPSG.Construction.sig Ent

A finite construct of the clause with a noun phrase filler and a sentential head, whose mother has semantic type semSort and GAP list rest. Its head is inverted and independent in a wh-interrogative, uninverted and embedded in a wh-relative, and uninverted and independent otherwise.

Equations

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

theorem Sag2010.models_construct_iff (c : FGClause) (σ : HPSG.Construction.Srt) (hσ : σ ∈ [HPSG.Construction.Srt.question, HPSG.Construction.Srt.fact, HPSG.Construction.Srt.modifier, HPSG.Construction.Srt.austinean]) : (c.construct σ Ent.nil).Models HPSG.Construction.grammar ↔ σ = c.sem

A construct of the clause's sort satisfies the grammar exactly when its mother has the clause's semantic type.

theorem Sag2010.isWellTyped_constructs (c : FGClause) : (c.construct c.sem Ent.nil).IsWellTyped ∧ (c.construct c.sem Ent.g2).IsWellTyped

The constructs of each clause, with one gap or two, are well-typed, so the grammar's verdict on them is a verdict of its constructions and not of the appropriateness conditions.

Islands

def Sag2010.FGClause.IsIsland (c : FGClause) : Prop

A clause is an absolute island when, in every model of the grammar, every construct of its sort has a mother with an empty GAP list, so that no gap inside the clause is bound outside it.

Equations

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

theorem Sag2010.satisfies_gapRest_elist {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} {u : U} (hI : I.Models HPSG.Construction.grammar) {c : FGClause} (hc : c = FGClause.topicalized ∨ c = FGClause.whExclamative ∨ c = FGClause.theClause) (hu : I.S u ≤ c.sort) : I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.HDDTR, HPSG.Construction.Attr.GAP, HPSG.Construction.Attr.REST]) HPSG.Construction.Srt.elist)

In a model of the grammar, the head daughter of a topicalized clause, a wh-exclamative or a the-clause has a single gap.

theorem Sag2010.isIsland_iff (c : FGClause) : c.IsIsland ↔ c = FGClause.topicalized ∨ c = FGClause.whExclamative ∨ c = FGClause.theClause

Exactly topicalized clauses, wh-exclamatives and the-clauses are absolute islands. Their constructions give the head daughter a single gap, which the filler discharges, while a wh-interrogative or a wh-relative construct may pass a second gap to its mother.

The parameters of variation

The constructions fix the parameters of variation (6) in every model of the grammar, not only in the worked constructs.

theorem Sag2010.satisfies_filler_nonverbal {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} {u : U} (hI : I.Models HPSG.Construction.grammar) (hs : I.IsSortResolved) (c : FGClause) (hu : I.S u ≤ c.sort) : I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.FILLERDTR, HPSG.Construction.Attr.CAT]) HPSG.Construction.Srt.nonverbal)

The filler daughter of each of the five clauses is nonverbal, a noun phrase, prepositional phrase, adjective phrase or adverb phrase (25). A wh-relative's is nominal or prepositional, according as it is finite or infinitival.

theorem Sag2010.satisfies_head_verb {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} {u : U} (hI : I.Models HPSG.Construction.grammar) (hw : I.IsWellTyped) {c : FGClause} (hc : c ≠ FGClause.theClause) (hu : I.S u ≤ c.sort) : I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.HDDTR, HPSG.Construction.Attr.CAT]) HPSG.Construction.Srt.verb)

The head daughter of a topicalized clause, wh-exclamative, wh-interrogative or wh-relative is a projection of a verb (27). Except in the topicalized clause, which states it, this follows from the head's inversion value, which only a verb has; a wh-relative's comes from the relative construction on its mother.

theorem Sag2010.satisfies_head_uninverted {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} {u : U} (hI : I.Models HPSG.Construction.grammar) {c : FGClause} (hc : c = FGClause.topicalized ∨ c = FGClause.whExclamative ∨ c = FGClause.whRelative) (hu : I.S u ≤ c.sort) : I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.HDDTR, HPSG.Construction.Attr.CAT, HPSG.Construction.Attr.INV]) HPSG.Construction.Srt.minus)

The head daughter of a topicalized clause, wh-exclamative or wh-relative is uninverted (28). A wh-relative inherits this from the relative construction on its mother.

theorem Sag2010.satisfies_head_fin {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} {u : U} (hI : I.Models HPSG.Construction.grammar) (hu : I.S u ≤ HPSG.Construction.Srt.topCl ∨ I.S u ≤ HPSG.Construction.Srt.whExclCl ∨ I.S u ≤ HPSG.Construction.Srt.theCl ∨ I.S u ≤ HPSG.Construction.Srt.finWhRelCl) : I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.HDDTR, HPSG.Construction.Attr.CAT, HPSG.Construction.Attr.VFORM]) HPSG.Construction.Srt.fin)

The head daughter of a topicalized clause, wh-exclamative, the-clause or finite wh-relative is finite (29). In a finite wh-relative the construction makes the mother finite, and the head daughter shares the mother's category.

theorem Sag2010.satisfies_head_ic {U : Type u_1} {I : HPSG.RSRL.Interpretation HPSG.Construction.sig U} {u : U} (hI : I.Models HPSG.Construction.grammar) : (I.S u ≤ HPSG.Construction.Srt.topCl → I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.HDDTR, HPSG.Construction.Attr.CAT, HPSG.Construction.Attr.IC]) HPSG.Construction.Srt.plus)) ∧ (I.S u ≤ HPSG.Construction.Srt.whRelCl → I.Satisfies (fun (x : ℕ) => u) u (HPSG.RSRL.Desc.sortAssign (HPSG.RSRL.Term.path [HPSG.Construction.Attr.HDDTR, HPSG.Construction.Attr.CAT, HPSG.Construction.Attr.IC]) HPSG.Construction.Srt.minus))

The head daughter of a topicalized clause is independent and that of a wh-relative is not. A wh-relative inherits this from the relative construction on its mother.

The distinguished element

inductive Sag2010.Marker : Type

The distinguished element that a construction requires in its filler daughter. Topicalization requires none, a the-clause requires the definite degree marker, and the other constructions require a wh-word of their own kind.

• none : Marker
• the : Marker
• interrogative : Marker
• exclamative : Marker
• relative : Marker

@[instance_reducible]

instance Sag2010.instDecidableEqMarker : DecidableEq Marker

Equations

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

def Sag2010.instReprMarker.repr : Marker → ℕ → Std.Format

Equations

• Sag2010.instReprMarker.repr Sag2010.Marker.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Marker.none")).group prec✝
• Sag2010.instReprMarker.repr Sag2010.Marker.the prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Marker.the")).group prec✝
• Sag2010.instReprMarker.repr Sag2010.Marker.interrogative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Marker.interrogative")).group prec✝
• Sag2010.instReprMarker.repr Sag2010.Marker.exclamative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Marker.exclamative")).group prec✝
• Sag2010.instReprMarker.repr Sag2010.Marker.relative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Marker.relative")).group prec✝

@[instance_reducible]

instance Sag2010.instReprMarker : Repr Marker

Equations

• Sag2010.instReprMarker = { reprPrec := Sag2010.instReprMarker.repr }

def Sag2010.FGClause.marker : FGClause → Marker

The marker each construction requires.

Equations

• Sag2010.FGClause.topicalized.marker = Sag2010.Marker.none
• Sag2010.FGClause.theClause.marker = Sag2010.Marker.the
• Sag2010.FGClause.whInterrogative.marker = Sag2010.Marker.interrogative
• Sag2010.FGClause.whExclamative.marker = Sag2010.Marker.exclamative
• Sag2010.FGClause.whRelative.marker = Sag2010.Marker.relative

inductive Sag2010.WhForm : Type

The wh-forms of the inventory.

• who : WhForm
• whose : WhForm
• what : WhForm
• whatA : WhForm
• which : WhForm
• how : WhForm
• when : WhForm
• where : WhForm
• why : WhForm

@[instance_reducible]

instance Sag2010.instDecidableEqWhForm : DecidableEq WhForm

Equations

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

def Sag2010.instReprWhForm.repr : WhForm → ℕ → Std.Format

Equations

• Sag2010.instReprWhForm.repr Sag2010.WhForm.who prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.who")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.whose prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.whose")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.what prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.what")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.whatA prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.whatA")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.which prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.which")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.how prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.how")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.when prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.when")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.where prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.where")).group prec✝
• Sag2010.instReprWhForm.repr Sag2010.WhForm.why prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhForm.why")).group prec✝

@[instance_reducible]

instance Sag2010.instReprWhForm : Repr WhForm

Equations

• Sag2010.instReprWhForm = { reprPrec := Sag2010.instReprWhForm.repr }

@[instance_reducible]

instance Sag2010.instFintypeWhForm : Fintype WhForm

Equations

• Sag2010.instFintypeWhForm = { elems := { val := ↑Sag2010.WhForm.enumList, nodup := Sag2010.WhForm.enumList_nodup }, complete := Sag2010.instFintypeWhForm._proof_1 }

inductive Sag2010.WhCategory : Type

The categories a wh-form bears.

• np : WhCategory
• det : WhCategory
• detSing : WhCategory
• detPl : WhCategory
• degree : WhCategory
• advpManner : WhCategory
• ap : WhCategory
• ppTime : WhCategory
• ppPlace : WhCategory
• ppReason : WhCategory

@[instance_reducible]

instance Sag2010.instDecidableEqWhCategory : DecidableEq WhCategory

Equations

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

@[instance_reducible]

instance Sag2010.instReprWhCategory : Repr WhCategory

Equations

• Sag2010.instReprWhCategory = { reprPrec := Sag2010.instReprWhCategory.repr }

def Sag2010.instReprWhCategory.repr : WhCategory → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.np prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.np")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.det prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.det")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.detSing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.detSing")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.detPl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.detPl")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.degree prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.degree")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.ap prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.ap")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.ppTime prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.ppTime")).group prec✝
• Sag2010.instReprWhCategory.repr Sag2010.WhCategory.ppPlace prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.WhCategory.ppPlace")).group prec✝

@[instance_reducible]

instance Sag2010.instFintypeWhCategory : Fintype WhCategory

Equations

• Sag2010.instFintypeWhCategory = { elems := { val := ↑Sag2010.WhCategory.enumList, nodup := Sag2010.WhCategory.enumList_nodup }, complete := Sag2010.instFintypeWhCategory._proof_1 }

The paper's examples

inductive Sag2010.Parameter : Type

The parameters of variation the rows probe, and the wh-word inventory.

• distinguished : Parameter
• inventory : Parameter
• fillerCategory : Parameter
• headCategory : Parameter
• inversion : Parameter
• finiteness : Parameter
• independence : Parameter
• island : Parameter

@[instance_reducible]

instance Sag2010.instDecidableEqParameter : DecidableEq Parameter

Equations

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

def Sag2010.instReprParameter.repr : Parameter → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Sag2010.instReprParameter.repr Sag2010.Parameter.inventory prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Parameter.inventory")).group prec✝
• Sag2010.instReprParameter.repr Sag2010.Parameter.inversion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Parameter.inversion")).group prec✝
• Sag2010.instReprParameter.repr Sag2010.Parameter.island prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sag2010.Parameter.island")).group prec✝

@[instance_reducible]

instance Sag2010.instReprParameter : Repr Parameter

Equations

• Sag2010.instReprParameter = { reprPrec := Sag2010.instReprParameter.repr }

def Sag2010.parameters : List (String × Parameter)

Equations

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

def Sag2010.clauses : List (String × FGClause)

Equations

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

def Sag2010.cats : List (String × Cat)

Equations

• Sag2010.cats = [("NP", Sag2010.Cat.NP), ("PP", Sag2010.Cat.PP), ("AP", Sag2010.Cat.AP), ("AdvP", Sag2010.Cat.AdvP), ("VP", Sag2010.Cat.VP), ("S", Sag2010.Cat.S), ("CP", Sag2010.Cat.CP)]

def Sag2010.bools : List (String × Bool)

Equations

• Sag2010.bools = [("true", true), ("false", false)]

def Sag2010.whForms : List (String × WhForm)

Equations

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

def Sag2010.whCategories : List (String × WhCategory)

Equations

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

def Sag2010.probing (p : Parameter) : List Datum

The rows probing a parameter.

Equations

• Sag2010.probing p = List.filter (fun (x : Datum) => decide (x.parse? "parameter" Sag2010.parameters = some p)) Sag2010.Examples.all

def Sag2010.clause? (x : Datum) : Option FGClause

The clause a row instantiates.

Equations

• Sag2010.clause? x = x.parse? "construction" Sag2010.clauses

def Sag2010.inversions : List (String × Ent)

The inversion values that rows record.

Equations

• Sag2010.inversions = [("true", Sag2010.Ent.plus), ("false", Sag2010.Ent.minus)]

def Sag2010.embeddings : List (String × Ent)

The independence values of embedded and matrix clauses.

Equations

• Sag2010.embeddings = [("true", Sag2010.Ent.minus), ("false", Sag2010.Ent.plus)]

def Sag2010.verbForms : List (String × Ent)

The verb forms of finite and infinitival clauses.

Equations

• Sag2010.verbForms = [("true", Sag2010.Ent.fin), ("false", Sag2010.Ent.inf)]

@[reducible]

def Sag2010.rowConstruct (c : FGClause) (x : Datum) : HPSG.RSRL.Interpretation HPSG.Construction.sig Ent

The construct of the clause c that a row describes, with its filler and head categories and the inversion, embedding and finiteness of its head. The filler is an NP and the head an uninverted, finite, matrix S unless the row records otherwise.

Equations

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

def Sag2010.whWord? (x : Datum) : Option (WhForm × WhCategory)

The wh-form and category of a row's filler, if it contains a wh-word.

Equations

• Sag2010.whWord? x = (x.parse? "whForm" Sag2010.whForms).bind fun (f : Sag2010.WhForm) => Option.map (fun (x : Sag2010.WhCategory) => (f, x)) (x.parse? "whCategory" Sag2010.whCategories)

def Sag2010.occurs (f : WhForm) (cat : WhCategory) (c : FGClause) : Option Judgment

The judgment the inventory records for a wh-form of a category in a wh-construction.

Equations

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

def Sag2010.whClauses : List FGClause

The three wh-constructions.

Equations

• Sag2010.whClauses = [Sag2010.FGClause.whInterrogative, Sag2010.FGClause.whExclamative, Sag2010.FGClause.whRelative]

theorem Sag2010.no_universal_wh_word (x : Datum) : x ∈ probing Parameter.inventory → ∀ w ∈ whWord? x, ∃ c ∈ whClauses, occurs w.1 w.2 c ≠ some Judgment.acceptable

No wh-form of any category occurs in all three wh-constructions: there is no unitary category of English wh-expression.

def Sag2010.markers (f : WhForm) (cat : WhCategory) : List Marker

The markers a filler containing a wh-form of a category can bear: those of the wh-constructions in which the inventory records it as acceptable.

Equations

• Sag2010.markers f cat = List.map Sag2010.FGClause.marker (List.filter (fun (c : Sag2010.FGClause) => decide (Sag2010.occurs f cat c = some Judgment.acceptable)) Sag2010.whClauses)

def Sag2010.fillerMarkers (x : Datum) : List Marker

The markers that a row's filler can bear. They are those of its wh-word if it contains one, the definite degree marker if it contains comparative the, and none otherwise.

Equations

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

theorem Sag2010.distinguished (x : Datum) : x ∈ probing Parameter.distinguished → ∀ (c : FGClause), clause? x = some c → (x.judgment = Judgment.acceptable ↔ c.marker ∈ fillerMarkers x)

The rows probing the distinguished element are acceptable exactly when the filler can bear the construction's marker.

theorem Sag2010.judgments (p : Parameter) : p ∈ [Parameter.fillerCategory, Parameter.headCategory, Parameter.inversion, Parameter.finiteness, Parameter.independence] → ∀ x ∈ probing p, ∀ (c : FGClause), clause? x = some c → (x.judgment = Judgment.acceptable ↔ (rowConstruct c x).Models HPSG.Construction.grammar)

The rows probing the categories of the daughters and the inversion, finiteness and independence of the head are acceptable exactly when the construct they describe is a model of the grammar.

theorem Sag2010.isWellTyped_rowConstruct (p : Parameter) : p ∈ [Parameter.fillerCategory, Parameter.headCategory, Parameter.inversion, Parameter.finiteness, Parameter.independence] → ∀ x ∈ probing p, ∀ (c : FGClause), clause? x = some c → (rowConstruct c x).IsWellTyped

The constructs that the rows describe are well-typed, so each verdict of judgments is one of the constructions.

theorem Sag2010.island_rows (x : Datum) : x ∈ probing Parameter.island → ∀ (c : FGClause), clause? x = some c → x.judgment = Judgment.acceptable → ¬c.IsIsland

The rows extracting a second gap from a clause are acceptable only when the clause is not an island.