8
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • 4
    $\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
    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$
    – Discrete lizard
    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
    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
    May 1, 2018 at 21:51

Your Answer

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

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