Asudeh (2022): Glue Semantics

In Glue Semantics a word contributes meaning constructors, lambda terms paired with formulas of the implicational fragment of linear logic, and a sentence means what a proof of its clause from these premises computes, implication elimination being function application and introduction abstraction. Linear logic lacks weakening and contraction, so a proof uses each premise exactly once, but keeps commutativity, so word order does not constrain composition. Asudeh's examples follow: Finnish Join vettä and English I drank water spread the same three premises over two and three words, and Everybody loves somebody has one syntactic structure but two proofs, one per scope reading. Asudeh also takes resource sensitivity to do the work of LFG's Completeness and Coherence, which the Dutch cross-serial clauses of Bresnan, Kaplan, Peters and Zaenen bear out.

Main statements

• Term.Linear.rename_perm, Term.not_linear_weaken, Term.Linear.not_linear_contract: reordering premises keeps a proof linear, while weakening and contraction never do.
• Term.Linear.count_eq, derivable_iff_complete_coherent: linear proofs preserve the count of every atom, and a Dutch clause's premises have a proof exactly when its f-structure is complete and coherent.
• finnish_english: the Finnish and English sentences instantiate the same premises.
• card_correct_loves, surface_eval, inverse_eval, interp_qr_eq_eval: Everybody loves somebody has exactly two correct proof nets, and its two proofs mean its surface and inverse readings, which Heim and Kratzer derive from two Quantifier Raising trees.

Implementation notes

• Proofs are intrinsically typed λ-terms over a list of premises; the structural rules rename premise positions, and Term.Linear counts uses.
• The quantifiers' scope variable ∀S is instantiated to the clause, as in the paper's proofs.
• A Dutch control verb takes its complement as a property, so the object it shares is used twice only in the meaning.
• Proof nets use Danos and Regnier's criterion on mathlib's SimpleGraph.IsTree.

TODO

• Prove derivable_iff_exists_correct, by desequentialization and sequentialization, and define the net of a linear term, so that card_correct_loves counts proofs up to βη.
• Planarity of linkings characterizes the Lambek calculus, but stating it needs directional types, which Glue's ⊸ lacks.

References

• [Asu22]
• [Gir87]
• [KS85]
• [KB82]
• [DR89]
• [BKPZ82]
• [HK98]

Proofs as linear terms

inductive Asudeh2022.GlueTy (α : Type u_1) : Type u_1

Formulas of the implicational fragment of linear logic over instantiated atoms.

• atom {α : Type u_1} (a : α) : GlueTy α
• lolli {α : Type u_1} (A B : GlueTy α) : GlueTy α

def Asudeh2022.instDecidableEqGlueTy.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : GlueTy α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Asudeh2022.instDecidableEqGlueTy.decEq (Asudeh2022.GlueTy.atom a) (Asudeh2022.GlueTy.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Asudeh2022.instDecidableEqGlueTy.decEq (Asudeh2022.GlueTy.atom a) (A ⊸ B) = isFalse ⋯
• Asudeh2022.instDecidableEqGlueTy.decEq (A ⊸ B) (Asudeh2022.GlueTy.atom a) = isFalse ⋯

@[instance_reducible]

instance Asudeh2022.instDecidableEqGlueTy {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (GlueTy α✝)

Equations

• Asudeh2022.instDecidableEqGlueTy = Asudeh2022.instDecidableEqGlueTy.decEq

@[instance_reducible]

instance Asudeh2022.instReprGlueTy {α✝ : Type u_1} [Repr α✝] : Repr (GlueTy α✝)

Equations

• Asudeh2022.instReprGlueTy = { reprPrec := Asudeh2022.instReprGlueTy.repr }

def Asudeh2022.instReprGlueTy.repr {α✝ : Type u_1} [Repr α✝] : GlueTy α✝ → ℕ → Std.Format

Equations

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

def Asudeh2022.«term_⊸_» : Lean.TrailingParserDescr

Equations

• Asudeh2022.«term_⊸_» = Lean.ParserDescr.trailingNode `Asudeh2022.«term_⊸_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊸ ") (Lean.ParserDescr.cat `term 25))

inductive Asudeh2022.Term {α : Type u_1} : List (GlueTy α) → GlueTy α → Type u_1

A proof from a list of premises, as a λ-term. A variable names a position of the list, application is implication elimination, and abstraction discharges a hypothesis appended to the list.

• var {α : Type u_1} {Γ : List (GlueTy α)} (n : ℕ) {T : GlueTy α} (h : Γ[n]? = some T) : Term Γ T
• app {α : Type u_1} {Γ : List (GlueTy α)} {A B : GlueTy α} : Term Γ (A ⊸ B) → Term Γ A → Term Γ B
• lam {α : Type u_1} {Γ : List (GlueTy α)} (A : GlueTy α) {B : GlueTy α} : Term (Γ ++ [A]) B → Term Γ (A ⊸ B)

def Asudeh2022.Term.uses {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} : Term Γ T → List ℕ

The positions a proof uses, with repetition.

Equations

• (Asudeh2022.Term.var n h).uses = [n]
• (f.app a).uses = f.uses ++ a.uses
• (Asudeh2022.Term.lam A b).uses = b.uses

def Asudeh2022.Term.HypLinear {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} : Term Γ T → Prop

Every hypothesis is used exactly once.

Equations

• (Asudeh2022.Term.var n h).HypLinear = True
• (f.app a).HypLinear = (f.HypLinear ∧ a.HypLinear)
• (Asudeh2022.Term.lam A b).HypLinear = (List.count Γ.length b.uses = 1 ∧ b.HypLinear)

@[instance_reducible]

instance Asudeh2022.Term.decHypLinear {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} (t : Term Γ T) : Decidable t.HypLinear

Equations

• (Asudeh2022.Term.var n h).decHypLinear = isTrue trivial
• (f.app a).decHypLinear = instDecidableAnd
• (Asudeh2022.Term.lam A b).decHypLinear = instDecidableAnd

def Asudeh2022.Term.Linear {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} (t : Term Γ T) : Prop

A proof is linear if it uses every premise and every hypothesis exactly once.

Equations

• t.Linear = ((∀ i < Γ.length, List.count i t.uses = 1) ∧ t.HypLinear)

