structure CCG.Equivalence.DerivEquiv (m : Semantics.Montague.Model) : Type

Two derivations are semantically equivalent iff they span the same substring, have the same category, and have the same meaning.

This defines equivalence for "spurious ambiguity" analysis.

• cat : Cat

  First derivation's category

• meaning₁ : m.interpTy (catToTy self.cat)

  First derivation's meaning

• meaning₂ : m.interpTy (catToTy self.cat)

  Second derivation's meaning

• meanings_eq : self.meaning₁ = self.meaning₂

  The meanings are equal

def CCG.Equivalence.semanticallyEquivalent {m : Semantics.Montague.Model} (cm₁ cm₂ : (c : Cat) × m.interpTy (catToTy c)) : Prop

Semantic equivalence for category-meaning pairs.

Equations

• CCG.Equivalence.semanticallyEquivalent cm₁ cm₂ = ∃ (h : cm₁.fst = cm₂.fst), h ▸ cm₁.snd = cm₂.snd

theorem CCG.Equivalence.sem_equiv_refl {m : Semantics.Montague.Model} (cm : (c : Cat) × m.interpTy (catToTy c)) : semanticallyEquivalent cm cm

Semantic equivalence is reflexive.

theorem CCG.Equivalence.sem_equiv_symm {m : Semantics.Montague.Model} (cm₁ cm₂ : (c : Cat) × m.interpTy (catToTy c)) : semanticallyEquivalent cm₁ cm₂ → semanticallyEquivalent cm₂ cm₁

Semantic equivalence is symmetric.

theorem CCG.Equivalence.sem_equiv_trans {m : Semantics.Montague.Model} (cm₁ cm₂ cm₃ : (c : Cat) × m.interpTy (catToTy c)) : semanticallyEquivalent cm₁ cm₂ → semanticallyEquivalent cm₂ cm₃ → semanticallyEquivalent cm₁ cm₃

Semantic equivalence is transitive.

theorem CCG.Equivalence.B_assoc {α β γ δ : Type} (f : γ → δ) (g : β → γ) (h : α → β) : Combinators.B (Combinators.B f g) h = Combinators.B f (Combinators.B g h)

B (composition) is associative: (f ∘ g) ∘ h = f ∘ (g ∘ h)

theorem CCG.Equivalence.B_assoc_apply {α β γ δ : Type} (f : γ → δ) (g : β → γ) (h : α → β) (x : α) : Combinators.B (Combinators.B f g) h x = Combinators.B f (Combinators.B g h) x

Associativity stated pointwise.

theorem CCG.Equivalence.composition_order_irrelevant {α β γ δ : Type} (f : γ → δ) (g : β → γ) (h : α → β) (x : α) : f (g (h x)) = Combinators.B f (Combinators.B g h) x

Consequence: Two ways of composing three functions yield the same result.

This is why "Harry thinks that Anna married" can be derived by:

1. (Harry ∘ thinks) ∘ (that ∘ (Anna ∘ married))
2. Harry ∘ (thinks ∘ that) ∘ (Anna ∘ married)
3. Harry ∘ (thinks ∘ (that ∘ Anna)) ∘ married ... etc.

All yield the same predicate-argument structure.

inductive CCG.Equivalence.BinTree : Type

A full binary tree represents a bracketing of items.

• leaf: A single item (no bracketing needed)
• node l r: A binary split (l r) combining two sub-bracketings

For n items, a full binary tree has n leaves and n-1 internal nodes.

• leaf : BinTree
• node : BinTree → BinTree → BinTree

instance CCG.Equivalence.instReprBinTree : Repr BinTree

Equations

• CCG.Equivalence.instReprBinTree = { reprPrec := CCG.Equivalence.instReprBinTree.repr }

def CCG.Equivalence.instReprBinTree.repr : BinTree → ℕ → Std.Format

Equations

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

instance CCG.Equivalence.instDecidableEqBinTree : DecidableEq BinTree

Equations

• CCG.Equivalence.instDecidableEqBinTree = CCG.Equivalence.instDecidableEqBinTree.decEq

def CCG.Equivalence.instDecidableEqBinTree.decEq (x✝ x✝¹ : BinTree) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CCG.Equivalence.instDecidableEqBinTree.decEq CCG.Equivalence.BinTree.leaf CCG.Equivalence.BinTree.leaf = isTrue ⋯
• CCG.Equivalence.instDecidableEqBinTree.decEq CCG.Equivalence.BinTree.leaf (a.node a_1) = isFalse ⋯
• CCG.Equivalence.instDecidableEqBinTree.decEq (a.node a_1) CCG.Equivalence.BinTree.leaf = isFalse ⋯

