1
$\begingroup$

When I am trying to understand logic programming languages e.g. Prolog, I am immediately confused by the following two ways of relating logic systems and programming languages or type systems.

  1. In Types and Programming Languages by Pierce, Section 9.4 Curry–Howard correspondence on p109 has a table

    enter image description here

    Does it mean that a logic system is a programming language, where

    • types are propositions and
    • values of a type are proofs of the proposition?

  2. On the other hand, a logic system is described in a formal language that defines what a logic expression is. Can we view a logic system (e.g. the first order predicate logic system) as a programming language, where

    • it has two types: Boolean type and function type, and
    • Each logic expression without a variable has Boolean type, so can be evaluated to a truth value. Each logic expression with any variable has Boolean function type, so its application to truth values for its variables can be evaluated to a truth value?

Are the above two views of a logic system as a programming language completely unrelated/orthogonal, or are they the same or can they be unified?

Thanks.

Improve this question
$\endgroup$
1
  • $\begingroup$ In (2), you should not regard those boolean-valued functions as computable functions that programmers write, because there are non-computable ones. Hence this relationship between programming languages and logic is broken. $\endgroup$
    – beroal
    Feb 27, 2020 at 15:27

2 Answers 2

Reset to default
1
$\begingroup$

Does it mean that a logic system is a programming language, where types are propositions and values of a type are proofs of the proposition?

Not necessarily, being both (logic systems and programming language) formal languages, there certainly is a certain degree of isomorphism between the two concepts, this translates into the fact that we can encode a logical system through a programming language and develop algorithms to identify proofs of the theorems of our logical system.

If you are interested in the similarities between logical propositions and types, I strongly suggest you take a look at Homotopy type theory.

Improve this answer
$\endgroup$
2
  • $\begingroup$ Thanks. See my clarification of my questions. $\endgroup$
    – Tim
    Nov 28, 2019 at 13:53
  • $\begingroup$ I am mainly wondering if the two views of a logic system are related or not, and if the second view (from mine) is sensible. $\endgroup$
    – Tim
    Nov 28, 2019 at 14:50
1
$\begingroup$

The relationship between the two is related to intuistionistic logic vs. classical logic. When you add sufficiently powerful versions of the excluded middle law to Curry-Howard-style type systems, you can translate between propositions (types of sort Prop, which are inhabited if and only if they are provable) and Boolean values at will. Check out the list of excluded middle/proof irrelevance laws available in Coq for a jumping-off point.

Improve this answer
$\endgroup$

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.