@[instance_reducible]

instance Asudeh2022.instDecidableLinear {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} (t : Term Γ T) : Decidable t.Linear

Equations

• Asudeh2022.instDecidableLinear t = { decide := decide (∀ i < Γ.length, List.count i t.uses = 1) && decide t.HypLinear, reflects_decide := ⋯ }

Curry–Howard evaluation

def Asudeh2022.GlueTy.denote {α : Type u_1} (D : α → Type) : GlueTy α → Type

The type of meanings a formula pairs with.

Equations

• Asudeh2022.GlueTy.denote D (Asudeh2022.GlueTy.atom a) = D a
• Asudeh2022.GlueTy.denote D (A ⊸ B) = (Asudeh2022.GlueTy.denote D A → Asudeh2022.GlueTy.denote D B)

inductive Asudeh2022.Env {α : Type u_1} (D : α → Type) : List (GlueTy α) → Type u_1

Meanings for the premises of a list.

• nil {α : Type u_1} {D : α → Type} : Env D []
• cons {α : Type u_1} {D : α → Type} {T : GlueTy α} {Γ : List (GlueTy α)} : GlueTy.denote D T → Env D Γ → Env D (T :: Γ)

def Asudeh2022.Env.get {α : Type u_1} {D : α → Type} {Γ : List (GlueTy α)} : Env D Γ → (n : ℕ) → {T : GlueTy α} → Γ[n]? = some T → GlueTy.denote D T

The meaning at a position.

Equations

• (Asudeh2022.Env.cons v a).get 0 x_1 = ⋯ ▸ v
• (Asudeh2022.Env.cons a ρ).get n.succ x_1 = ρ.get n x_1

def Asudeh2022.Env.snoc {α : Type u_1} {D : α → Type} {T : GlueTy α} {Γ : List (GlueTy α)} : Env D Γ → GlueTy.denote D T → Env D (Γ ++ [T])

The meanings extended by one, for a hypothesis.

Equations

• Asudeh2022.Env.nil.snoc x✝ = Asudeh2022.Env.cons x✝ Asudeh2022.Env.nil
• (Asudeh2022.Env.cons u ρ).snoc x✝ = Asudeh2022.Env.cons u (ρ.snoc x✝)