def CCG.Equivalence.BinTree.leaves : BinTree → ℕ

Number of leaves in a binary tree (= number of items being bracketed).

Equations

• CCG.Equivalence.BinTree.leaf.leaves = 1
• (a.node a_1).leaves = a.leaves + a_1.leaves

def CCG.Equivalence.BinTree.nodes : BinTree → ℕ

Number of internal nodes (= number of binary operations / compositions).

Equations

• CCG.Equivalence.BinTree.leaf.nodes = 0
• (a.node a_1).nodes = 1 + a.nodes + a_1.nodes

theorem CCG.Equivalence.BinTree.nodes_eq_leaves_minus_one (t : BinTree) : t.nodes + 1 = t.leaves

A tree with n leaves has n-1 internal nodes.

def CCG.Equivalence.allTreesWithLeavesAux (n fuel : ℕ) : List BinTree

Generate all binary trees with exactly n leaves (helper with explicit termination).

Equations

• One or more equations did not get rendered due to their size.
• CCG.Equivalence.allTreesWithLeavesAux x✝ 0 = []
• CCG.Equivalence.allTreesWithLeavesAux 0 x✝ = []
• CCG.Equivalence.allTreesWithLeavesAux 1 x✝ = [CCG.Equivalence.BinTree.leaf]

def CCG.Equivalence.allTreesWithLeaves (n : ℕ) : List BinTree

Generate all binary trees with exactly n leaves.

Equations

• CCG.Equivalence.allTreesWithLeaves n = CCG.Equivalence.allTreesWithLeavesAux n n

def CCG.Equivalence.catalan : ℕ → ℕ

Catalan numbers via the closed formula.

Equations

• CCG.Equivalence.catalan 0 = 1
• CCG.Equivalence.catalan n.succ = 2 * (2 * n + 1) * CCG.Equivalence.catalan n / (n + 2)

def CCG.Equivalence.countBracketingsAux (n fuel : ℕ) : ℕ

Count bracketings directly (helper with explicit termination).

Equations

• One or more equations did not get rendered due to their size.
• CCG.Equivalence.countBracketingsAux x✝ 0 = 0
• CCG.Equivalence.countBracketingsAux 0 x✝ = 0
• CCG.Equivalence.countBracketingsAux 1 x✝ = 1

def CCG.Equivalence.countBracketings (n : ℕ) : ℕ

Count bracketings directly (matches Catalan structure).

Equations

• CCG.Equivalence.countBracketings n = CCG.Equivalence.countBracketingsAux n n

theorem CCG.Equivalence.catalan_counts_bracketings_1 : countBracketings 1 = catalan 0

countBracketings n = catalan (n-1) for n >= 1.

Verified computationally for small values.

theorem CCG.Equivalence.catalan_counts_bracketings_2 : countBracketings 2 = catalan 1

theorem CCG.Equivalence.catalan_counts_bracketings_3 : countBracketings 3 = catalan 2

theorem CCG.Equivalence.catalan_counts_bracketings_4 : countBracketings 4 = catalan 3

theorem CCG.Equivalence.catalan_counts_bracketings_5 : countBracketings 5 = catalan 4

theorem CCG.Equivalence.catalan_counts_bracketings_6 : countBracketings 6 = catalan 5

theorem CCG.Equivalence.tree_count_eq_bracketings_1 : (allTreesWithLeaves 1).length = countBracketings 1

allTreesWithLeaves generates exactly countBracketings trees.

The tree enumeration function produces the correct count.

theorem CCG.Equivalence.tree_count_eq_bracketings_2 : (allTreesWithLeaves 2).length = countBracketings 2

theorem CCG.Equivalence.tree_count_eq_bracketings_3 : (allTreesWithLeaves 3).length = countBracketings 3

theorem CCG.Equivalence.tree_count_eq_bracketings_4 : (allTreesWithLeaves 4).length = countBracketings 4

theorem CCG.Equivalence.tree_count_eq_bracketings_5 : (allTreesWithLeaves 5).length = countBracketings 5

theorem CCG.Equivalence.tree_count_eq_catalan_1 : (allTreesWithLeaves 1).length = catalan 0

Combined: tree count equals Catalan number.

theorem CCG.Equivalence.tree_count_eq_catalan_2 : (allTreesWithLeaves 2).length = catalan 1

theorem CCG.Equivalence.tree_count_eq_catalan_3 : (allTreesWithLeaves 3).length = catalan 2

