Curry-Howard Logic and Correspondence Question

Question

Could you explain to me what is the main connection between the basic principles of logical programming and the phenomenon of syntactic similarity between type systems and traditional logic?

Answer 1

Curry-Howard correspondence is not logical programming, but functional programming. Prolog's founding mechanic is grounded in the theory of evidence by the John Robinson method, which shows how you can check if logical formulas can be expressed by a Horn expression, that is, if you can find substitution terms for your logical variables that make them true.

Thus, logical programming is an indication of programs as logical formulas, and computing a program is some form of proof of output, in Prolog reolution, as I said. On the contrary, the Curry-Howard correspondence shows how evidence in a special logical expression called natural deduction corresponds to lambda calculus programs, and the type of program corresponding to the formula that the proof proves; computation in lambda calculus corresponds to an important phenomenon in the theory of evidence called normalization, which turns evidence into new, more direct evidence. Thus, logical programming and functional programming correspond to different levels in these logics: logical programs correspond to logic formulas, while functional programs correspond to proofs of formulas.

There is another difference: the logics used are usually different. Logic programming usually uses simpler logic — as I said, Prolog is based on Horn's sentences, which are a very limited class of formulas where the consequences may not be nested and there are no differences, although Prolog restores the full power of classical logic using the cut-out rule . In contrast, functional programming languages ​​such as Haskell make heavy use of programs whose types have nested consequences and are decorated with all kinds of forms of polymorphism. They are also based on intuitionistic logic, a class of logics that prohibits the use of the excluded mean principle on which Robinson's computational mechanism is based.

Some other points:

• Logical programming on more complex logics than Horn's suggestions is possible; for example, the Lambda prologue is based on intuitionistic logic with a different calculation mechanism than resolution.
• Dale Miller called the theoretical and theoretical paradigm of logical search search programming as a programming metaphor, as opposed to proof as a programming metaphor, which is another term used to match Curry-Howard.

Answer 2

Logical programming is mainly about the goal of finding evidence. The structural relationship between typed languages ​​and logic usually includes functional languages, although sometimes imperative and other languages, but not logical programming languages. This relationship links evidence for programs.

Thus, the search for evidence of logical programming can be used to search for evidence, which is then interpreted as functional programs. This is apparently the most direct connection between the two (as you requested).

Building entire programs in this way is impractical, but can be useful for filling out tedious details in programs, and there are some important examples of this in practice. The main example of this is structural subtyping — which corresponds to filling out several stages of evidence with a simple collection proof. A more complex example is the Haskell class system, which includes a certain type of target search - in extreme cases, this includes the full form of Turing's logical programming at compile time.