theorem Asudeh2022.Env.get_congr {α : Type u_1} {D : α → Type} {Γ : List (GlueTy α)} (ρ : Env D Γ) {n m : ℕ} {T : GlueTy α} (e : n = m) (h : Γ[n]? = some T) (h' : Γ[m]? = some T) : ρ.get n h = ρ.get m h'

theorem Asudeh2022.Env.get_snoc_of_lt {α : Type u_1} {D : α → Type} {A B : GlueTy α} {Γ : List (GlueTy α)} (ρ : Env D Γ) (v : GlueTy.denote D A) {n : ℕ} : n < Γ.length → ∀ (h : (Γ ++ [A])[n]? = some B) (h' : Γ[n]? = some B), (ρ.snoc v).get n h = ρ.get n h'

theorem Asudeh2022.Env.get_snoc_of_eq {α : Type u_1} {D : α → Type} {A : GlueTy α} {Γ : List (GlueTy α)} (ρ : Env D Γ) (v : GlueTy.denote D A) {n : ℕ} : n = Γ.length → ∀ (h : (Γ ++ [A])[n]? = some A), (ρ.snoc v).get n h = v

def Asudeh2022.Term.eval {α : Type u_1} {D : α → Type} {Γ : List (GlueTy α)} {T : GlueTy α} : Term Γ T → Env D Γ → GlueTy.denote D T

The meaning a proof assembles, applying for each elimination and abstracting for each introduction.

Equations

• (Asudeh2022.Term.var n h).eval x✝ = x✝.get n h
• (f.app a).eval x✝ = f.eval x✝ (a.eval x✝)
• (Asudeh2022.Term.lam A b).eval x✝ = fun (v : Asudeh2022.GlueTy.denote D A) => b.eval (x✝.snoc v)

Structural rules

Weakening, contraction and commutativity act on a proof by renaming the positions of its premises. Commutativity preserves linearity and meaning; weakening and contraction destroy linearity, so every premise is used exactly once. Asudeh takes this resource sensitivity to do the work of Klein and Sag's bounded closure and of Kaplan and Bresnan's Completeness and Coherence.

def Asudeh2022.liftPos (m m' : ℕ) (f : ℕ → ℕ) (n : ℕ) : ℕ

Under a binder, a renaming f of m premises into m' extends to the hypotheses past the premises, which shift to follow the new ones.

Equations

• Asudeh2022.liftPos m m' f n = if n < m then f n else n - m + m'

theorem Asudeh2022.liftPos_liftPos (m m' : ℕ) (f : ℕ → ℕ) : liftPos (m + 1) (m' + 1) (liftPos m m' f) = liftPos m m' f

theorem Asudeh2022.liftPos_getElem? {α : Type u_1} {Γ Γ' : List (GlueTy α)} {f : ℕ → ℕ} (hf : ∀ (n : ℕ) (B : GlueTy α), Γ[n]? = some B → Γ'[f n]? = some B) (A : GlueTy α) (n : ℕ) (B : GlueTy α) : (Γ ++ [A])[n]? = some B → (Γ' ++ [A])[liftPos Γ.length Γ'.length f n]? = some B

def Asudeh2022.Term.rename {α : Type u_1} {Γ Γ' : List (GlueTy α)} (f : ℕ → ℕ) : (∀ (n : ℕ) (B : GlueTy α), Γ[n]? = some B → Γ'[f n]? = some B) → {T : GlueTy α} → Term Γ T → Term Γ' T

Rename the premises of a proof along a map of positions that preserves their formulas.

Equations

• Asudeh2022.Term.rename x_2 x_3 (Asudeh2022.Term.var n h) = Asudeh2022.Term.var (x_2 n) ⋯
• Asudeh2022.Term.rename x_2 x_3 (s.app a) = (Asudeh2022.Term.rename x_2 x_3 s).app (Asudeh2022.Term.rename x_2 x_3 a)
• Asudeh2022.Term.rename x_2 x_3 (Asudeh2022.Term.lam A b) = Asudeh2022.Term.lam A (Asudeh2022.Term.rename (Asudeh2022.liftPos x.length x_1.length x_2) ⋯ b)

theorem Asudeh2022.Term.uses_rename {α : Type u_1} {Γ Γ' : List (GlueTy α)} (f : ℕ → ℕ) (hf : ∀ (n : ℕ) (B : GlueTy α), Γ[n]? = some B → Γ'[f n]? = some B) {T : GlueTy α} (t : Term Γ T) : (rename f hf t).uses = List.map (liftPos Γ.length Γ'.length f) t.uses

theorem Asudeh2022.Term.HypLinear.rename {α : Type u_1} {Γ Γ' : List (GlueTy α)} {f : ℕ → ℕ} (hf : ∀ (n : ℕ) (B : GlueTy α), Γ[n]? = some B → Γ'[f n]? = some B) {T : GlueTy α} {t : Term Γ T} (ht : t.HypLinear) : (Term.rename f hf t).HypLinear

theorem Asudeh2022.Term.Linear.rename_perm {α : Type u_1} {Γ Γ' : List (GlueTy α)} {T : GlueTy α} {t : Term Γ T} (ht : t.Linear) (σ : Equiv.Perm ℕ) (hσ : ∀ (n : ℕ), Γ.length ≤ n → σ n = n) (hlen : Γ'.length = Γ.length) (hf : ∀ (n : ℕ) (B : GlueTy α), Γ[n]? = some B → Γ'[σ n]? = some B) : (rename (⇑σ) hf t).Linear

Reordering the premises of a linear proof leaves it linear, so commutativity holds.

theorem Asudeh2022.Term.eval_rename {α : Type u_1} {D : α → Type} {Γ Γ' : List (GlueTy α)} (f : ℕ → ℕ) (hf : ∀ (n : ℕ) (B : GlueTy α), Γ[n]? = some B → Γ'[f n]? = some B) {T : GlueTy α} (t : Term Γ T) (ρ : Env D Γ) (ρ' : Env D Γ') (hρ : ∀ (n : ℕ) (B : GlueTy α) (h : Γ[n]? = some B), ρ'.get (f n) ⋯ = ρ.get n h) : (rename f hf t).eval ρ' = t.eval ρ

Renaming the premises of a proof, with meanings that agree position by position, does not change what it means.

theorem Asudeh2022.getElem?_append_left_of_eq_some {α : Type u_1} {Γ : List (GlueTy α)} {A : GlueTy α} {n : ℕ} {B : GlueTy α} (h : Γ[n]? = some B) : (Γ ++ [A])[n]? = some B

def Asudeh2022.Term.weaken {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} (A : GlueTy α) (t : Term Γ T) : Term (Γ ++ [A]) T

Weakening adds a premise that the proof does not use.

Equations

• Asudeh2022.Term.weaken A t = Asudeh2022.Term.rename id ⋯ t

theorem Asudeh2022.Term.not_linear_weaken {α : Type u_1} {Γ : List (GlueTy α)} {T : GlueTy α} (A : GlueTy α) (t : Term Γ T) : ¬(weaken A t).Linear

A weakened proof is never linear, since its added premise is left over.

theorem Asudeh2022.contract_getElem? {α : Type u_1} {Γ : List (GlueTy α)} {A : GlueTy α} (n : ℕ) (B : GlueTy α) : (Γ ++ [A, A])[n]? = some B → (Γ ++ [A])[min n Γ.length]? = some B

def Asudeh2022.Term.contract {α : Type u_1} {Γ : List (GlueTy α)} {A T : GlueTy α} (t : Term (Γ ++ [A, A]) T) : Term (Γ ++ [A]) T

Contraction lets one premise stand for two occurrences of its formula.

Equations

• t.contract = Asudeh2022.Term.rename (fun (n : ℕ) => min n Γ.length) ⋯ t

theorem Asudeh2022.Term.Linear.not_linear_contract {α : Type u_1} {Γ : List (GlueTy α)} {A T : GlueTy α} {t : Term (Γ ++ [A, A]) T} (ht : t.Linear) : ¬t.contract.Linear

Contracting a linear proof never yields a linear one, since the merged premise is used twice.

Count invariance

The count of an atom in a formula is its positive occurrences less its negative ones. A linear proof preserves counts, so a premise multiset whose counts differ from its conclusion's has no linear proof at all.

def Asudeh2022.Derivable {α : Type u_1} (M : Multiset (GlueTy α)) (C : GlueTy α) : Prop

A formula is derivable from a multiset of premises if some ordering of them has a linear proof of it.

Equations

• Asudeh2022.Derivable M C = ∃ (Γ : List (Asudeh2022.GlueTy α)), ↑Γ = M ∧ ∃ (t : Asudeh2022.Term Γ C), t.Linear

def Asudeh2022.GlueTy.count {α : Type u_1} [DecidableEq α] (x : α) : GlueTy α → ℤ

The count of an atom in a formula, its positive occurrences less its negative ones.

Equations

• Asudeh2022.GlueTy.count x (Asudeh2022.GlueTy.atom a) = if a = x then 1 else 0
• Asudeh2022.GlueTy.count x (A ⊸ B) = Asudeh2022.GlueTy.count x B - Asudeh2022.GlueTy.count x A

def Asudeh2022.countAt {α : Type u_1} [DecidableEq α] (x : α) (Γ : List (GlueTy α)) (i : ℕ) : ℤ

The count of an atom in the formula at a position of a list, zero past its end.

Equations

• Asudeh2022.countAt x Γ i = (Option.map (Asudeh2022.GlueTy.count x) Γ[i]?).getD 0

theorem Asudeh2022.Term.count_eq_sum {α : Type u_1} {Γ : List (GlueTy α)} [DecidableEq α] (x : α) {T : GlueTy α} (t : Term Γ T) (ht : t.HypLinear) : GlueTy.count x T = (List.map (countAt x Γ) t.uses).sum

theorem Asudeh2022.Term.Linear.count_eq {α : Type u_1} {Γ : List (GlueTy α)} [DecidableEq α] (x : α) {T : GlueTy α} {t : Term Γ T} (ht : t.Linear) : GlueTy.count x T = (List.map (GlueTy.count x) Γ).sum

The conclusion of a linear proof has the total count of its premises, which is count invariance.

theorem Asudeh2022.Derivable.count_eq {α : Type u_1} [DecidableEq α] {M : Multiset (GlueTy α)} {C : GlueTy α} (h : Derivable M C) (x : α) : GlueTy.count x C = (Multiset.map (GlueTy.count x) M).sum

A formula derivable from a multiset has the multiset's total count of every atom.

Proof nets

A proof net forgets the order in which a proof applies its rules. The sequent Γ ⊢ C is read with its premises negative and its conclusion positive, so that a negative implication is a tensor and a positive one a par, and a net links every negative atom occurrence to a positive occurrence of the same atom. By Danos and Regnier's criterion, a linking is a proof when every switching, which keeps one of the two edges at each par, leaves a tree.

inductive Asudeh2022.GlueTy.Node {α : Type u_1} : GlueTy α → Type u_1

The subformula occurrences of a formula, as paths from its root.

• root {α : Type u_1} {A : GlueTy α} : A.Node
• left {α : Type u_1} {A B : GlueTy α} : A.Node → (A ⊸ B).Node
• right {α : Type u_1} {A B : GlueTy α} : B.Node → (A ⊸ B).Node

def Asudeh2022.GlueTy.Node.path {α : Type u_1} {A : GlueTy α} : A.Node → List Bool

The path to a node, false for each step into an antecedent and true for each step into a consequent.

Equations

• Asudeh2022.GlueTy.Node.root.path = []
• n.left.path = false :: n.path
• n.right.path = true :: n.path

theorem Asudeh2022.GlueTy.Node.path_injective {α : Type u_1} {A : GlueTy α} : Function.Injective path

@[instance_reducible]

instance Asudeh2022.GlueTy.instDecidableEqNode {α : Type u_1} (A : GlueTy α) : DecidableEq A.Node

Equations

• A.instDecidableEqNode x✝¹ x✝ = decidable_of_iff (x✝¹.path = x✝.path) ⋯

def Asudeh2022.GlueTy.Node.all {α : Type u_1} (A : GlueTy α) : List A.Node

The subformula occurrences of a formula, root first.

Equations

• One or more equations did not get rendered due to their size.
• Asudeh2022.GlueTy.Node.all (Asudeh2022.GlueTy.atom a) = [Asudeh2022.GlueTy.Node.root]

theorem Asudeh2022.GlueTy.Node.mem_all {α : Type u_1} {A : GlueTy α} (n : A.Node) : n ∈ all A

theorem Asudeh2022.GlueTy.Node.nodup_all {α : Type u_1} (A : GlueTy α) : (all A).Nodup

@[instance_reducible]

instance Asudeh2022.GlueTy.instFintypeNode {α : Type u_1} (A : GlueTy α) : Fintype A.Node

Equations

• A.instFintypeNode = { elems := { val := ↑(Asudeh2022.GlueTy.Node.all A), nodup := ⋯ }, complete := ⋯ }

def Asudeh2022.GlueTy.Node.sub {α : Type u_1} {A : GlueTy α} : A.Node → GlueTy α

The subformula at a node.

Equations

• Asudeh2022.GlueTy.Node.root.sub = x✝
• n.left.sub = n.sub
• n.right.sub = n.sub

def Asudeh2022.GlueTy.Node.flip {α : Type u_1} {A : GlueTy α} : A.Node → Bool

Whether a node lies under an odd number of antecedents.

Equations

• Asudeh2022.GlueTy.Node.root.flip = false
• n.left.flip = !n.flip
• n.right.flip = n.flip

def Asudeh2022.GlueTy.Node.childDir {α : Type u_1} {A : GlueTy α} : A.Node → A.Node → Option Bool

Whether c is the antecedent (false) or the consequent (true) child of p.

def Asudeh2022.GlueTy.label? {α : Type u_1} : GlueTy α → Option α

The atom a formula is, if it is one.

Equations

• (Asudeh2022.GlueTy.atom a).label? = some a
• (A ⊸ B).label? = none

def Asudeh2022.reachWithin {V : Type u_2} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (v : V) : ℕ → Finset V

The vertices reachable from v in at most k steps.

Equations

• Asudeh2022.reachWithin G v 0 = {v}
• Asudeh2022.reachWithin G v k.succ = (Asudeh2022.reachWithin G v k).biUnion fun (u : V) => insert u (Finset.filter (G.Adj u) Finset.univ)

theorem Asudeh2022.mem_reachWithin_succ {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v w : V} {k : ℕ} : w ∈ reachWithin G v (k + 1) ↔ ∃ u ∈ reachWithin G v k, w = u ∨ G.Adj u w

theorem Asudeh2022.reachWithin_mono {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (v : V) {k m : ℕ} (h : k ≤ m) : reachWithin G v k ⊆ reachWithin G v m

theorem Asudeh2022.reachable_of_mem_reachWithin {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v w : V} {k : ℕ} : w ∈ reachWithin G v k → G.Reachable v w

theorem Asudeh2022.reachWithin_subset_of_adj {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v u : V} (h : G.Adj v u) (k : ℕ) : reachWithin G u k ⊆ reachWithin G v (k + 1)

theorem Asudeh2022.mem_reachWithin_length {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {v w : V} (p : G.Walk v w) : w ∈ reachWithin G v p.length

theorem Asudeh2022.connected_iff_reachWithin {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (v : V) : G.Connected ↔ reachWithin G v (Fintype.card V) = Finset.univ

theorem Asudeh2022.isTree_iff_reachWithin {V : Type u_2} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (v : V) : G.IsTree ↔ reachWithin G v (Fintype.card V) = Finset.univ ∧ ∑ w : V, G.degree w + 2 = 2 * Fintype.card V

A finite graph is a tree when everything is reachable from one vertex and it has one edge fewer than vertices.

@[reducible, inline]

abbrev Asudeh2022.Sequent (α : Type u_2) : Type u_2

A one-sided sequent lists formulas with their polarities.

Equations

• Asudeh2022.Sequent α = List (Bool × Asudeh2022.GlueTy α)

def Asudeh2022.Sequent.of {α : Type u_1} (Γ : List (GlueTy α)) (C : GlueTy α) : Sequent α

The sequent of premises Γ and conclusion C, the premises negative.

Equations

• Asudeh2022.Sequent.of Γ C = List.map (fun (x : Asudeh2022.GlueTy α) => (false, x)) Γ ++ [(true, C)]

@[reducible, inline]

abbrev Asudeh2022.Sequent.Vert {α : Type u_1} (S : Sequent α) : Type u_1

The subformula occurrences of a sequent.

Equations

• S.Vert = ((i : Fin (List.length S)) × S[i].2.Node)

@[instance_reducible, instance 10000]

instance Asudeh2022.Sequent.instDecidableEqVert {α : Type u_1} (S : Sequent α) : DecidableEq S.Vert

Equations

• S.instDecidableEqVert u v = decidable_of_iff (↑u.fst = ↑v.fst ∧ u.snd.path = v.snd.path) ⋯

def Asudeh2022.Sequent.pol {α : Type u_1} (S : Sequent α) (v : S.Vert) : Bool

The polarity of an occurrence.

Equations

• S.pol v = (S[v.fst].1 != v.snd.flip)

def Asudeh2022.Sequent.label? {α : Type u_1} (S : Sequent α) (v : S.Vert) : Option α

The atom an occurrence is, if it is one.

Equations

• S.label? v = v.snd.sub.label?

@[reducible, inline]

abbrev Asudeh2022.Sequent.Neg {α : Type u_1} (S : Sequent α) : Type u_1

The negative atom occurrences.

Equations

• S.Neg = { v : S.Vert // (S.label? v).isSome = true ∧ S.pol v = false }

@[reducible, inline]

abbrev Asudeh2022.Sequent.Pos {α : Type u_1} (S : Sequent α) : Type u_1

The positive atom occurrences.

Equations

• S.Pos = { v : S.Vert // (S.label? v).isSome = true ∧ S.pol v = true }

def Asudeh2022.Sequent.IsPar {α : Type u_1} (S : Sequent α) (v : S.Vert) : Prop

A par is a positive implication; a switching keeps one of its two edges.

Equations

• S.IsPar v = ((S.label? v).isNone = true ∧ S.pol v = true)

@[instance_reducible]

instance Asudeh2022.Sequent.instDecidablePredVertIsPar {α : Type u_1} (S : Sequent α) : DecidablePred S.IsPar

Equations

• S.instDecidablePredVertIsPar x✝ = { decide := decide ((S.label? x✝).isNone = true) && decide (S.pol x✝ = true), reflects_decide := ⋯ }

@[reducible, inline]

abbrev Asudeh2022.Sequent.Switching {α : Type u_1} (S : Sequent α) : Type u_1

A switching chooses an edge at each par.

Equations

• S.Switching = ({ v : S.Vert // S.IsPar v } → Bool)

def Asudeh2022.Sequent.edgeDir {α : Type u_1} (S : Sequent α) : S.Vert → S.Vert → Option Bool

The direction of the formula-tree edge from p down to c, if there is one.

Equations

• S.edgeDir ⟨i, p⟩ ⟨j, c⟩ = if h : i = j then (h ▸ p).childDir c else none

def Asudeh2022.Sequent.kept {α : Type u_1} (S : Sequent α) (σ : S.Switching) (p c : S.Vert) : Bool

The switching keeps the formula-tree edge from p down to c.

Equations

• S.kept σ p c = match S.edgeDir p c with | some b => if h : S.IsPar p then σ ⟨p, h⟩ == b else true | none => false

@[reducible, inline]

abbrev Asudeh2022.Sequent.Linking {α : Type u_1} (S : Sequent α) : Type u_1

A linking pairs each negative atom occurrence with a positive occurrence of the same atom.

Equations

• S.Linking = { e : S.Neg ≃ S.Pos // ∀ (v : S.Neg), S.label? ↑(e v) = S.label? ↑v }

def Asudeh2022.Sequent.Linking.ax {α : Type u_1} {S : Sequent α} (L : S.Linking) (u v : S.Vert) : Bool

The axiom link from a negative occurrence u to v.

Equations

• L.ax u v = if h : (S.label? u).isSome = true ∧ S.pol u = false then ↑(↑L ⟨u, h⟩) == v else false

def Asudeh2022.Sequent.Linking.graph {α : Type u_1} {S : Sequent α} (L : S.Linking) (σ : S.Switching) : SimpleGraph S.Vert

The switching graph keeps the chosen formula-tree edges and every axiom link.

Equations

• L.graph σ = SimpleGraph.fromRel fun (u v : S.Vert) => S.kept σ u v = true ∨ L.ax u v = true

@[instance_reducible]

instance Asudeh2022.Sequent.instDecidableRelVertAdjGraph {α : Type u_1} {S : Sequent α} (L : S.Linking) (σ : S.Switching) : DecidableRel (L.graph σ).Adj

Equations

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

def Asudeh2022.Sequent.Linking.Correct {α : Type u_1} {S : Sequent α} (L : S.Linking) : Prop

A linking is correct if every switching graph is a tree.

Equations

• L.Correct = ∀ (σ : S.Switching), (L.graph σ).IsTree

def Asudeh2022.Sequent.lastRoot {α : Type u_1} {S : Sequent α} (h : 0 < List.length S) : S.Vert

The root of the last formula.

Equations

• Asudeh2022.Sequent.lastRoot h = ⟨⟨List.length S - 1, ⋯⟩, Asudeh2022.GlueTy.Node.root⟩

@[instance_reducible]

instance Asudeh2022.Sequent.instDecidableIsTreeVertGraph {α : Type u_1} {S : Sequent α} (L : S.Linking) (σ : S.Switching) : Decidable (L.graph σ).IsTree

Equations

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

@[instance_reducible]

instance Asudeh2022.Sequent.instDecidableCorrect {α : Type u_1} {S : Sequent α} (L : S.Linking) : Decidable L.Correct

Equations

• Asudeh2022.Sequent.instDecidableCorrect L = { decide := decide (∀ a ∈ Finset.univ, (fun (x : S.Switching) => (L.graph x).IsTree) a), reflects_decide := ⋯ }

theorem Asudeh2022.derivable_iff_exists_correct {α : Type u_1} [DecidableEq α] (Γ : List (GlueTy α)) (C : GlueTy α) : Derivable (↑Γ) C ↔ ∃ (L : (Sequent.of Γ C).Linking), L.Correct

A sequent is derivable exactly when it has a correct proof net.

def Asudeh2022.GlueTy.leafCount {α : Type u_1} [DecidableEq α] (A : GlueTy α) (x : α) (b : Bool) : ℕ

The occurrences of x under an even (false) or odd (true) number of antecedents.

Equations

• A.leafCount x b = List.countP (fun (n : A.Node) => decide (n.sub.label? = some x ∧ n.flip = b)) (Asudeh2022.GlueTy.Node.all A)

theorem Asudeh2022.GlueTy.count_eq_leafCount {α : Type u_1} [DecidableEq α] (A : GlueTy α) (x : α) : count x A = ↑(A.leafCount x false) - ↑(A.leafCount x true)

def Asudeh2022.Sequent.occCount {α : Type u_1} [DecidableEq α] (S : Sequent α) (x : α) (p : Bool) : ℕ

The number of occurrences of x of polarity p in a sequent.

Equations

• S.occCount x p = Fintype.card { v : S.Vert // S.label? v = some x ∧ S.pol v = p }

theorem Asudeh2022.Sequent.occCount_eq {α : Type u_1} [DecidableEq α] (S : Sequent α) (x : α) (p : Bool) : S.occCount x p = (List.map (fun (F : Bool × GlueTy α) => F.2.leafCount x (F.1 != p)) S).sum

def Asudeh2022.Sequent.Linking.equivLabel {α : Type u_1} {S : Sequent α} (L : S.Linking) (x : α) : { v : S.Vert // S.label? v = some x ∧ S.pol v = false } ≃ { v : S.Vert // S.label? v = some x ∧ S.pol v = true }

A linking pairs the negative and the positive occurrences of each atom one to one.

Equations

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

theorem Asudeh2022.Sequent.Linking.count_eq {α : Type u_1} [DecidableEq α] {Γ : List (GlueTy α)} {C : GlueTy α} (L : (of Γ C).Linking) (x : α) : GlueTy.count x C = (List.map (GlueTy.count x) Γ).sum

A sequent with a linking has a conclusion with its premises' total count of every atom.

The substructural hierarchy

A logic is characterized by the structural rules it admits, and admitting more rules makes it stronger. The Lambek calculus admits none, linear logic commutativity only; relevance logic adds contraction, affine logic weakening, and intuitionistic logic both.

inductive Asudeh2022.StructuralRule : Type

The structural rules whose presence or absence characterizes a logic.

• weakening : StructuralRule
• contraction : StructuralRule
• commutativity : StructuralRule

@[instance_reducible]

instance Asudeh2022.instDecidableEqStructuralRule : DecidableEq StructuralRule

Equations

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

@[reducible, inline]

abbrev Asudeh2022.Logic : Type

A logic, by the structural rules it admits.

Equations

• Asudeh2022.Logic = Finset Asudeh2022.StructuralRule

def Asudeh2022.Logic.lambek : Logic

The Lambek calculus admits no structural rules.

Equations

• Asudeh2022.Logic.lambek = ∅

def Asudeh2022.Logic.linear : Logic

Linear logic admits commutativity only.

Equations

• Asudeh2022.Logic.linear = {Asudeh2022.StructuralRule.commutativity}

def Asudeh2022.Logic.Resource (l : Logic) : Prop

A resource logic admits neither weakening nor contraction.

Equations

• l.Resource = (Asudeh2022.StructuralRule.weakening ∉ l ∧ Asudeh2022.StructuralRule.contraction ∉ l)

theorem Asudeh2022.resource_iff (l : Logic) : l.Resource ↔ l = Logic.lambek ∨ l = Logic.linear

The resource logics are the Lambek calculus and linear logic.

theorem Asudeh2022.commutative_resource_iff (l : Logic) : l.Resource ∧ StructuralRule.commutativity ∈ l ↔ l = Logic.linear

Linear logic is the commutative resource logic.

The paper's proofs

inductive Asudeh2022.Label : Type

The instantiated atoms of the paper's examples.

• a : Label
• b : Label
• c : Label
• l : Label
• e : Label
• s : Label
• p : Label
• w : Label
• d : Label

@[instance_reducible]

instance Asudeh2022.instDecidableEqLabel : DecidableEq Label

Equations

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

@[instance_reducible]

instance Asudeh2022.instReprLabel : Repr Label

Equations

• Asudeh2022.instReprLabel = { reprPrec := Asudeh2022.instReprLabel.repr }

def Asudeh2022.instReprLabel.repr : Label → ℕ → Std.Format

Equations

• Asudeh2022.instReprLabel.repr Asudeh2022.Label.a prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.a")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.b prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.b")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.c prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.c")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.l prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.l")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.e prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.e")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.s prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.s")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.p")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.w prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.w")).group prec✝
• Asudeh2022.instReprLabel.repr Asudeh2022.Label.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Asudeh2022.Label.d")).group prec✝

def Asudeh2022.recurry : Term [GlueTy.atom Label.a ⊸ GlueTy.atom Label.b ⊸ GlueTy.atom Label.c] (GlueTy.atom Label.b ⊸ GlueTy.atom Label.a ⊸ GlueTy.atom Label.c)

Recurrying by hypothetical reasoning turns a head taking a then b into one taking b then a, discharging both hypotheses.

Equations

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

theorem Asudeh2022.recurry_linear : recurry.Linear

theorem Asudeh2022.recurry_eval {D : Label → Type} (f : D Label.a → D Label.b → D Label.c) : recurry.eval (Env.cons f Env.nil) = fun (u : D Label.b) (v : D Label.a) => f v u

The recurried proof means the same function with its arguments swapped.

def Asudeh2022.alexLikesBlake : List (List (GlueTy Label))

The meaning constructors of Alex likes Blake, word by word.

Equations

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

def Asudeh2022.likesProof : Term alexLikesBlake.flatten (GlueTy.atom Label.l)

The single normal-form proof applies likes to Blake and then to Alex, taking the premises out of word order.

Equations

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

theorem Asudeh2022.likesProof_linear : likesProof.Linear

theorem Asudeh2022.likesProof_eval {D : Label → Type} (alex : D Label.a) (like : D Label.b → D Label.a → D Label.l) (blake : D Label.b) : likesProof.eval (Env.cons alex (Env.cons like (Env.cons blake Env.nil))) = like blake alex

def Asudeh2022.finnish : List (List (GlueTy Label))

The meaning constructors of Finnish Join vettä, where join contributes the speaker and the drinking and vettä the water.

Equations

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

def Asudeh2022.english : List (List (GlueTy Label))

The meaning constructors of English I drank water, one per word.

Equations

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

theorem Asudeh2022.finnish_english : finnish.flatten = english.flatten ∧ finnish.length ≠ english.length

Two words and three words instantiate the same premises.

def Asudeh2022.drinkProof : Term english.flatten (GlueTy.atom Label.d)

The one normal-form proof of I drank water in either language.

Equations

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

theorem Asudeh2022.drinkProof_linear : drinkProof.Linear

theorem Asudeh2022.drinkProof_eval {D : Label → Type} (speaker : D Label.p) (drink : D Label.w → D Label.p → D Label.d) (water : D Label.w) : drinkProof.eval (Env.cons speaker (Env.cons drink (Env.cons water Env.nil))) = drink water speaker

def Asudeh2022.everybodyLovesSomebody : List (List (GlueTy Label))

The meaning constructors of Everybody loves somebody, word by word, with both quantifiers' scope instantiated to the clause.

Equations

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

def Asudeh2022.surface : Term everybodyLovesSomebody.flatten (GlueTy.atom Label.l)

Surface scope hypothesizes the object and then the subject, discharges the object under somebody and then the subject under everybody.

Equations

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

def Asudeh2022.inverse : Term everybodyLovesSomebody.flatten (GlueTy.atom Label.l)

Inverse scope hypothesizes the object only, applies everybody to loves of it, and discharges the object under somebody.

Equations

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

theorem Asudeh2022.surface_linear : surface.Linear

theorem Asudeh2022.inverse_linear : inverse.Linear

theorem Asudeh2022.card_correct_loves : Fintype.card { L : (Sequent.of everybodyLovesSomebody.flatten (GlueTy.atom Label.l)).Linking // L.Correct } = 2

Everybody loves somebody has exactly two correct proof nets, the two normal-form proofs the paper finds for it.

def Asudeh2022.lovesGoal : (Sequent.of everybodyLovesSomebody.flatten (GlueTy.atom Label.l)).Pos

The occurrence of the clause the sentence proves.

Equations

• Asudeh2022.lovesGoal = ⟨⟨⟨3, Asudeh2022.lovesGoal._proof_1⟩, Asudeh2022.GlueTy.Node.root⟩, Asudeh2022.lovesGoal._proof_2⟩

theorem Asudeh2022.clause_from_quantifier {L : (Sequent.of everybodyLovesSomebody.flatten (GlueTy.atom Label.l)).Linking} (hL : L.Correct) : ↑(↑((↑L).symm lovesGoal)).fst ≠ 1

In a correct net the clause is the result of a quantifier, never of loves itself, so one of the two quantifiers takes widest scope.

def Asudeh2022.Label.ty : Label → Montague.Ty

Clause atoms denote propositions and argument atoms entities.

Equations

• Asudeh2022.Label.l.ty = Montague.Ty.t
• Asudeh2022.Label.c.ty = Montague.Ty.t
• Asudeh2022.Label.d.ty = Montague.Ty.t
• x✝.ty = Montague.Ty.e

def Asudeh2022.scopeEnv {E : Type} (person : E → Prop) (love : E → E → Prop) : Env (fun (x : Label) => Montague.Ty.Domain E Unit x.ty) everybodyLovesSomebody.flatten

The premises mean every person, love and some person, the two quantifiers being the generalized quantifiers of the determiners.

Equations

• Asudeh2022.scopeEnv person love = Asudeh2022.Env.cons (Quantifier.GQ.every person) (Asudeh2022.Env.cons love (Asudeh2022.Env.cons (Quantifier.GQ.some person) Asudeh2022.Env.nil))

theorem Asudeh2022.surface_eval {E : Type} (person : E → Prop) (love : E → E → Prop) : surface.eval (scopeEnv person love) = Quantifier.Polyadic.surfaceScope Quantifier.GQ.every Quantifier.GQ.some person person fun (x y : E) => love y x

The surface proof means the surface-scope reading, every person loving some person.

theorem Asudeh2022.inverse_eval {E : Type} (person : E → Prop) (love : E → E → Prop) : inverse.eval (scopeEnv person love) = Quantifier.Polyadic.inverseScope Quantifier.GQ.every Quantifier.GQ.some person person fun (x y : E) => love y x

The inverse proof means the inverse-scope reading, some person loved by every person.

theorem Asudeh2022.interp_qr_eq_eval : HeimKratzer.Tree.interp HeimKratzer1998.lex HeimKratzer1998.g₀ HeimKratzer1998.tree_surface = some ⟨Montague.Ty.t, surface.eval (scopeEnv HeimKratzer.Toy.person HeimKratzer.Toy.sees)⟩ ∧ HeimKratzer.Tree.interp HeimKratzer1998.lex HeimKratzer1998.g₀ HeimKratzer1998.tree_inverse = some ⟨Montague.Ty.t, inverse.eval (scopeEnv HeimKratzer.Toy.person HeimKratzer.Toy.sees)⟩

One set of premises yields, by its two proofs, what Heim and Kratzer's engine computes from their two Quantifier Raising trees.

theorem Asudeh2022.readings_differ : surface.eval (scopeEnv HeimKratzer.Toy.person HeimKratzer.Toy.sees) ∧ ¬inverse.eval (scopeEnv HeimKratzer.Toy.person HeimKratzer.Toy.sees)

The two proofs are two readings, since in Heim and Kratzer's model the surface reading holds and the inverse one fails.

Completeness and Coherence

Asudeh takes resource sensitivity to do the work of Completeness and Coherence. The Dutch cross-serial clauses of Bresnan, Kaplan, Peters and Zaenen test the claim: their f-structure spine is complete and coherent exactly when its objects match its non-final verbs, and exactly then do the meaning constructors it instantiates have a linear proof of the clause.

inductive Asudeh2022.DutchAtom : Type

The atoms of a Dutch clause's semantic structure, for its noun phrases and for the clause each verb heads.

• np (j : ℕ) : DutchAtom
• clause (i : ℕ) : DutchAtom

def Asudeh2022.instDecidableEqDutchAtom.decEq (x✝ x✝¹ : DutchAtom) : Decidable (x✝ = x✝¹)

Equations

• Asudeh2022.instDecidableEqDutchAtom.decEq (Asudeh2022.DutchAtom.np a) (Asudeh2022.DutchAtom.np b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Asudeh2022.instDecidableEqDutchAtom.decEq (Asudeh2022.DutchAtom.np j) (Asudeh2022.DutchAtom.clause i) = isFalse ⋯
• Asudeh2022.instDecidableEqDutchAtom.decEq (Asudeh2022.DutchAtom.clause i) (Asudeh2022.DutchAtom.np j) = isFalse ⋯
• Asudeh2022.instDecidableEqDutchAtom.decEq (Asudeh2022.DutchAtom.clause a) (Asudeh2022.DutchAtom.clause b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Asudeh2022.instDecidableEqDutchAtom : DecidableEq DutchAtom

Equations

• Asudeh2022.instDecidableEqDutchAtom = Asudeh2022.instDecidableEqDutchAtom.decEq

def Asudeh2022.verbPremise (s : BresnanEtAl1982.Spine) (i : ℕ) : GlueTy DutchAtom

The meaning constructor of the verb at depth i. A non-final verb takes its complement as a property of the complement's subject, which functional control identifies with the verb's object, then the object and its own subject; the final verb takes its subject alone.

Equations

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

def Asudeh2022.premisesFrom (s : BresnanEtAl1982.Spine) : ℕ → ℕ → List (GlueTy DutchAtom)

The premises at the d depths from i, the object and the verb at each.

Equations

• One or more equations did not get rendered due to their size.
• Asudeh2022.premisesFrom s 0 x✝ = []

def Asudeh2022.premises (s : BresnanEtAl1982.Spine) : Multiset (GlueTy DutchAtom)

The premises of a spine are the objects and verbs at every depth and the subject.

Equations

• Asudeh2022.premises s = ↑(Asudeh2022.premisesFrom s (max s.objects s.verbs) 0 ++ [Asudeh2022.GlueTy.atom (Asudeh2022.DutchAtom.np 0)])

theorem Asudeh2022.complete_coherent_of_derivable {s : BresnanEtAl1982.Spine} (hv : 1 ≤ s.verbs) (h : Derivable (premises s) (GlueTy.atom (DutchAtom.clause 0))) : s.Complete ∧ s.Coherent

Premises with a linear proof of the clause come from a complete and coherent spine.

def Asudeh2022.build (n d i : ℕ) : i + d = n → Term (premisesFrom { objects := n, verbs := n + 1 } (d + 1) i ++ [GlueTy.atom (DutchAtom.np (BresnanEtAl1982.subjOfVerb i))]) (GlueTy.atom (DutchAtom.clause i))

The proof from the premises at the depths from i and the subject of the verb at i applies that verb to the property its complement proves, its object and its subject.

Equations

• One or more equations did not get rendered due to their size.
• Asudeh2022.build n 0 x x_1 = (Asudeh2022.Term.var 0 ⋯).app (Asudeh2022.Term.var 1 ⋯)

theorem Asudeh2022.build_linear (n d i : ℕ) (h : i + d = n) : (build n d i h).Linear

theorem Asudeh2022.derivable_of_complete_coherent {s : BresnanEtAl1982.Spine} (hv : 1 ≤ s.verbs) (h : s.Complete ∧ s.Coherent) : Derivable (premises s) (GlueTy.atom (DutchAtom.clause 0))

A complete and coherent spine instantiates premises with a linear proof of its clause.

theorem Asudeh2022.derivable_iff_complete_coherent (s : BresnanEtAl1982.Spine) (hv : 1 ≤ s.verbs) : Derivable (premises s) (GlueTy.atom (DutchAtom.clause 0)) ↔ s.Complete ∧ s.Coherent

The meaning constructors of a spine have a linear proof of its clause exactly when the spine is complete and coherent.

theorem Asudeh2022.derivable_dutch (n : ℕ) : Derivable (premises (BresnanEtAl1982.Spine.ofTree (BresnanEtAl1982.dutch n))) (GlueTy.atom (DutchAtom.clause 0))

Every clause with its objects matching its non-final verbs composes.

theorem Asudeh2022.not_derivable_extra_verb_or_np : ¬Derivable (premises (BresnanEtAl1982.Spine.ofTree (BresnanEtAl1982.tree 1 3))) (GlueTy.atom (DutchAtom.clause 0)) ∧ ¬Derivable (premises (BresnanEtAl1982.Spine.ofTree (BresnanEtAl1982.tree 2 2))) (GlueTy.atom (DutchAtom.clause 0))

dat Jan Piet Marie zag helpen laten zwemmen, with a verb too many, and dat Jan Piet Marie Hans zag helpen zwemmen, with a noun phrase too many, do not compose.

The paper's examples

def Asudeh2022.lexicon? (r : Datum) : Option (List (List (GlueTy Label)))

The meaning constructors a row's words contribute.

Equations

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

def Asudeh2022.wordCount (r : Datum) : ℕ

The number of words of a row's sentence, which are separated by single spaces.

Equations

• Asudeh2022.wordCount r = (List.filter (fun (x : Char) => decide (x = ' ')) r.primaryText.toList).length + 1

theorem Asudeh2022.rows_lexicon (r : Datum) : r ∈ Examples.all → ∃ lex ∈ lexicon? r, wordCount r = lex.length

Every row has a lexicon, and each of its words contributes meaning constructors.