Grammar

Grammar comparison interface and empirical testing infrastructure.

Defines:

• ClauseType — sentence types (declarative, question variants)
• Grammar typeclass — assigns derivations to strings
• MinimalPair / PhenomenonData — word-based grammaticality testing
• SentencePair / StringPhenomenonData — theory-neutral string-based testing
• Capture predicates and agreement theorems

structure V2Data : Type

Theory-neutral V2 data: for each clause type, whether verb movement to second position is observed. Used by Fragment V2 files for descriptive encoding of cross-Germanic V2 variation.

• name : String
• declV2 : Bool
• whQV2 : Bool
• ynQV2 : Bool
• exclV2 : Bool
• impV2 : Bool
• embFinV2 : Bool
• embQV2 : Bool

def instReprV2Data.repr : V2Data → Nat → Std.Format

Equations

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

instance instReprV2Data : Repr V2Data

Equations

• instReprV2Data = { reprPrec := instReprV2Data.repr }

def instBEqV2Data.beq : V2Data → V2Data → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqV2Data.beq x✝¹ x✝ = false

instance instBEqV2Data : BEq V2Data

Equations

• instBEqV2Data = { beq := instBEqV2Data.beq }

instance instDecidableEqV2Data : DecidableEq V2Data

Equations

• instDecidableEqV2Data = instDecidableEqV2Data.decEq

def instDecidableEqV2Data.decEq (x✝ x✝¹ : V2Data) : Decidable (x✝ = x✝¹)

Equations

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

inductive ClauseType : Type

Clause types - determines constraints on word order.

• declarative : ClauseType
• matrixQuestion : ClauseType
• embeddedQuestion : ClauseType
• echo : ClauseType

instance instReprClauseType : Repr ClauseType

Equations

• instReprClauseType = { reprPrec := instReprClauseType.repr }

def instReprClauseType.repr : ClauseType → Nat → Std.Format

Equations

• instReprClauseType.repr ClauseType.declarative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClauseType.declarative")).group prec✝
• instReprClauseType.repr ClauseType.matrixQuestion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClauseType.matrixQuestion")).group prec✝
• instReprClauseType.repr ClauseType.embeddedQuestion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClauseType.embeddedQuestion")).group prec✝
• instReprClauseType.repr ClauseType.echo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClauseType.echo")).group prec✝

instance instDecidableEqClauseType : DecidableEq ClauseType

Equations

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

def precedes (p q : Word → Bool) (ws : List Word) : Bool

Does some word satisfying p precede some word satisfying q?

Equations

• precedes p q ws = match List.findIdx? p ws, List.findIdx? q ws with | some i, some j => decide (i < j) | x, x_1 => false

def isSubjectCat (c : UD.UPOS) : Bool

Is this a nominal category that can be a subject?

Equations

• isSubjectCat c = (c == UD.UPOS.PROPN || c == UD.UPOS.NOUN || c == UD.UPOS.PRON)

def isSubject (w : Word) : Bool

Is this word a non-wh subject?

Equations

• isSubject w = (isSubjectCat w.cat && !w.features.wh)

def auxPrecedesSubject (ws : List Word) : Bool

Does the auxiliary precede the subject?

Equations

• auxPrecedesSubject ws = precedes (fun (x : Word) => x.cat == UD.UPOS.AUX) isSubject ws

def subjectPrecedesAux (ws : List Word) : Bool

Does the subject precede the auxiliary?

Equations

• subjectPrecedesAux ws = precedes isSubject (fun (x : Word) => x.cat == UD.UPOS.AUX) ws

class Grammar (G : Type) : Type 1

A Grammar assigns derivations to strings. Derivations are proof objects.

• Derivation : Type

  The type of derivations/analyses this grammar produces

• realizes : Derivation G → List Word → ClauseType → Prop

  Whether a derivation yields a given string with given clause type

• derives : G → List Word → ClauseType → Prop

  Whether the grammar can produce some derivation for a string

structure MinimalPair : Type

