
CMUCS98183
Computer Science Department
School of Computer Science, Carnegie Mellon University
CMUCS98183
Ordered Linear Logic Programming
Jeff Polakow, Frank Pfenning
December 1998
CMUCS98183.pdf
Keywords: Intuitionistic noncommutative linear logic,
linear logic programming
We begin with a review of intuitionistic
noncommutative linear logic (INCLL), a refinement of linear
logic with an inherent notion of order proposed by the authors in
prior work. We then develop a logic programming interpretation for
INCLL in two steps: (1) we give a system of ordered uniform
derivations which is sound and complete with respect to INCLL, and
(2) we present a model of resource consumption which removes
nondeterminism from ordered resource allocation during search for
uniform derivations. We also illustrate the expressive power of the
resulting ordered linear logic programming language through
some examples, including programs for merge sort, insertion sort,
and natural language parsing.
33 pages
