Skip to content
DraconiticResearch
Search Sources API
197,768 studies31 sourcesUpdated 3 min ago
PreprintarXiv licencearXiv

A Lambda Calculus Based on Quantum Logic

  • Kenji Tokuo
Open at sourcePDFDOICite

Abstract

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 λ-abstraction. Under this restriction, ordinary currying is not available in general, but it is still possible to perform λ-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.

Related

  1. On Models of the Planar Lambda Calculus
    Chad Nester
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv
  2. Tense Logic via Truth Degrees: An Algebraic Completeness Result for Kashima's Calculus
    Martín Figallo, Jonathan Sarmiento, Luis Pezzini
    arXivPreprintarXiv licenceFull textLogic & foundationsarXiv
  3. Remarks on covariant differential calculus on the non-standard quantum Podleś sphere
    Tomasz Brzezinski, Réamonn Ó Buachalla
    arXivPreprintarXiv licenceFull textAlgebra & number theoryarXiv
  4. Closed Response Calculus and Joint Densities for the Liouville Quantum Gravity Metric
    Chunhao Cai
    arXivPreprintarXiv licenceFull textProbabilityarXiv
  5. A density calculus for quantum field theory
    Tanay Kibe, Pratik Roy
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsMathematical physicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{tokuo2026lambda,
  title = {{A Lambda Calculus Based on Quantum Logic}},
  author = {Kenji Tokuo},
  howpublished = {arXiv},
  year = {2026},
  month = oct,
  doi = {10.48550/arxiv.2610.34266},
  eprint = {2610.34266},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2610.34266},
}
RIS
TY  - UNPB
TI  - A Lambda Calculus Based on Quantum Logic
AU  - Kenji Tokuo
PY  - 2026
DA  - 2026/10/25
PB  - arXiv
DO  - 10.48550/arxiv.2610.34266
UR  - https://arxiv.org/abs/2610.34266
AB  - 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 λ-abstraction. Under this restriction, ordinary currying is not available in general, but it is still possible to perform λ-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.
ER  -