A Lambda Calculus Based on Quantum Logic

Overview & Synopsis

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.