A question about logic and the Curry-Howard correspondence

Question

Could you please explain me what is the basic connection between the fundamentals of logical programming and the phenomenon of syntactic similarity between type systems and conventional logic?

Asa

Can you be more specific, or provide examples? – Farhi

Answer 1

The Curry-Howard correspondence is not about logic programming, but functional programming. The fundamental mechanic of Prolog is justified in proof theory by John Robinson's resolution technique, which shows how it is possible to check whether logical formulae expressed as Horn clauses are satisfiable, that is, whether you can find terms to substitue for their logic variables that make them true.

Thus logic programming is about specifying programs as logical formulae, and the calculation of the program is some form of proof inference, in Prolog reolution, as I have said. By contrast the Curry-Howard correspondence shows how proofs in a special formulasition of logic, called natural deduction, correspond to programs in the lambda calculus, with the type of the program corresponding to the formula that the proof proves; computation in the lambda calculus corresponds to an important phenomenon in proof theory called normalisation, which transforms proofs into new, more direct proofs. So logic programming and functional programming correspond to different levels in these logics: logic programs match formulae of a logic, whilst functional programs match proofs of formulae.

There's another difference: the logics used are generally different. Logic programming generally uses simpler logics — as I said, Prolog is founded on Horn clauses, which are a highly restricted class of formulae where implications may not be nested, and there are no disjunctions, although Prolog recovers the full strength of classical logic using the cut rule. By contrast, functional programming languages such as Haskell make heavy use of programs whose types have nested implications, and are decorated by all kinds of forms of polymorphism. They are also based on intuitionistic logic, a class of logics that forbids use of the principle of the excluded middle, which Robinson's computational mechanism is based on.

Some other points:

1. It is possible to base logic programming on more sophisticated logics than Horn clauses; for example, Lambda-prolog is based on intuitionistic logic, with a different computation mechanism than resolution.
2. Dale Miller has called the proof-theoretic paradigm behind logic programming the proof search as programming metaphor, to contrast with the proofs as programs metaphor that is another term used for the Curry-Howard correspondence.

Jaborandi

What a wonderful explanation! You did it better that wiki and books I've read, thank you very much! – Asa

And a would like to ask (maybe a somewhat silly) question: In general, what do the first-class functions in lambda calculust correspond to WRT to natural deduction.. are these higher-order predicates? – Asa

Oops, I meant 'in natural deduction' if extended with predicates :) – Asa

Sorry, another comment: just to be clear with the point of my last question - could you decipher the phrase functional programming languages such as Haskell make heavy use of programs whose types have nested implications for me please? – Asa

@Bubba: Quantification in first-order predicate calulus corresponds to dependent typing in the lambda calculus: there are a few ways of doing this. You can't express combinators like map using Horn clauses: the type is (a -> b) -> [a] -> [b], where the first "->" is nested because it appears bracketed to the left of the final "->", making this an order 2 function. Horn clauses can express only order 1 functions. – Jaborandi

That's what I was after :) Thank you. – Asa

@CharlesStewart Is sequent calculus more appropriate then natural deduction? In the sequent calculus all inference rules have a purely bottom-up reading. In natural deduction - bidirectional. en.wikipedia.org/wiki/… – Downthrow

Answer 2

Logic programming is fundamentally about goal directed searching for proofs. The structural relationship between typed languages and logic generally involves functional languages, although sometimes imperative and other languages - but not logic programming languages directly. This relationship relates proofs to programs.

So, logic programming proof search can be used to find proofs that are then interpreted as functional programs. This seems to be the most direct relationship between the two (as you asked for).

Building whole programs this way isn't practical, but it can be useful for filling in tedious details in programs, and there's some important examples of this in practice. A basic example of this is structural subtyping - which corresponds to filling in a few proof steps via a simple entailment proof. A much more sophisticated example is the type class system of Haskell, which involves a particular kind of goal directed search - in the extreme this involves a Turing-complete form of logic programming at compile time.

Nerveless