inductive HPSG.VForm : Type

Verb form features.

• finite : VForm
• infinitive : VForm
• gerund : VForm
• pastParticiple : VForm
• presentParticiple : VForm

def HPSG.instReprVForm.repr : VForm → Nat → Std.Format

Equations

• HPSG.instReprVForm.repr HPSG.VForm.finite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.VForm.finite")).group prec✝
• HPSG.instReprVForm.repr HPSG.VForm.infinitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.VForm.infinitive")).group prec✝
• HPSG.instReprVForm.repr HPSG.VForm.gerund prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.VForm.gerund")).group prec✝
• HPSG.instReprVForm.repr HPSG.VForm.pastParticiple prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.VForm.pastParticiple")).group prec✝
• HPSG.instReprVForm.repr HPSG.VForm.presentParticiple prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.VForm.presentParticiple")).group prec✝

instance HPSG.instReprVForm : Repr VForm

Equations

• HPSG.instReprVForm = { reprPrec := HPSG.instReprVForm.repr }

instance HPSG.instDecidableEqVForm : DecidableEq VForm

Equations

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

inductive HPSG.Inv : Type

The INV(erted) feature for subject-aux inversion.

• plus : Inv
• minus : Inv

def HPSG.instReprInv.repr : Inv → Nat → Std.Format

Equations

• HPSG.instReprInv.repr HPSG.Inv.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Inv.plus")).group prec✝
• HPSG.instReprInv.repr HPSG.Inv.minus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Inv.minus")).group prec✝

instance HPSG.instReprInv : Repr Inv

Equations

• HPSG.instReprInv = { reprPrec := HPSG.instReprInv.repr }

instance HPSG.instDecidableEqInv : DecidableEq Inv

Equations

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

inductive HPSG.Mode : Type

The MODE feature on CONTENT, per @cite{sag-wasow-bender-2003} Ch. 7.

SWB2003 uses MODE to classify the semantic type of CONTENT:

• ref: referential — pronouns, R-expressions, nouns
• ana: anaphoric — reflexives, reciprocals
• prop: propositional — declarative clauses
• ques: question — interrogative clauses
• dir: directive — imperative clauses
• noneMode: for elements with no MODE specification

• ref : Mode
• ana : Mode
• prop : Mode
• ques : Mode
• dir : Mode
• noneMode : Mode

def HPSG.instReprMode.repr : Mode → Nat → Std.Format

Equations

• HPSG.instReprMode.repr HPSG.Mode.ref prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Mode.ref")).group prec✝
• HPSG.instReprMode.repr HPSG.Mode.ana prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Mode.ana")).group prec✝
• HPSG.instReprMode.repr HPSG.Mode.prop prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Mode.prop")).group prec✝
• HPSG.instReprMode.repr HPSG.Mode.ques prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Mode.ques")).group prec✝
• HPSG.instReprMode.repr HPSG.Mode.dir prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Mode.dir")).group prec✝
• HPSG.instReprMode.repr HPSG.Mode.noneMode prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "HPSG.Mode.noneMode")).group prec✝

instance HPSG.instReprMode : Repr Mode

Equations

• HPSG.instReprMode = { reprPrec := HPSG.instReprMode.repr }

instance HPSG.instDecidableEqMode : DecidableEq Mode

Equations

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

def HPSG.instBEqMode.beq : Mode → Mode → Bool

Equations

• HPSG.instBEqMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance HPSG.instBEqMode : BEq Mode

Equations

• HPSG.instBEqMode = { beq := HPSG.instBEqMode.beq }

structure HPSG.HeadFeatures : Type

Head features (shared between head and phrase).

• vform : VForm
• inv : Inv
• aux : Bool

instance HPSG.instReprHeadFeatures : Repr HeadFeatures

Equations

• HPSG.instReprHeadFeatures = { reprPrec := HPSG.instReprHeadFeatures.repr }

def HPSG.instReprHeadFeatures.repr : HeadFeatures → Nat → Std.Format

Equations

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

instance HPSG.instDecidableEqHeadFeatures : DecidableEq HeadFeatures

Equations

• HPSG.instDecidableEqHeadFeatures = HPSG.instDecidableEqHeadFeatures.decEq

def HPSG.instDecidableEqHeadFeatures.decEq (x✝ x✝¹ : HeadFeatures) : Decidable (x✝ = x✝¹)

Equations

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

structure HPSG.ContentFeatures : Type

Content features for binding theory, per @cite{sag-wasow-bender-2003} Ch. 7.

