Re: Why Prolog and CBV?

To: types
Subject: Re: Why Prolog and CBV?
From: Frank Pfenning <Frank_Pfenning@ALONZO.TIP.CS.CMU.EDU>
Date: Sat, 09 Nov 91 17:27:59 EST
In-Reply-To: Your message of Fri, 08 Nov 91 18:23:23 -0500. <199111082323.AA08667@stork.lcs.mit.edu>
Sender: meyer@theory.lcs.mit.edu

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