theorem CCG.Equivalence.tree_count_eq_catalan_4 : (allTreesWithLeaves 4).length = catalan 3

theorem CCG.Equivalence.tree_count_eq_catalan_5 : (allTreesWithLeaves 5).length = catalan 4

def CCG.Equivalence.bracketings (n : ℕ) : ℕ

The number of bracketings of n items equals the (n-1)th Catalan number.

Equations

• CCG.Equivalence.bracketings n = if n ≤ 1 then 1 else CCG.Equivalence.catalan (n - 1)

theorem CCG.Equivalence.bracketings_eq_tree_count_1 : bracketings 1 = (allTreesWithLeaves 1).length

theorem CCG.Equivalence.bracketings_eq_tree_count_2 : bracketings 2 = (allTreesWithLeaves 2).length

theorem CCG.Equivalence.bracketings_eq_tree_count_3 : bracketings 3 = (allTreesWithLeaves 3).length

theorem CCG.Equivalence.bracketings_eq_tree_count_4 : bracketings 4 = (allTreesWithLeaves 4).length

theorem CCG.Equivalence.bracketings_eq_tree_count_5 : bracketings 5 = (allTreesWithLeaves 5).length

theorem CCG.Equivalence.bracketings_5_eq_14 : bracketings 5 = 14

theorem CCG.Equivalence.bracketings_6_eq_42 : bracketings 6 = 42

inductive CCG.Equivalence.BracketStrategy : Type

A derivation strategy selects bracketings.

• leftAssoc : BracketStrategy
• rightAssoc : BracketStrategy
• balanced : BracketStrategy

instance CCG.Equivalence.instDecidableEqBracketStrategy : DecidableEq BracketStrategy

Equations

• CCG.Equivalence.instDecidableEqBracketStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CCG.Equivalence.instReprBracketStrategy.repr : BracketStrategy → ℕ → Std.Format

Equations

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

instance CCG.Equivalence.instReprBracketStrategy : Repr BracketStrategy

Equations

• CCG.Equivalence.instReprBracketStrategy = { reprPrec := CCG.Equivalence.instReprBracketStrategy.repr }

theorem CCG.Equivalence.strategy_irrelevant {α : Type} (f g h : α → α) (x : α) : ∀ (x✝ : BracketStrategy), f (g (h x)) = f (g (h x))

Under purely compositional derivation, all strategies yield the same meaning.

structure CCG.Equivalence.ChartEntry (m : Semantics.Montague.Model) : Type

A chart entry: category + meaning for a span.

• leftPos : ℕ
• rightPos : ℕ
• cat : Cat
• meaning : m.interpTy (catToTy self.cat)

def CCG.Equivalence.chartEntriesMatch {m : Semantics.Montague.Model} (e₁ e₂ : ChartEntry m) : Prop

Two chart entries match if they have the same span, category, and meaning.

Equations

• CCG.Equivalence.chartEntriesMatch e₁ e₂ = (e₁.leftPos = e₂.leftPos ∧ e₁.rightPos = e₂.rightPos ∧ ∃ (h : e₁.cat = e₂.cat), h ▸ e₁.meaning = e₂.meaning)

def CCG.Equivalence.chartEntriesSameCat {m : Semantics.Montague.Model} (e₁ e₂ : ChartEntry m) : Bool

The matching relation is decidable for categories (not meanings in general).

Equations

• CCG.Equivalence.chartEntriesSameCat e₁ e₂ = (e₁.leftPos == e₂.leftPos && e₁.rightPos == e₂.rightPos && e₁.cat == e₂.cat)

structure CCG.Equivalence.EquivalenceClass (m : Semantics.Montague.Model) : Type

An equivalence class of derivations: all have the same meaning.

• cat : Cat
• meaning : m.interpTy (catToTy self.cat)

def CCG.Equivalence.reallyAmbiguous {m : Semantics.Montague.Model} (classes : List (EquivalenceClass m)) : Prop

Real ambiguity: multiple equivalence classes for the same string.

Equations

• CCG.Equivalence.reallyAmbiguous classes = (classes.length > 1)

def CCG.Equivalence.spuriouslyAmbiguous {m : Semantics.Montague.Model} (derivCount : ℕ) (classes : List (EquivalenceClass m)) : Prop

Spuriously ambiguous: multiple derivations but only one equivalence class.

Equations

• CCG.Equivalence.spuriouslyAmbiguous derivCount classes = (derivCount > 1 ∧ classes.length = 1)