SWB2003's binding theory uses MODE and ARG-ST outranking:

• Principle A: [MODE ana] must be outranked by a coindexed element
• Principle B: [MODE ref] must NOT be outranked by a coindexed element

This subsumes the Chomskyan three-principle system — both pronouns and R-expressions are [MODE ref], so Principle B handles both. No separate "Principle C" is needed.

• mode : Mode

  MODE feature: ana for anaphors, ref for referential NPs

• index : Option Nat

  Referential index (for coindexation)

def HPSG.instReprContentFeatures.repr : ContentFeatures → Nat → Std.Format

Equations

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

instance HPSG.instReprContentFeatures : Repr ContentFeatures

Equations

• HPSG.instReprContentFeatures = { reprPrec := HPSG.instReprContentFeatures.repr }

def HPSG.instDecidableEqContentFeatures.decEq (x✝ x✝¹ : ContentFeatures) : Decidable (x✝ = x✝¹)

Equations

• HPSG.instDecidableEqContentFeatures.decEq { mode := a, index := a_1 } { mode := b, index := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance HPSG.instDecidableEqContentFeatures : DecidableEq ContentFeatures

Equations

• HPSG.instDecidableEqContentFeatures = HPSG.instDecidableEqContentFeatures.decEq

def HPSG.instBEqContentFeatures.beq : ContentFeatures → ContentFeatures → Bool

Equations

• HPSG.instBEqContentFeatures.beq { mode := a, index := a_1 } { mode := b, index := b_1 } = (a == b && a_1 == b_1)
• HPSG.instBEqContentFeatures.beq x✝¹ x✝ = false

instance HPSG.instBEqContentFeatures : BEq ContentFeatures

Equations

• HPSG.instBEqContentFeatures = { beq := HPSG.instBEqContentFeatures.beq }

structure HPSG.Valence : Type

Valence features (what arguments are needed).

• subj : List UD.UPOS
• comps : List UD.UPOS

instance HPSG.instReprValence : Repr Valence

Equations

• HPSG.instReprValence = { reprPrec := HPSG.instReprValence.repr }

def HPSG.instReprValence.repr : Valence → Nat → Std.Format

Equations

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

def HPSG.instDecidableEqValence.decEq (x✝ x✝¹ : Valence) : Decidable (x✝ = x✝¹)

Equations

• HPSG.instDecidableEqValence.decEq { subj := a, comps := a_1 } { subj := b, comps := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance HPSG.instDecidableEqValence : DecidableEq Valence

Equations

• HPSG.instDecidableEqValence = HPSG.instDecidableEqValence.decEq

structure HPSG.Synsem : Type

The SYNSEM value (syntax-semantics bundle).

• cat : UD.UPOS
• head : HeadFeatures
• val : Valence
• cont : ContentFeatures
• mod : Option UD.UPOS

  MOD feature: what this sign modifies (none = not a modifier).

  Per @cite{pollard-sag-1994} Ch. 1, MOD is a HEAD feature that restricts what a modifier can combine with. Relative clauses have [MOD NP]; adjectives have [MOD N].

instance HPSG.instReprSynsem : Repr Synsem

Equations

• HPSG.instReprSynsem = { reprPrec := HPSG.instReprSynsem.repr }

def HPSG.instReprSynsem.repr : Synsem → Nat → Std.Format

Equations

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

structure HPSG.ArgSt : Type

ARG-ST: the ordered list of a word's arguments, per @cite{sag-wasow-bender-2003} Ch. 7.

ARG-ST = SPR ⊕ COMPS. Outranking is defined over position in this list: element i outranks element j iff i < j.

• args : List Synsem

def HPSG.instReprArgSt.repr : ArgSt → Nat → Std.Format

Equations

• HPSG.instReprArgSt.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "args" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.args)).group) " }"

instance HPSG.instReprArgSt : Repr ArgSt

Equations

• HPSG.instReprArgSt = { reprPrec := HPSG.instReprArgSt.repr }

def HPSG.Valence.toArgSt (v : Valence) : ArgSt

Build ARG-ST from valence (SPR ⊕ COMPS).

Equations

• v.toArgSt = { args := List.map (fun (c : UD.UPOS) => { cat := c }) (v.subj ++ v.comps) }

def HPSG.ArgSt.outranks (argSt : ArgSt) (i j : Nat) : Bool

Does element at position i outrank element at position j on ARG-ST?

Per @cite{sag-wasow-bender-2003}: "X outranks Y iff X precedes Y on some ARG-ST list."

Equations

