Hi.
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?
What a wonderful explanation! You did it better that wiki and books I've read, thank you very much!
Bubba88
2010-05-18 17:41:29
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?
Bubba88
2010-05-18 17:43:05
Oops, I meant 'in natural deduction' if extended with predicates :)
Bubba88
2010-05-18 17:47:21
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?
Bubba88
2010-05-18 18:58:25
@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.
Charles Stewart
2010-05-19 11:14:59
That's what I was after :) Thank you.
Bubba88
2010-05-19 11:23:27
+1
A:
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.
RD1
2010-07-31 10:23:40