Glue Semantics

@cite{asudeh-2022}

Glue Semantics is a composition framework where meanings are assembled via proof search in the implicational fragment of linear logic (⊸). Meaning constructors are pairs M : G, where M is a lambda term and G is a linear logic formula. Composition corresponds to ⊸-elimination (functional application) and ⊸-introduction (lambda abstraction) via the Curry-Howard isomorphism.

Key properties (@cite{asudeh-2022}, §1)

1. Resource-sensitive composition: Each premise is used exactly once (no weakening, no contraction). This subsumes the Theta Criterion, Projection Principle, Full Interpretation, Completeness/Coherence, No Vacuous Quantification, and the Inclusiveness Condition as instances of a single logical principle.
2. Flexible composition: The logic is commutative — word order doesn't determine composition order.
3. Autonomy of syntax: Structural syntax and the logical syntax of composition are separate levels.
4. Syntax/semantics non-isomorphism: One word may contribute multiple or zero meaning constructors.

Scope ambiguity

"Everybody loves somebody" (@cite{asudeh-2022}, §4.2) yields two scope readings. Each reading corresponds to a different instantiation of the second-order ∀ in the quantifier types, producing a different premise multiset. Each multiset has exactly one normal-form proof.

Integration with linglib

This module connects Glue to:

• ScopeConfig from Montague/Scope.lean
• interp-based QR composition from Composition/Tree.lean
• QuantifierComposition.lean for the same scope example via H&K

The bridge theorem glue_qr_agree proves that Glue proof search and QR tree interpretation yield the same truth values on the canonical scope example.

inductive Semantics.Composition.Glue.GlueTy : Type

Glue types: the implicational fragment of linear logic.

