[Prev][Next][Index][Thread]
Logic programming in a fragment of linear logic
Date: Fri, 17 Apr 92 11:53:03 EDT
To: linear@cs.stanford.edu
The following paper is available by anonymous ftp. It describes a linear
logic refinement to the foundation of the lambda Prolog programming
language.
Logic Programming in a Fragment of Intuitionistic Linear Logic
Joshua S. Hodas and Dale Miller
Computer Science Department
University of Pennsylvania
Philadelphia, PA 19104-6389 USA
When logic programming is based on the proof theory of intuitionistic logic,
it is natural to allow implications in goals and in the bodies of clauses.
Attempting to prove a goal of the form D => G from the context (set of
formulas) Gamma leads to an attempt to prove the goal G in the extended
context Gamma U {D}. Thus during the bottom-up search for a cut-free proof
contexts, represented as the left-hand side of intuitionistic sequents, grow
as stacks. While such an intuitionistic notion of context provides for
elegant specifications of many computations, contexts can be made more
expressive and flexible if they are based on linear logic. After presenting
two equivalent formulations of a fragment of linear logic, we show that the
fragment has a goal-directed interpretation, thereby partially justifying
calling it a logic programming language. Logic programs based on the
intuitionistic theory of hereditary Harrop formulas can be modularly
embedded into this linear logic setting. Programming examples taken from
theorem proving, natural language parsing, and data base programming are
presented: each example requires a linear, rather than intuitionistic,
notion of context to be modeled adequately. An interpreter for this logic
programming language must address the problem of splitting contexts; that
is, when attempting to prove a multiplicative conjunction (tensor), say (G1
tensor G2), from the context Delta, the latter must be split into disjoint
contexts Delta1 and Delta2 for which G1 follows from Delta1 and G2 follows
>from Delta2. Since there is an exponential number of such splits, it is
important to delay the choice of a split as much as possible. A mechanism
for the lazy splitting of contexts is presented based on viewing proof
search as a process that takes a context, consumes part of it, and returns
the rest (to be consumed elsewhere). In addition, we use collections of
Kripke interpretations indexed by a commutative monoid to provide models for
this logic programming language and show that logic programs admit a
canonical model.
[[Accepted to the Journal of Information and Computation.]]]
This paper can be retrieved by anonymous ftp using the instructions below.
If you want a copy but cannot use ftp to this site, send me
(dale@cis.upenn.edu) your postal address.
% ftp ftp.cis.upenn.edu
Name: anonymous
Password: <<your e-mail address>>
ftp> cd pub/papers/miller
ftp> binary
ftp> get ic92.dvi.Z
ftp> quit
Use the unix uncompress command on this file to get ic92.dvi. The file
llinterp.tar.Z is also available: it contains a simple Prolog implementation
of an interpreter described in the above paper. Some examples are also
included.