[Prev][Next][Index][Thread]
Re: Why Prolog and CBV?
Date: Fri, 08 Nov 91 20:25:28 EST
Regarding John Mitchell's equation:
>> PROLOG Call-by-value
>> ------------- = -----------------
>> Resolution Lambda calculus
I think the following analogy is a little more accurate
PROLOG Scheme
------------- ---------------
Pure Prolog = Call-by-value lambda calculus
------------ ---------------
Horn logic Lambda calculus
where resolution plays roughly the same role as beta-reduction.
A similar picture exists for typed languages:
Elf Lambda Prolog ML
----- = --------------------------- = ---------
LF Higher-order Harrop logic Typed lambda calculus
In each case, an undecidable search problem (for a normal form or for a proof
of a query) is made deterministic by a commitment to a particular control
strategy. This is the step from a theorem prover to a programming language.
A theorem prover's operational behavior is hard to predict and it is intended
to search for answers in a space whose structure we do not understand very
well. A programming language with a well-defined operational semantics, on
the other hand, can be used to implement solutions for problems whose
structure we understand well enough to solve it algorithmically. One pays the
price of completeness with respect to a "declarative" semantics (eg the
lambda-calculus or Horn logic).
This doesn't really answer the quest for a "unifying principle" in all these
situations, but I think the design space for these languages (and many others
not mentioned above) is too rich to allow a uniform analysis.
- Frank