• argSt.outranks i j = (decide (i < j) && decide (j < argSt.args.length))

inductive HPSG.Sign : Type

An HPSG sign: word or phrase with syntactic info.

• word : Word → Synsem → Sign
• phrase : List Sign → Synsem → Sign

instance HPSG.instReprSign : Repr Sign

Equations

• HPSG.instReprSign = { reprPrec := HPSG.instReprSign.repr }

partial def HPSG.instReprSign.repr : Sign → Nat → Std.Format

def HPSG.Sign.synsem : Sign → Synsem

Get the SYNSEM of a sign.

Equations

• (HPSG.Sign.word a a_1).synsem = a_1
• (HPSG.Sign.phrase a a_1).synsem = a_1

partial def HPSG.Sign.yield : Sign → List Word

Get the yield (word list) of a sign.

structure HPSG.HeadCompRule : Type

Head-Complement Schema: head combines with its complements.

• head : Sign
• comps : List Sign
• result : Sign
• compsMatch : self.head.synsem.val.comps = List.map (fun (x : Sign) => x.synsem.cat) self.comps
• hfp : self.result.synsem.cat = self.head.synsem.cat

  Head Feature Principle: result category = head category

structure HPSG.HeadSubjRule : Type

Head-Subject Schema: phrase combines with its subject.

• subj : Sign
• headPhrase : Sign
• result : Sign
• subjMatch : self.headPhrase.synsem.val.subj = [self.subj.synsem.cat]
• hfp : self.result.synsem.cat = self.headPhrase.synsem.cat

  Head Feature Principle: result category = head phrase category

structure HPSG.HeadModRule : Type

Head-Modifier Schema: head combines with a modifier.

Per @cite{sag-wasow-bender-2003} (46), a saturated head combines with a modifier whose MOD value matches the head's category. Used for adjective modification ("tall boy"), PP modification ("book on the table"), and relative clauses ("book that John read").

• headSign : Sign
• modifier : Sign
• result : Sign
• modMatch : self.modifier.synsem.mod = some self.headSign.synsem.cat

  The modifier's MOD value must match the head's category

• hfp : self.result.synsem.cat = self.headSign.synsem.cat

  Head Feature Principle: result category = head category

def HPSG.satisfiesInversionConstraint (s : Sign) : Prop

[INV +] requires aux-initial; [INV -] requires subject-initial.

Equations

• One or more equations did not get rendered due to their size.
• HPSG.satisfiesInversionConstraint (HPSG.Sign.word a a_1) = True

def HPSG.matrixQuestionRequiresInv (s : Sign) (ct : ClauseType) : Prop

Matrix questions require [INV +].

Equations

• HPSG.matrixQuestionRequiresInv s ct = (ct = ClauseType.matrixQuestion → s.synsem.head.inv = HPSG.Inv.plus)

def HPSG.embeddedQuestionProhibitsInv (s : Sign) (ct : ClauseType) : Prop

Embedded questions require [INV -].

Equations

• HPSG.embeddedQuestionProhibitsInv s ct = (ct = ClauseType.embeddedQuestion → s.synsem.head.inv = HPSG.Inv.minus)

structure HPSG.HPSGGrammar : Type

An HPSG grammar is a collection of signs with constraints.

• signs : List Sign
• wellFormed (s : Sign) : s ∈ self.signs → satisfiesInversionConstraint s

structure HPSG.HPSGDerivation (g : HPSGGrammar) : Type

HPSG derivations are signs that satisfy all constraints.

• sign : Sign
• clauseType : ClauseType
• inSign : self.sign ∈ g.signs
• invOk : satisfiesInversionConstraint self.sign
• matrixOk : matrixQuestionRequiresInv self.sign self.clauseType
• embeddedOk : embeddedQuestionProhibitsInv self.sign self.clauseType

instance HPSG.instGrammarHPSGGrammar : Grammar HPSGGrammar

HPSG Grammar instance.

Equations

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

def HPSG.invPlusImpliesAuxFirst (inv : Inv) (ws : List Word) : Prop

[INV +] correlates with aux-before-subject order.

Equations

• HPSG.invPlusImpliesAuxFirst inv ws = (inv = HPSG.Inv.plus → auxPrecedesSubject ws = true)

def HPSG.invMinusImpliesSubjectFirst (inv : Inv) (ws : List Word) : Prop

[INV -] correlates with subject-before-aux order.

Equations

• HPSG.invMinusImpliesSubjectFirst inv ws = (inv = HPSG.Inv.minus → subjectPrecedesAux ws = true)