def HPSG.matrixRequiresInvPlus (ct : ClauseType) (inv : Inv) : Prop

Matrix questions require [INV +]

Equations

• HPSG.matrixRequiresInvPlus ct inv = (ct = ClauseType.matrixQuestion → inv = HPSG.Inv.plus)

def HPSG.embeddedRequiresInvMinus (ct : ClauseType) (inv : Inv) : Prop

Embedded questions require [INV -]

Equations

• HPSG.embeddedRequiresInvMinus ct inv = (ct = ClauseType.embeddedQuestion → inv = HPSG.Inv.minus)

theorem HPSG.matrix_has_aux_before_subject (inv : Inv) (ws : List Word) (hct : matrixRequiresInvPlus ClauseType.matrixQuestion inv) (hord : invPlusImpliesAuxFirst inv ws) : auxPrecedesSubject ws = true

Matrix questions have aux before subject

theorem HPSG.embedded_has_subject_before_aux (inv : Inv) (ws : List Word) (hct : embeddedRequiresInvMinus ClauseType.embeddedQuestion inv) (hord : invMinusImpliesSubjectFirst inv ws) : subjectPrecedesAux ws = true

Embedded questions have subject before aux

structure HPSG.Clause : Type

A clause: words + INV feature + clause type

• words : List Word
• inv : Inv
• clauseType : ClauseType

def HPSG.wordOrderMatchesInv (c : Clause) : Prop

Word order must match INV feature

Equations

• HPSG.wordOrderMatchesInv c = (HPSG.invPlusImpliesAuxFirst c.inv c.words ∧ HPSG.invMinusImpliesSubjectFirst c.inv c.words)

def HPSG.wellFormed (c : Clause) : Prop

Well-formed clause

Equations

• HPSG.wellFormed c = (HPSG.wordOrderMatchesInv c ∧ HPSG.matrixRequiresInvPlus c.clauseType c.inv ∧ HPSG.embeddedRequiresInvMinus c.clauseType c.inv)

def HPSG.licenses (ws : List Word) (ct : ClauseType) : Prop

A word sequence is licensed for a clause type if some INV value works

Equations

• HPSG.licenses ws ct = ∃ (inv : HPSG.Inv), HPSG.wellFormed { words := ws, inv := inv, clauseType := ct }

theorem HPSG.licenses_matrix_aux_first (ws : List Word) (h : auxPrecedesSubject ws = true) : licenses ws ClauseType.matrixQuestion

Matrix questions with aux-first order are licensed

theorem HPSG.not_licenses_matrix_subject_first (ws : List Word) (h : auxPrecedesSubject ws = false) : ¬licenses ws ClauseType.matrixQuestion

Matrix questions with subject-first are NOT licensed

theorem HPSG.licenses_embedded_subject_first (ws : List Word) (h : subjectPrecedesAux ws = true) : licenses ws ClauseType.embeddedQuestion

Embedded questions with subject-first are licensed

theorem HPSG.not_licenses_embedded_aux_first (ws : List Word) (h : subjectPrecedesAux ws = false) : ¬licenses ws ClauseType.embeddedQuestion

Embedded questions with aux-first are NOT licensed