Source-linked AI summary
A Lambda Calculus Based on Quantum Logic
Kenji Tokuo
TL;DR
Quantum logic uses orthomodular lattices as semantics, while implication does not generally have a satisfactory set of properties. The paper develops NQ and the typed lambda calculus QuLam, connects them through Curry–Howard, and proves soundness and completeness for NQ and strong normalization for QuLam.
Problem
Quantum logic has orthomodular-lattice semantics, but implication cannot in general satisfy a satisfactory set of properties.
Source: §1.1 · p. 1Method
The paper develops NQ with the Sasaki hook and connects it through Curry–Howard to QuLam, a typed lambda calculus whose abstraction body depends only on its bound argument.
Source: §1.2 · p. 1, §2.2 · p. 3, §5.3 · p. 19Results
NQ is sound and complete with respect to orthomodular lattices, and every well-typed QuLam term is strongly normalizing.
Source: Theorem 2.9 (Soundness and… · p. 6, Proposition 2.24 (Strong normalization) · p. 13Takeaways & Limitations
QuLam can abstract over multiple assumptions by combining them into a product argument and can represent deductions based on the Sasaki projection.
Source: §5.4 · p. 19, Proposition 5.4 (Abstraction over a… · p. 19, §6 · p. 21Ordinary currying is unavailable in general because an inner abstraction cannot depend on a variable free in that abstraction’s body.
Source: §5.5 · p. 20
Abstract
from arXiv · showhide
We propose a typed lambda calculus based on quantum logic. We first present a natural deduction system for quantum logic with the Sasaki hook as its implication operation and then formulate a typed lambda calculus connected to this system through the Curry-Howard correspondence. We prove soundness and completeness of the former with respect to orthomodular lattices and strong normalization of the latter. The resulting lambda calculus has the characteristic feature that only one assumption is available in the typing derivation that serves as the premise of $\lambda$-abstraction. Under this restriction, ordinary currying is not available in general, but it is still possible to perform $\lambda$-abstraction by combining multiple assumptions into a single argument of product type and to construct a term corresponding to a deduction using the Sasaki projection.
1 Introduction
The paper situates quantum logic and related proof systems, then revisits NQ and QuLam with explicit additional rules and establishes their formal results. It also outlines the paper’s structure.
1.1 Background
- Quantum logic uses orthomodular lattices as algebraic semantics, while the Sasaki hook serves as a candidate implication; related work includes quantum-logic deduction systems and quantum lambda calculi.Earlier work introduced NQ and an associated typed lambda calculus; SOM uses ordered assumptions, while other quantum lambda calculi address quantum computation.Source: §1.1 · p. 1
1.2 Contributions
- NQ and QuLam are extended with explicit missing rules; the paper establishes their correspondence with GOM, soundness and completeness, and strong normalization.QuLam restricts abstraction to a single assumption, but supports abstraction over a combined product argument and terms for deductions based on the Sasaki projection.Source: §1.2 · pp. 1–2
1.3 Organization
- The paper moves from NQ and QuLam’s formal foundations to their correspondence, semantics, term structure, and conclusion.Section 2 includes NQ soundness and completeness and QuLam strong normalization; Sections 3–5 cover correspondence, semantics, and term structure.Source: §1.3 · p. 2
2 Formal Foundations
The formal foundations define orthomodular-lattice semantics and Sasaki operations, then give NQ’s language and inference rules. The Sasaki hook and restricted implication rules distinguish the system’s treatment of implication.
2.1 Orthomodular Lattices
- In an orthomodular lattice, propositions are ordered by entailment, negation is orthocomplement, and distributivity need not hold.Closed subspaces of a Hilbert space, ordered by inclusion, provide an example.Source: §2.1 · p. 2
Definition 2.1 (Sasaki operations)
- The Sasaki hook is a⊥∨(a∧b), and the Sasaki projection is ϕa(b)=a∧(a⊥∨b).The hook is used for implication and the projection for the study of terms.Source: Definition 2.1 (Sasaki operations) · p. 2, §2.1 · p. 2
Lemma 2.2 (Sasaki adjunction)
- The Sasaki projection and hook satisfy an adjunction: ϕa(c) ≤ b exactly when c ≤ a →S b.Source: Lemma 2.2 (Sasaki adjunction) · p. 2
2.2 Natural Deduction for Quantum Logic
- NQ formulas use propositional variables, ⊥, conjunction, and primitive implication; negation abbreviates implication to ⊥.Assumptions are labeled, and contexts are finite sets of labeled assumptions; unused assumptions are permitted.Source: §2.2 · p. 3
Definition 2.3 (Natural deduction system NQ)
- NQ derivations are built from labeled assumption occurrences and inference rules whose displayed figures give each rule’s final inference.Discharged assumption labels may be renamed, and schematic derivations denote entire premise derivations.Source: Definition 2.3 (Natural deduction… · p. 3
- NQ includes conjunction introduction and elimination, as well as implication introduction and elimination.Source: Definition 2.3 (Natural deduction… · p. 3
- Implication introduction requires its premise derivation to have no undischarged assumption other than the discharged assumption; modus tollens is also included.The conclusion of implication introduction has no undischarged assumptions, including when used inside a larger proof.Source: Definition 2.3 (Natural deduction… · p. 4
- NQ also includes double-negation rules and Sasaki-hook rules, which preserve the undischarged assumptions of their premise derivations.The Sasaki-hook rules are distinct from restricted implication introduction and modus ponens.Source: Definition 2.3 (Natural deduction… · p. 4
Remark 2.4 (Relation to the earlier rules)
NQ adds explicit Sasaki-hook introduction and elimination rules to the earlier system. Its formulas are interpreted in orthomodular lattices, and its derivations translate into GOM.
Remark 2.4 (Relation to the earlier rules)
- NQ adds explicit →IS and →ES rules to the rules from, making explicit an inference previously implicit and supporting formulas with implication subformulas.The earlier proof identified ¬(α ∧¬(α ∧β)) with primitive implication; →ES is needed to work with formulas containing implication as a subformula.Source: Remark 2.4 (Relation to the earlier… · p. 4
Definition 2.5 (Interpretation of formulas)
- Formulas interpret variables as lattice elements, conjunction as meet, ⊥ as 0, and implication as the Sasaki hook; contexts are interpreted by meet.The empty context has value 1.Source: Definition 2.5 (Interpretation of… · p. 4
2.3 Soundness and Completeness
- GOM is a quantum-logic sequent calculus with conjunction and negation as primitives, sound and complete for orthomodular lattice semantics.Its Sasaki hook abbreviates ¬(α ∧¬(α ∧β)).Source: §2.3 · pp. 4–5
Lemma 2.6 (Admissibility in GOM)
- If Γ ⊢NQ α, then translating the assumptions and conclusion with H yields a derivable GOM sequent H(Γ) ⊢ H(α).The proof proceeds by induction on the NQ derivation, using semantic interderivability for Sasaki-hook rules.Source: Lemma 2.6 (Admissibility in GOM) · p. 5
Lemma 2.7 (Translation of normal GOM sequents)
The paper translates normal GOM sequents back into NQ, establishes congruence of interderivability, and proves NQ sound and complete for orthomodular-lattice semantics. It then defines QuLam’s types and typing rules.
Lemma 2.7 (Translation of normal GOM sequents)
- A normal GOM derivation translates to an NQ derivation of the translated succedent, or of ⊥ when the succedent is empty.The translation first replaces O-modular steps with MP; →IS and →E handle translated MP steps.Source: Lemma 2.7 (Translation of normal GOM… · pp. 5–6
Lemma 2.8 (Congruence of interderivability)
- NQ interderivability is preserved when equivalent formulas are placed under negation, conjunction, or implication.For implication, the proof uses its interderivability with the conjunction-and-negation expansion of the Sasaki hook.Source: Lemma 2.8 (Congruence of… · p. 6
Theorem 2.9 (Soundness and completeness of NQ)
- For every finite Γ and formula α, Γ ⊢NQ α exactly when [[Γ]]ν ≤ [[α]]ν in every orthomodular lattice under every valuation.Completeness proceeds through GOM and normal sequents, then translates back to NQ.Source: Theorem 2.9 (Soundness and… · p. 6
Definition 2.10 (Types)
- QuLam types are generated from type variables and ⊥ using product and implication constructors.Only finite applications of these formation rules yield types.Source: Definition 2.10 (Types) · p. 7
Definition 2.11 (Typing environments)
- Typing environments are finite partial maps from term variables to types, and typing judgments state that a term has a type under an environment.Term formation includes variables, pairing and projections, application, abstraction, and constructors corresponding to NQ rules.Source: Definition 2.11 (Typing environments) · pp. 7–8
- QuLam also includes term constructors for modus tollens, double-negation introduction and elimination, and Sasaki-hook introduction and elimination.The Sasaki-hook constructors convert between α → β and ¬(α ׬(α ×β)).Source: Definition 2.11 (Typing environments) · p. 7
Definition 2.13 (Variables in terms)
The section defines free variables and establishes how they relate to typing environments, including the closedness of typable abstractions.
Definition 2.13 (Variables in terms)
- The free variables of a term are defined recursively, with FV(x) = {x}; terms equivalent under α-conversion count as the same term.The section states that the remaining free-variable clauses follow the usual definition.Source: Definition 2.13 (Variables in terms) · p. 8
Lemma 2.14 (Free variables)
- If Γ ⊢ M : α, then FV(M) ⊆ dom(Γ); any typable λx.N is closed, with FV(N) ⊆ {x}.These environment properties are used in subject reduction and in constructing abstractions over product arguments.Source: Lemma 2.14 (Free variables) · p. 8, Definition 2.13 (Variables in terms) · p. 8
Lemma 2.15 (Weakening)
The section establishes weakening and substitution properties for QuLam typings, then introduces subterms in preparation for conversion rules.
Lemma 2.15 (Weakening)
- A term’s typing is preserved when its environment is extended consistently.Source: Lemma 2.15 (Weakening) · p. 9
Lemma 2.16 (Substitution)
- Simultaneously substituting terms for a set of distinct variables preserves the resulting term’s type under their common environment.The result also applies when the original term is typed under a subenvironment of the variables being replaced.Source: Lemma 2.16 (Substitution) · p. 9
Definition 2.17 (Subterms)
- A subterm is a subexpression, equivalently a subtree of the term’s abstract syntax tree; conversion rules correspond to eliminating detours in NQ proofs.Source: Definition 2.17 (Subterms) · p. 10
Definition 2.18 (Conversion)
The calculus defines conversion and normal forms, then shows that conversion preserves typing. Reducibility sets provide the proof framework for the later strong-normalization result.
Definition 2.18 (Conversion)
- A beta conversion replaces an application of an abstraction with its capture-avoiding substitution instance; conversion also includes other subterm replacements.The reflexive-transitive closure permits zero or more steps, and a term with no applicable step is a normal form.Source: Definition 2.18 (Conversion) · p. 10, Definition 2.19 (Normal forms) · p. 10
- No conversion rule has ζ or ξ at its root, so ξ(ζ(M)) and ζ(ξ(N)) remain unchanged at their roots.Source: Definition 2.18 (Conversion) · p. 10
Proposition 2.20 (Subject reduction)
- If Γ ⊢ M : α and M converts to N in one or more steps, then Γ ⊢ N : α.The proof handles root conversions and conversions inside subterms while preserving the required environments.Source: Proposition 2.20 (Subject reduction) · p. 10
Definition 2.21 (Reducibility sets)
- Reducibility sets are defined over raw terms by type: base types use strongly normalizing terms, products test projections, and implications test applications.The proof also uses the finite maximum conversion-sequence length h(M) for strongly normalizing terms.Source: Definition 2.21 (Reducibility sets) · p. 11
Lemma 2.22 (Properties of reducibility sets)
- Every reducible term is strongly normalizing, and a term whose immediate reducts are reducible is reducible when its outermost constructor is not pairing, abstraction, or θ.Source: Lemma 2.22 (Properties of reducibility… · p. 11
Lemma 2.23 (Reducibility of constructors)
The constructor lemma establishes that reducibility is preserved by the calculus’s term constructors, including abstraction and the operators for negation and the Sasaki hook.
Lemma 2.23 (Reducibility of constructors)
- The lemma also establishes reducibility for η and θ under their respective input-type conditions.Source: Lemma 2.23 (Reducibility of… · pp. 12–13
- Pairing is reducible when both components are reducible, as established by showing that each projection of the pair is reducible.Source: Lemma 2.23 (Reducibility of… · p. 12
- For abstraction, if substituting every reducible argument into the body yields a reducible term, then applying the abstraction to any reducible argument is reducible.The proof uses induction on the maximal conversion lengths of the body and argument.Source: Lemma 2.23 (Reducibility of… · p. 12
- The modus tollens constructor τ is reducible for reducible arguments, using that its applications have no root conversion and its arguments are strongly normalizing.Source: Lemma 2.23 (Reducibility of… · p. 13
Proposition 2.24 (Strong normalization)
The strong-normalization proof substitutes reducible terms for a typing derivation’s assumptions, obtains reducibility of the resulting term, and concludes that every well-typed QuLam term is strongly normalizing.
Proposition 2.24 (Strong normalization)
- Every well-typed QuLam term is strongly normalizing under the conversions of Definition 2.18.Source: Proposition 2.24 (Strong normalization) · pp. 13–14
- The proof establishes by induction on typing derivations that substituting reducible terms for all assumptions yields a term reducible at the conclusion type.Taking each substituted term to be its corresponding variable gives reducibility of the original term; property (C1) then gives strong normalization.Source: Proposition 2.24 (Strong normalization) · pp. 13–14
- The induction covers the Sasaki hook constructors ζ and ξ by showing their substituted terms remain reducible through conversion-length inductions.Source: Proposition 2.24 (Strong normalization) · p. 14
3 Curry–Howard Correspondence
The paper maps quantum-logic formulas and derivations to QuLam types and typing derivations. This correspondence preserves the restricted abstraction rule and represents the Sasaki hook with dedicated constructors.
3.1 Types as Propositions
- A bijection between propositional variables and type variables extends recursively to mutually inverse, structure-preserving maps between NQ formulas and QuLam types.Source: §3.1 · p. 14
3.2 Terms as Proofs
- Labeled assumptions map to term variables and typing environments, while equivalent derivations identify changes to discharged labels or bound-variable names.Source: §3.2 · pp. 14–15
- Implication introduction maps to λ-abstraction, whose premise permits only the discharged assumption; unused assumptions are handled by extending the environment.Source: §3.2 · p. 15, Proposition 3.1 (Derivation… · p. 15
Proposition 3.1 (Derivation correspondence)
- The correspondence is a bijection between labeled NQ derivations and canonical QuLam typing derivations, with matching environments and conclusion types.Source: Proposition 3.1 (Derivation… · p. 15, §3.2 · p. 15
3.3 Constructors for the Sasaki Hook
- The Sasaki hook introduction and elimination rules map to ζ and ξ, respectively, and neither rule discharges assumptions.Source: Proposition 3.1 (Derivation… · p. 15, §3.3 · p. 16
Example 3.2 (Term for the rule MP)
- The term λz.(ζ(π2z))(π1z) represents modus ponens, which the paper says is used to replace the O-modular rule in Lemma 2.7.Source: Example 3.2 (Term for the rule MP) · p. 16
Example 3.3 (Implication from a conjunction)
- From an assumption α × β, the example constructs a term of type α → β using θ, τ, and ζ.Source: Example 3.3 (Implication from a… · p. 16
4 Orthomodular Lattice Semantics
QuLam typing judgments are interpreted in orthomodular lattices by mapping types and environments to lattice elements and testing an order relation. This semantics is sound and complete for typing judgments.
4 Orthomodular Lattice Semantics
- The semantics for typing judgments is established by interpreting QuLam types and environments in orthomodular lattices.The section proves both soundness and completeness with respect to this semantics.Source: §4 · p. 16, §4.1 · p. 16, Theorem 4.3 (Soundness) · p. 17
4.1 Interpretation of Types
- Types are interpreted inductively as elements of an orthomodular lattice, and corresponding NQ formulas and finite sets of assumptions have matching interpretations.The interpretation uses the Sasaki hook for implication.Source: Definition 4.1 (Interpretation of types) · p. 16, Lemma 4.2 (Transport of valuations) · pp. 16–17
4.2 Semantics of Typing Judgments
- An environment is interpreted as the meet of its declared types, with the empty environment interpreted as 1; a judgment is valid when the environment’s value is below the type’s value.This makes typing validity correspond to the interpretation of the conjunction of the corresponding NQ assumptions.Source: §4.2 · p. 17
Theorem 4.3 (Soundness)
- Every derivable QuLam judgment Γ ⊢ M : α satisfies [[Γ]]ρ ≤ [[α]]ρ in every orthomodular lattice, and the converse holds whenever that inequality holds universally.For closed judgments, soundness requires [[α]]ρ = 1.Source: Theorem 4.3 (Soundness) · p. 17, Corollary 4.4 (Completeness of typing… · p. 18
5 Structure of Terms
QuLam’s term constructors represent quantum-logical deductions while enforcing a singleton dependency for abstraction. Product arguments and the Sasaki projection provide alternative constructions where ordinary currying is unavailable.
5.1 Negative Composition
- The constructor τ assigns a term to modus tollens when a closed α → β term is paired with a context-dependent β → ⊥ term.Applying the resulting term to an α argument yields ⊥ under the union of consistent environments.Source: Proposition 5.1 (Term assignment for… · p. 18
5.2 Double Negation
- For each type α, θ embeds terms into double-negation type and η returns them, with ηα(θαM) reducing to M.The corresponding types are α → ((α → ⊥) → ⊥) and ((α → ⊥) → ⊥) → α.Source: Proposition 5.2 (Double-negation… · p. 19
5.3 Restrictions on Dependencies
- An abstraction body can have no free variable other than its bound variable, so the abstraction itself is closed.The corresponding τ construction keeps its positive implication term closed while assumptions remain in the negative premise.Source: Proposition 5.3 (Explicit dependency… · p. 19
5.4 Abstraction over Product Arguments
- Multiple assumptions can be combined into a product argument and abstracted over as one argument, with projections recovering the original components.For x : α and y : β, the resulting closed term has type (α × β) → γ; the construction extends to any finite list of at least two assumptions.Source: Proposition 5.4 (Abstraction over a… · pp. 19–20
5.5 Failure of Ordinary Currying
- Ordinary currying is unavailable in general: QuLam cannot type λx.λy.x because x remains free in the inner abstraction.The semantic example shows α → (β → α) is not valid in all orthomodular lattices, so no closed QuLam term has that type.Source: §5.5 · p. 20
5.6 Sasaki Projection
- The paper defines ϕα(γ) as α × ¬(α × ¬γ), whose lattice interpretation is the Sasaki projection of γ onto α.This projection supplies the premise used in the deduction construction.Source: §5.6 · p. 20, Proposition 5.5 (Deduction using the… · p. 20
- The Sasaki-projection deduction principle constructs a term of type α → β from a derivation of β under the assumption ϕα(γ).When the interpretations of α and γ commute, the premise’s projection equals their meet.Source: Proposition 5.5 (Deduction using the… · p. 20
6 Conclusion
The paper refines NQ and QuLam with explicit Sasaki-hook rules and term constructors. It establishes their logical and normalization properties while showing how product arguments and the Sasaki projection support constructions under restricted abstraction.
6 Conclusion
- The extended NQ and QuLam systems include explicit Sasaki-hook rules and corresponding term constructors ζ and ξ.Source: §6 · p. 21
- The paper establishes soundness and completeness for NQ and typing judgments, the Curry–Howard correspondence, and strong normalization of QuLam.Source: §6 · p. 21
- Although ordinary currying is not generally available, QuLam supports abstraction over product arguments, uncurrying closed terms, and term constructions for Sasaki-projection deduction.Source: §6 · p. 21