In words of Wikipedia,

The Curry–Howard correspondence is the observation that two families of seemingly unrelated formalisms—namely, the proof systems on one hand, and the models of computation on the other—are in fact the same kind of mathematical objects [...] a proof is a program, and the formula it proves is the type for the program.

Further, under General Formulation, it provides the following table and the statement that bears my question:

enter image description here

In its more general formulation, the Curry–Howard correspondence is a correspondence between formal proof calculi and type systems for models of computation. In particular, it splits into two correspondences. One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs which, this time, is specific to the particular choice of proof system and model of computation considered.

Is quantum computing in this hindsight equivalent to classical computing, or is it a different "model of computation" (i.e. does it have a different set of elements in the Programming side)? Would it still correspond to the exact same Logic side?


2 Answers 2


Quantum computing doesn't change the Curry-Howard isomorphism, for the following reasons:

  1. Quantum computers can simulate Turing machines and vice versa. These devices can be faster at certain tasks, but the computable languages remain the same.

  2. There is, a priori, no reason we cannot apply the model of the Turing machine of Lambda calculus to quantum computers, even if they can compute different, mutually exclusive languages!

  3. For practical purposes, I very much doubt quantum computing will be of use in automated theorem proving or proof assistance (by computers).

So, as for your question, yes in the context of Curry-Howard, we can consider a quantum computer and a classical machine equivalent, as it is likely we wish to model both with the Lambda calculus for the purpose of the isomorphism.

  • 5
    $\begingroup$ In my opinion your answer does is not really satisfying. The question is more about how to define a type system for the programming model of quantum computer (e.g. the model of quantum circuits) and how and which logic corresponded to it via Curry-Howard. There are attempts (algebraic calculi for quantum computing) and I plan to give an extend answer as soon as I find the time. $\endgroup$
    – dtell
    Commented Mar 30, 2018 at 11:16
  • 1
    $\begingroup$ Well, I interpreted the question as "does quantum change anything". I'm not surprised by the fact that a type system for quantum programming can be made. I only fail to see why you would do so, as I doubt QC would improve the type checking task. Of course, type checking a quantum programming language is useful, but that isn't what is being asked here (though interesting on its own). $\endgroup$ Commented Mar 30, 2018 at 12:16
  • $\begingroup$ @datell as discussed with Discrete lizard I made a specific question for the answer you are willing to post, I am very curious about that! cheers $\endgroup$
    – fr_andres
    Commented Mar 30, 2018 at 15:31
  • $\begingroup$ @datell I wanted to take a look into that, were you meaning something like this? $\endgroup$
    – fr_andres
    Commented May 1, 2018 at 21:51
  • $\begingroup$ @dtell I wonder if after 5 yrs you managed to find the time to give an extended answer. I'd be really interested in hearing :) $\endgroup$ Commented Nov 19, 2023 at 19:01

A formulation of the logic underlying quantum theory (and quantum systems), posed by Isham et al., that supersedes the older (non-distributive) quantum logic formulation associated with von Neumann, came about early this century and late last century. It is a logic on a bi-Heyting lattice, which means you have all the structure of (distributive) intuitionist logic, but also all the dual connectives.

It's actually easy to fully characterize [bi-/dual-]Heyting lattices and Boolean lattices and the logics based on them. Let $A ⊢ B$ (or equivalently $B ⊣ A$) denote the "inference" relation (that statement $A$ infers statement $B$, i.e. that $B$ can be inferred from $A$). It's a pre-order relation by virtue of the properties $$A ⊢ A,\quad \left(\begin{aligned}A ⊢ B\\B ⊢ C\end{aligned}\right) ⇒ A ⊢ C.$$ The corresponding equivalence relation $$A ⊣⊢ B ⇔ \left(\begin{aligned}A ⊢ B\\A ⊣ B\end{aligned}\right),$$ then gives you equivalence classes $[A] = \{ B: A ⊣⊢ B \}$ that are, then, partially ordered by $[A] ≤ [B]$ if and only if $A ⊢ B$, and the ordering forms a bi-Heyting lattice.

Associated with it are connectives that may be succinctly (and precisely) characterized by the following properties $$\begin{array}{lcl} C ⊢& A ∧ B &⇔ \left(\begin{aligned}C ⊢ A\\C ⊢ B\end{aligned}\right),\\ C ⊢& ⊤ &⇔\text{ always},\\ C ⊢& A ⊃ B &⇔ C ∧ A ⊢ B,\\ C ⊢& ¬A &⇔ C ∧ A ⊢ ⊥, \end{array}$$ and $$\begin{array}{cll} A ∨ B &⊢ D &⇔ \left(\begin{aligned}A ⊢ D\\B ⊢ D\end{aligned}\right),\\ ⊥ &⊢ D &⇔\text{ always},\\ A ⊂ B &⊢ D &⇔ A ⊢ B ∨ D,\\ ⨽B &⊢ D &⇔ ⊤ ⊢ B ∧ D. \end{array}$$

The connective $A ⊃ B$, also written as $A → B$, is the conditional "if $A$ then $B$" connective, while the dual $A ⊂ B$, which could also be written as $A - B$, is the actual Boolean connective (meant in the sense that Boole, himself, used it in his "Laws of Thought" book) "$A$ unless $B$" or "$A$ except $B$". I've also seen it written as $A ← B$. The stronger "is false" negation, associated with Heyting lattices, is $¬A ⊣⊢ A ⊃ ⊥$, while the weaker "isn't true" negation that Boole used $⨽B ⊣⊢ ⊤ ⊂ B$ is a kind of dual. I've also seen it written as $\sim B$. The inference $¬C ⊢ ⨽C$ is valid, while the converse $¬C ⊣ ⨽C$ is valid, as a rule, if and only if the logic is ... Boolean.

There is a presentation-mode PDF on this newer Isham-based quantum logic framework Contexts, Bi-Heyting Algebras and a New Logic for Quantum Systems and ArXiv pre-print Topos-Based Logic for Quantum Systems and Bi-Heyting Algebras, both by Döring, that discuss this in depth.

The logics are, as lattices, complete, which means that they have arbitrary least upper bounds (join) $∨$ and greatest lower bounds (meet) $∧$ on an arbitrary number of arguments of arbitrary cardinality, not just a finite number of arguments; and they are both distributive, including infinitely distributive. It's for that reason that you have the full set of connectives and their duals.

Everything is defined in the setting of topos theory, which (as per my best understanding) have some kind of "internal language" associated with them similar to that of a Curry-Howard representation for intuitionistic logics. I'm not entirely sure about that, since I haven't (yet) studied topos theory in any great depth. I see no references anywhere on doing Curry-Howard for bi-Heyting logics, but I do see this PDF Topos Internal Language, which might be useful for connecting the dots.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.