A minimal pair: grammatical vs ungrammatical, with context

• grammatical : List Word
• ungrammatical : List Word
• clauseType : ClauseType
• description : String
• citation : Option String

structure PhenomenonData : Type

Collection of minimal pairs for a phenomenon

• name : String
• pairs : List MinimalPair
• generalization : String

def capturesMinimalPairBy (pred : List Word → Bool) (pair : MinimalPair) : Bool

Check if a grammaticality predicate captures a minimal pair.

Captures the pair iff the predicate accepts the grammatical sentence and rejects the ungrammatical sentence.

Equations

• capturesMinimalPairBy pred pair = (pred pair.grammatical && !pred pair.ungrammatical)

def capturesPhenomenonData (pred : List Word → Bool) (phenom : PhenomenonData) : Bool

Check if a grammaticality predicate captures all minimal pairs in a phenomenon dataset.

Equations

• capturesPhenomenonData pred phenom = phenom.pairs.all (capturesMinimalPairBy pred)

def Grammar.capturesPair (G : Type) [Grammar G] (g : G) (pair : MinimalPair) : Prop

A grammar captures a minimal pair if it derives the good one and blocks the bad one

Equations

• Grammar.capturesPair G g pair = (Grammar.derives g pair.grammatical pair.clauseType ∧ ¬Grammar.derives g pair.ungrammatical pair.clauseType)

def Grammar.capturesPhenomenon (G : Type) [Grammar G] (g : G) (phenom : PhenomenonData) : Prop

A grammar captures a phenomenon if it captures all its minimal pairs

Equations

• Grammar.capturesPhenomenon G g phenom = ∀ (pair : MinimalPair), pair ∈ phenom.pairs → Grammar.capturesPair G g pair

theorem grammars_agree_on_phenomenon (G₁ G₂ : Type) [Grammar G₁] [Grammar G₂] (g₁ : G₁) (g₂ : G₂) (phenom : PhenomenonData) (h₁ : Grammar.capturesPhenomenon G₁ g₁ phenom) (h₂ : Grammar.capturesPhenomenon G₂ g₂ phenom) (pair : MinimalPair) (hp : pair ∈ phenom.pairs) : Grammar.derives g₁ pair.grammatical pair.clauseType ↔ Grammar.derives g₂ pair.grammatical pair.clauseType

If two grammars both capture a phenomenon, they agree on grammatical sentences

structure SentencePair : Type

String-based minimal pair for theory-neutral phenomena.

Unlike MinimalPair which uses List Word (requiring feature specifications), this type uses raw strings that can be parsed by any theory. This keeps empirical data in Phenomena/ free from theoretical commitments.

• grammatical : String

  The grammatical sentence

• ungrammatical : String

  The ungrammatical sentence

• clauseType : ClauseType

  Clause type (declarative, question, etc.)

• description : String

  Description of what the pair tests

• citation : Option String

  Optional citation for the data

def instReprSentencePair.repr : SentencePair → Nat → Std.Format

Equations

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

instance instReprSentencePair : Repr SentencePair

Equations

• instReprSentencePair = { reprPrec := instReprSentencePair.repr }

instance instBEqSentencePair : BEq SentencePair

Equations

• instBEqSentencePair = { beq := instBEqSentencePair.beq }

def instBEqSentencePair.beq : SentencePair → SentencePair → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqSentencePair.beq x✝¹ x✝ = false

structure StringPhenomenonData : Type

String-based phenomenon data for theory-neutral representation.

This is the string-based analogue of PhenomenonData. Phenomena files should use this type so that empirical data is decoupled from any particular grammatical theory's representation.

• name : String

  Name of the phenomenon

• pairs : List SentencePair

  List of minimal pairs

• generalization : String

  Generalization captured by this data

instance instReprStringPhenomenonData : Repr StringPhenomenonData

Equations

• instReprStringPhenomenonData = { reprPrec := instReprStringPhenomenonData.repr }

def instReprStringPhenomenonData.repr : StringPhenomenonData → Nat → Std.Format

Equations

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