Atomic types are parameterized by strings corresponding to s-structure nodes (e.g. "e" for the subject's semantic contribution, "l" for the clause). The linear implication A ⊸ B corresponds to lolli A B.

• atom : String → GlueTy
• lolli : GlueTy → GlueTy → GlueTy

def Semantics.Composition.Glue.instDecidableEqGlueTy.decEq (x✝ x✝¹ : GlueTy) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Composition.Glue.instDecidableEqGlueTy : DecidableEq GlueTy

Equations

• Semantics.Composition.Glue.instDecidableEqGlueTy = Semantics.Composition.Glue.instDecidableEqGlueTy.decEq

def Semantics.Composition.Glue.instReprGlueTy.repr : GlueTy → ℕ → Std.Format

Equations

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

instance Semantics.Composition.Glue.instReprGlueTy : Repr GlueTy

Equations

• Semantics.Composition.Glue.instReprGlueTy = { reprPrec := Semantics.Composition.Glue.instReprGlueTy.repr }

def Semantics.Composition.Glue.«term_⊸_» : Lean.TrailingParserDescr

Equations

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

structure Semantics.Composition.Glue.MeaningConstructor (α : Type) : Type

A meaning constructor: a meaning term M paired with a Glue type G. Written M : G in the Glue literature (@cite{asudeh-2022}, §2).

• meaning : α
• glue : GlueTy

instance Semantics.Composition.Glue.instReprMeaningConstructor {α✝ : Type} [Repr α✝] : Repr (MeaningConstructor α✝)

Equations

• Semantics.Composition.Glue.instReprMeaningConstructor = { reprPrec := Semantics.Composition.Glue.instReprMeaningConstructor.repr }

def Semantics.Composition.Glue.instReprMeaningConstructor.repr {α✝ : Type} [Repr α✝] : MeaningConstructor α✝ → ℕ → Std.Format

Equations

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

inductive Semantics.Composition.Glue.GlueProof : Type

Proof terms for the implicational fragment of linear logic.

By Curry-Howard, these are simply-typed linear lambda terms:

• ax n : use the term at context index n (premise or hypothesis)
• lolliE f a : ⊸-elimination = functional application
• lolliI hypTy body : ⊸-introduction = lambda abstraction. Extends the context with hypTy; the hypothesis is accessed in body via its new index (ctx.length).

• ax : ℕ → GlueProof
• lolliE : GlueProof → GlueProof → GlueProof
• lolliI : GlueTy → GlueProof → GlueProof

def Semantics.Composition.Glue.instReprGlueProof.repr : GlueProof → ℕ → Std.Format

Equations

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

instance Semantics.Composition.Glue.instReprGlueProof : Repr GlueProof

Equations

• Semantics.Composition.Glue.instReprGlueProof = { reprPrec := Semantics.Composition.Glue.instReprGlueProof.repr }

instance Semantics.Composition.Glue.instDecidableEqGlueProof : DecidableEq GlueProof

Equations

• Semantics.Composition.Glue.instDecidableEqGlueProof = Semantics.Composition.Glue.instDecidableEqGlueProof.decEq

def Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (x✝ x✝¹ : GlueProof) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (Semantics.Composition.Glue.GlueProof.ax a) (Semantics.Composition.Glue.GlueProof.ax b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (Semantics.Composition.Glue.GlueProof.ax a) (a_1.lolliE a_2) = isFalse ⋯
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (Semantics.Composition.Glue.GlueProof.ax a) (Semantics.Composition.Glue.GlueProof.lolliI a_1 a_2) = isFalse ⋯
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (a.lolliE a_1) (Semantics.Composition.Glue.GlueProof.ax a_2) = isFalse ⋯
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (a.lolliE a_1) (Semantics.Composition.Glue.GlueProof.lolliI a_2 a_3) = isFalse ⋯
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (Semantics.Composition.Glue.GlueProof.lolliI a a_1) (Semantics.Composition.Glue.GlueProof.ax a_2) = isFalse ⋯
• Semantics.Composition.Glue.instDecidableEqGlueProof.decEq (Semantics.Composition.Glue.GlueProof.lolliI a a_1) (a_2.lolliE a_3) = isFalse ⋯

def Semantics.Composition.Glue.GlueProof.check (ctx : List GlueTy) : GlueProof → Option GlueTy

Type-check a proof against a context (premises ++ hypotheses). lolliI extends the context by appending the hypothesis type; the hypothesis is accessed in the body at index ctx.length. Returns the conclusion type if well-typed.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.Glue.GlueProof.check ctx (Semantics.Composition.Glue.GlueProof.ax a) = ctx[a]?
• Semantics.Composition.Glue.GlueProof.check ctx (Semantics.Composition.Glue.GlueProof.lolliI a a_1) = do let bodyTy ← Semantics.Composition.Glue.GlueProof.check (ctx ++ [a]) a_1 some (a ⊸ bodyTy)

def Semantics.Composition.Glue.GlueProof.usedPremises (numPremises : ℕ) : GlueProof → List ℕ

Indices of premises (from the original context) used by a proof. Hypothesis indices (≥ numPremises) are excluded.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.Glue.GlueProof.usedPremises numPremises (Semantics.Composition.Glue.GlueProof.ax a) = if a < numPremises then [a] else []
• Semantics.Composition.Glue.GlueProof.usedPremises numPremises (Semantics.Composition.Glue.GlueProof.lolliI a a_1) = Semantics.Composition.Glue.GlueProof.usedPremises numPremises a_1

def Semantics.Composition.Glue.GlueProof.isResourceCorrect (numPremises : ℕ) (p : GlueProof) : Bool

A proof is resource-correct if every premise is used exactly once.

Equations

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

The logic landscape

@cite{asudeh-2022} (§3) situates linear logic in a hierarchy of substructural logics (Figure 1). Logics are characterized by which structural rules they admit:

• Weakening: A premise can be freely added (Γ⊢B → Γ,A⊢B)
• Contraction: A duplicate premise can be freely discarded (Γ,A,A⊢B → Γ,A⊢B)
• Commutativity: Premises can be freely reordered (Γ,A,B⊢C → Γ,B,A⊢C)

Lambek logic L has none of these. Linear logic adds commutativity. Relevance logic adds contraction. Affine/BCK logic adds weakening. Intuitionistic logic has all three.

Semantics is best modeled by a commutative resource logic: composition is order-independent (Klein & Sag 1985: types, not order, determine composition) but resource-sensitive (each meaning used exactly once).

inductive Semantics.Composition.Glue.StructuralRule : Type

Structural rules that characterize logics in the substructural hierarchy.

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

instance Semantics.Composition.Glue.instDecidableEqStructuralRule : DecidableEq StructuralRule

Equations

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

def Semantics.Composition.Glue.instReprStructuralRule.repr : StructuralRule → ℕ → Std.Format

Equations

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

instance Semantics.Composition.Glue.instReprStructuralRule : Repr StructuralRule

Equations

• Semantics.Composition.Glue.instReprStructuralRule = { reprPrec := Semantics.Composition.Glue.instReprStructuralRule.repr }

inductive Semantics.Composition.Glue.SubstructuralLogic : Type

Substructural logics, ordered by which structural rules they admit (@cite{asudeh-2022}, §3, Figure 1).

• lambekL : SubstructuralLogic
• linearLogic : SubstructuralLogic
• relevance : SubstructuralLogic
• affineBCK : SubstructuralLogic
• intuitionistic : SubstructuralLogic

instance Semantics.Composition.Glue.instDecidableEqSubstructuralLogic : DecidableEq SubstructuralLogic

Equations

• Semantics.Composition.Glue.instDecidableEqSubstructuralLogic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Composition.Glue.instReprSubstructuralLogic.repr : SubstructuralLogic → ℕ → Std.Format

Equations

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

instance Semantics.Composition.Glue.instReprSubstructuralLogic : Repr SubstructuralLogic

Equations

• Semantics.Composition.Glue.instReprSubstructuralLogic = { reprPrec := Semantics.Composition.Glue.instReprSubstructuralLogic.repr }

def Semantics.Composition.Glue.SubstructuralLogic.admitsRule : SubstructuralLogic → StructuralRule → Bool

Equations

• Semantics.Composition.Glue.SubstructuralLogic.lambekL.admitsRule x✝ = false
• Semantics.Composition.Glue.SubstructuralLogic.linearLogic.admitsRule Semantics.Composition.Glue.StructuralRule.commutativity = true
• Semantics.Composition.Glue.SubstructuralLogic.linearLogic.admitsRule x✝ = false
• Semantics.Composition.Glue.SubstructuralLogic.relevance.admitsRule Semantics.Composition.Glue.StructuralRule.weakening = false
• Semantics.Composition.Glue.SubstructuralLogic.relevance.admitsRule x✝ = true
• Semantics.Composition.Glue.SubstructuralLogic.affineBCK.admitsRule Semantics.Composition.Glue.StructuralRule.contraction = false
• Semantics.Composition.Glue.SubstructuralLogic.affineBCK.admitsRule x✝ = true
• Semantics.Composition.Glue.SubstructuralLogic.intuitionistic.admitsRule x✝ = true

def Semantics.Composition.Glue.SubstructuralLogic.isResourceSensitive : SubstructuralLogic → Bool

Equations

• Semantics.Composition.Glue.SubstructuralLogic.lambekL.isResourceSensitive = true
• Semantics.Composition.Glue.SubstructuralLogic.linearLogic.isResourceSensitive = true
• x✝.isResourceSensitive = false

def Semantics.Composition.Glue.glueLogic : SubstructuralLogic

The Glue logic is linear logic.

Equations

• Semantics.Composition.Glue.glueLogic = Semantics.Composition.Glue.SubstructuralLogic.linearLogic

theorem Semantics.Composition.Glue.glue_is_commutative : glueLogic.admitsRule StructuralRule.commutativity = true

theorem Semantics.Composition.Glue.glue_no_weakening : glueLogic.admitsRule StructuralRule.weakening = false

theorem Semantics.Composition.Glue.glue_no_contraction : glueLogic.admitsRule StructuralRule.contraction = false

theorem Semantics.Composition.Glue.glue_is_resource_sensitive : glueLogic.isResourceSensitive = true

Simple transitive composition (@cite{asudeh-2022}, §2)

The simplest Glue derivation: a transitive verb with two arguments. Given meaning constructors:

likes : λy.λx.like(y)(x) : b ⊸ a ⊸ l
alex  : alex              : a
blake : blake              : b

The unique normal-form proof applies likes to blake, then to alex:

likes : b⊸a⊸l    blake : b
────────────────────────── ⊸ε
   like(blake) : a⊸l      alex : a
   ────────────────────────────── ⊸ε
        like(blake)(alex) : l

def Semantics.Composition.Glue.a_ : GlueTy

Equations

• Semantics.Composition.Glue.a_ = Semantics.Composition.Glue.GlueTy.atom "a"

def Semantics.Composition.Glue.b_ : GlueTy

Equations

• Semantics.Composition.Glue.b_ = Semantics.Composition.Glue.GlueTy.atom "b"

def Semantics.Composition.Glue.l_ : GlueTy

Equations

• Semantics.Composition.Glue.l_ = Semantics.Composition.Glue.GlueTy.atom "l"

def Semantics.Composition.Glue.alexLikesBlakePremises : List GlueTy

Premises for "Alex likes Blake".

Equations

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

def Semantics.Composition.Glue.alexLikesBlakeProof : GlueProof

Proof: apply likes to blake, then to alex.

Equations

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

theorem Semantics.Composition.Glue.alex_likes_blake_typechecks : GlueProof.check alexLikesBlakePremises alexLikesBlakeProof = some l_

theorem Semantics.Composition.Glue.alex_likes_blake_resource_correct : GlueProof.isResourceCorrect 3 alexLikesBlakeProof = true

def Semantics.Composition.Glue.alexLikesBlakeReordered : List GlueTy

Argument reordering: the same proof works regardless of premise order, because the Glue logic is commutative (@cite{asudeh-2022}, §2).

Equations

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

def Semantics.Composition.Glue.alexLikesBlakeReorderedProof : GlueProof

Equations

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

theorem Semantics.Composition.Glue.reordered_typechecks : GlueProof.check alexLikesBlakeReordered alexLikesBlakeReorderedProof = some l_

theorem Semantics.Composition.Glue.reordered_resource_correct : GlueProof.isResourceCorrect 3 alexLikesBlakeReorderedProof = true

Meaning constructors (@cite{asudeh-2022}, §4.2)

Lexical entries (before instantiation):

love    : λy.λx.love(y)(x)     : (↑ OBJ)σ ⊸ (↑ SUBJ)σ ⊸ ↑σ
every   : λQ.every(person, Q)  : ∀S.(e ⊸ S) → S
some    : λQ.some(person, Q)   : ∀S.(s ⊸ S) → S

The ∀ quantifier in the Glue logic ranges over Glue types. Different instantiations of S yield different premise contexts, and each context has exactly one normal-form proof.

Surface scope (∀>∃): every instantiated with S=l, some with S=e⊸l. Inverse scope (∃>∀): some instantiated with S=l, every with S=s⊸l.

def Semantics.Composition.Glue.e_ : GlueTy

Equations

• Semantics.Composition.Glue.e_ = Semantics.Composition.Glue.GlueTy.atom "e"

def Semantics.Composition.Glue.s_ : GlueTy

Equations

• Semantics.Composition.Glue.s_ = Semantics.Composition.Glue.GlueTy.atom "s"

def Semantics.Composition.Glue.surfacePremises : List GlueTy

Equations

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

def Semantics.Composition.Glue.inversePremises : List GlueTy

Equations

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

def Semantics.Composition.Glue.surfaceProof : GlueProof

Surface scope proof: every(some(love)) : l

Proof structure (cf. @cite{asudeh-2022}, Figure 4):

1. Apply some(S=e⊸l) to love → e ⊸ l
2. Apply every(S=l) to result → l

Equations

• Semantics.Composition.Glue.surfaceProof = (Semantics.Composition.Glue.GlueProof.ax 2).lolliE ((Semantics.Composition.Glue.GlueProof.ax 1).lolliE (Semantics.Composition.Glue.GlueProof.ax 0))

def Semantics.Composition.Glue.inverseProof : GlueProof

Inverse scope proof: some(every(λv.λu.love(u)(v))) : l

Proof structure (cf. @cite{asudeh-2022}, Figure 5):

1. Assume [v:e]³, [u:s]⁴
2. Apply love to u (s-arg) then to v (e-arg) → l
3. Abstract over u → s⊸l, then over v → e⊸s⊸l
4. Apply every(S=s⊸l) → s⊸l
5. Apply some(S=l) → l

Equations

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

theorem Semantics.Composition.Glue.surface_typechecks : GlueProof.check surfacePremises surfaceProof = some l_

Surface proof type-checks to l.

theorem Semantics.Composition.Glue.inverse_typechecks : GlueProof.check inversePremises inverseProof = some l_

Inverse proof type-checks to l.

theorem Semantics.Composition.Glue.surface_resource_correct : GlueProof.isResourceCorrect 3 surfaceProof = true

Surface proof uses each premise exactly once.

theorem Semantics.Composition.Glue.inverse_resource_correct : GlueProof.isResourceCorrect 3 inverseProof = true

Inverse proof uses each premise exactly once.

The Glue logic tells us how to compose meanings but not what the meanings are. The meaning terms are ordinary Montague-style denotations. We connect Glue proofs to truth conditions by evaluating them over the same toyModel used by QuantifierComposition.lean.

The toy model has no `love` predicate, so we use `sees_sem` as
the transitive relation. The logical structure is identical.

Surface scope: every(person, λx. some(person, λy. sees(y)(x)))
Inverse scope: some(person, λy. every(person, λx. sees(y)(x)))

def Semantics.Composition.Glue.glue_surface_meaning : Bool

Equations

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

def Semantics.Composition.Glue.glue_inverse_meaning : Bool

Equations

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

theorem Semantics.Composition.Glue.glue_readings_differ : glue_surface_meaning ≠ glue_inverse_meaning

The two Glue readings differ (genuine ambiguity).

theorem Semantics.Composition.Glue.glue_surface_true : glue_surface_meaning = true

Surface scope is true in the toy model (each person sees some person).

theorem Semantics.Composition.Glue.glue_inverse_false : glue_inverse_meaning = false

Inverse scope is false in the toy model (no single person is seen by everyone).

Both Glue and QR are extensionally equivalent on the canonical scope example: both yield exactly {∀>∃, ∃>∀} with the same truth values. The QR side is computed via interp from Composition/Tree.lean, connecting Glue to the H&K composition engine.

def Semantics.Composition.Glue.glueReading : Scope.ScopeConfig → Bool

Map ScopeConfig to truth values via Glue evaluation.

Equations

• Semantics.Composition.Glue.glueReading Semantics.Scope.ScopeConfig.surface = Semantics.Composition.Glue.glue_surface_meaning
• Semantics.Composition.Glue.glueReading Semantics.Scope.ScopeConfig.inverse = Semantics.Composition.Glue.glue_inverse_meaning

def Semantics.Composition.Glue.qrReading : Scope.ScopeConfig → Option Bool

Map ScopeConfig to truth values via QR tree interpretation (@cite{heim-kratzer-1998} Ch. 5).

Equations

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

theorem Semantics.Composition.Glue.qr_surface_agrees : qrReading Scope.ScopeConfig.surface = some glue_surface_meaning

QR surface scope tree produces the same truth value as Glue.

theorem Semantics.Composition.Glue.qr_inverse_agrees : qrReading Scope.ScopeConfig.inverse = some glue_inverse_meaning

QR inverse scope tree produces the same truth value as Glue.

theorem Semantics.Composition.Glue.glue_qr_agree (s : Scope.ScopeConfig) : qrReading s = some (glueReading s)

Glue and QR yield identical truth values for both scope readings.

Two fundamentally different composition mechanisms — proof search in linear logic (Glue, @cite{asudeh-2022}) vs. covert movement with Predicate Abstraction (QR, @cite{heim-kratzer-1998}) — produce the same semantic results.

@cite{asudeh-2022} (§3) argues that linear logic resource sensitivity subsumes several well-formedness conditions from different frameworks. These are all instances of: in a valid linear logic proof, each premise is used exactly once.

inductive Semantics.Composition.Glue.ResourceCondition : Type

• completenessCoherence : ResourceCondition
• thetaCriterion : ResourceCondition
• projectionPrinciple : ResourceCondition
• noVacuousQuantification : ResourceCondition
• fullInterpretation : ResourceCondition
• inclusivenessCondition : ResourceCondition

instance Semantics.Composition.Glue.instDecidableEqResourceCondition : DecidableEq ResourceCondition

Equations

• Semantics.Composition.Glue.instDecidableEqResourceCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Composition.Glue.instReprResourceCondition : Repr ResourceCondition

Equations

• Semantics.Composition.Glue.instReprResourceCondition = { reprPrec := Semantics.Composition.Glue.instReprResourceCondition.repr }

def Semantics.Composition.Glue.instReprResourceCondition.repr : ResourceCondition → ℕ → Std.Format

Equations

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

def Semantics.Composition.Glue.ResourceCondition.fromNoWeakening : List ResourceCondition

Resource sensitivity = no weakening + no contraction. No weakening means every premise must be consumed (captures fullInterpretation, inclusivenessCondition). No contraction means each premise consumed at most once (captures thetaCriterion, noVacuousQuantification). Together they enforce completenessCoherence and projectionPrinciple.

Equations

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

def Semantics.Composition.Glue.ResourceCondition.fromNoContraction : List ResourceCondition

Equations

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

@cite{asudeh-2022} (§4) distinguishes three approaches to the syntax-semantics interface:

1. **Interpretive** (H&K/QR): Syntax produces LF, which is
   directly interpreted. Scope ambiguity requires a syntactic
   operation (QR/covert movement) — two distinct LF trees.
2. **Parallel** (CG/CCG): Syntax and semantics computed in
   lockstep. Scope ambiguity requires type-shifting operations
   and corresponding categorial modifications.
3. **Glue** (separable logic): Syntax produces meaning
   constructors; composition is proof search. Scope ambiguity
   arises from multiple ∀-instantiations — no syntactic ambiguity
   or type-shifting needed.

linglib formalizes all three: H&K in `Composition/Tree.lean`,
CCG in `CCG/Interface.lean`, Glue here. 

inductive Semantics.Composition.Glue.CompositionApproach : Type

• interpretive : CompositionApproach
• parallel : CompositionApproach
• glueSeparable : CompositionApproach

instance Semantics.Composition.Glue.instDecidableEqCompositionApproach : DecidableEq CompositionApproach

Equations

• Semantics.Composition.Glue.instDecidableEqCompositionApproach x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Composition.Glue.instReprCompositionApproach : Repr CompositionApproach

Equations

• Semantics.Composition.Glue.instReprCompositionApproach = { reprPrec := Semantics.Composition.Glue.instReprCompositionApproach.repr }

def Semantics.Composition.Glue.instReprCompositionApproach.repr : CompositionApproach → ℕ → Std.Format

Equations

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

inductive Semantics.Composition.Glue.ScopeAmbiguityMechanism : Type

How each approach handles scope ambiguity.

• covertMovement : ScopeAmbiguityMechanism
• typeShifting : ScopeAmbiguityMechanism
• proofSearch : ScopeAmbiguityMechanism

instance Semantics.Composition.Glue.instDecidableEqScopeAmbiguityMechanism : DecidableEq ScopeAmbiguityMechanism

Equations

• Semantics.Composition.Glue.instDecidableEqScopeAmbiguityMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Composition.Glue.instReprScopeAmbiguityMechanism : Repr ScopeAmbiguityMechanism

Equations

• Semantics.Composition.Glue.instReprScopeAmbiguityMechanism = { reprPrec := Semantics.Composition.Glue.instReprScopeAmbiguityMechanism.repr }

def Semantics.Composition.Glue.instReprScopeAmbiguityMechanism.repr : ScopeAmbiguityMechanism → ℕ → Std.Format

Equations

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

def Semantics.Composition.Glue.CompositionApproach.scopeMechanism : CompositionApproach → ScopeAmbiguityMechanism

Equations

• Semantics.Composition.Glue.CompositionApproach.interpretive.scopeMechanism = Semantics.Composition.Glue.ScopeAmbiguityMechanism.covertMovement
• Semantics.Composition.Glue.CompositionApproach.parallel.scopeMechanism = Semantics.Composition.Glue.ScopeAmbiguityMechanism.typeShifting
• Semantics.Composition.Glue.CompositionApproach.glueSeparable.scopeMechanism = Semantics.Composition.Glue.ScopeAmbiguityMechanism.proofSearch

theorem Semantics.Composition.Glue.glue_scope_via_proof_search : CompositionApproach.glueSeparable.scopeMechanism = ScopeAmbiguityMechanism.proofSearch

Glue is the only approach that derives scope ambiguity from proof search rather than syntactic or type-theoretic operations.

def Semantics.Composition.Glue.requiresSyntacticOperation : CompositionApproach → Bool

In Glue, the structural syntax need not be ambiguous to derive scope ambiguity — the ambiguity is in the proof space.

Equations

• Semantics.Composition.Glue.requiresSyntacticOperation Semantics.Composition.Glue.CompositionApproach.interpretive = true
• Semantics.Composition.Glue.requiresSyntacticOperation Semantics.Composition.Glue.CompositionApproach.parallel = false
• Semantics.Composition.Glue.requiresSyntacticOperation Semantics.Composition.Glue.CompositionApproach.glueSeparable = false

theorem Semantics.Composition.Glue.glue_no_syntactic_operation : requiresSyntacticOperation CompositionApproach.glueSeparable = false

theorem Semantics.Composition.Glue.interpretive_requires_syntactic_operation : requiresSyntacticOperation CompositionApproach.interpretive = true