Peter Van Roy writes:
>Where is the logic?
>...
>Very strange these modernists! Can someone "deconstruct" this
>definition for me?
Let me give it a try, off the top of my head:
"Logic programming" seems to be many beasts with the same name. We
must distinguish between operational uses of inference rules to
construct proofs and models of true statements, i.e. between the
semantics of proof theory (with SLD-resolution etc.) and that of
model theory (with Tp-operators, intended models, closed world
assumptions etc.). A lot of attention has been put on the
correspondence (or lack thereof) between the operational and the model
theoretic reading of Prolog. In fact most Prolog programmers, for
reasons of "efficiency" or "practicality" seem to ignore the model
theoretic reading, that we carefully teach in LP-courses. Moreover,
the least Herbrand model used in the theory (and sometimes the
equality theory, unification) does not cover floting point numbers,
rational trees or FD-constraints, often used in practical programs.
Logic programming could be seen as a paradigm where the basic idea is
that a computation is the construction of a proof according to some
valid proof rules, thus guaranteeing that any produced result is a
valid consequence of the program statements read as axioms.
(NB! No model theory here.)
This is of course different from the "programs as proofs" paradigm,
where the systematic construction of a program is done using a proof
procedure, whereby the resulting program "automatically" will be valid
if the specification is valid.
As Peter points out, any programming language can be given an
operational semantics in terms of "inference rules" or rather rewrite
rules, be it for instance Java, Oz, or Haskell. The distinction could,
I guess, be that in logic programming we read the rewrite rules as
rules to construct a proof.
Hence the loose talk about "specifications" being written in "the same
language" as "programs".
To be more precise we might want a number of things from a
specification language:
(a non-exhaustive list)
- a way to express the logical relations between data (objects)
- a way to express the pre-post conditions of algorithms (objects)
- a way to specify allowed inputs to sub-programs (procedures, objects)
- a way to specify communication patterns, error conditions,
timing constraints etc.
Given such a language we could go about designing algorithms that
use these statements to prove properties of programs,
transform programs etc. (analysers, compilers, partial evaluators).
A hard-line programmer/hacker would of course say that a programming
language is all that is required, since after all programs are the way
we think, and the program is the best specification of itself. Others
might not agree. A natural question to consider is what makes two
programs "equal" even if they have different syntax. Clearly, we all
normally have an ideal "program" in mind when we generate code, such
that the code is considered to be an "instance of the ideal program,
(or algorithm)".
A popular idea for instance in functional programming are to specify a
languages of "types" (or even meta-concept such as the "kinds" of Haskell
(sic!)), different from the programming language to specify a subset
of properties of the above kind, and used to verify whether a program
is well-formed with respect to the type. A more classical approach uses
some form of logic, first-order predicate logic, perhaps also with some
modal operators to express properties of time etc.
In either case we need to have means to establish relations between
specifications on different levels, hence the so called "semantic gap"
between the (type) specification and the actual code.
Trying to use logic as a programming language, could perhaps be seen
as an attempt to reduce this gap, making programmers more aware of
the close connection between the logic of proving properties of
specifications and the operational semantics of programming.
So far we haven't seen a logic programming language that meet such
standards. Prolog is one failed attempt, (a subset of) Mozart could
well be seen as a promising alternative.
-Thomas S.
-
Please send submissions to [email protected]
and administriva mail to [email protected].
The Mozart Oz web site is at http://www.mozart-oz.org/.