Lambda the Ultimate

The following three predicates are found in many dialects of Prolog:

• between/3: (+,+,?) succeeds if the third value is between the first two, provided the second is greater than the first two;
• succ/2: (?,?) succeeds if the second value is the successor of the first; can trivially be defined in terms of add/sum;
• plus/3: (?,?,?); exactly equivalent to add/3 in the paper.

(For those not familiar with Prolog's arity notation, something like (+,?,?) means that a 3-place predicate can generate answers to values provided in any of the places marked "?"; the predicate will neither succeed nor fail if a logic variable is passed to a position marked "+").

These are very useful predicates in Prolog, and though they are easy enough to define in standard Prolog, their absence from the standard counts as something of a defect.

The predicates other than add/3 defined in the paper do not seem to be so useful, but the implementation is clean, it's always nice to see code justified by correctness arguments, and I enjoyed looking over the code. I'm at a bit of a loss to see the point of the paper, though: what makes this count as a scientific communication? Does it lie in the fact that their code works for several different resolution strategies? Are they trying to promote a certain resolution-strategy-insensitive coding style? I don't get it.

Is this a new axiomatization of the natural numbers? Or does it correspond to other (decidable) axiomatizations of the numbers? Is it more powerful as e.g. Presburger arithmetic?

Did you look at the implementation of arithmetic in the logics of the HOL-Light, Isabelle, or ACL2 theorem provers? I doubt that any satisfy all of your goal properties, but I suspect that each of them may satisfy more than you'd guess.

To answer several questions, I'd like to point our two premises of the
paper. It is easy to write all-mode arithmetic relations in general:
by using var/1, we determine which of the arguments are instantiated,
and so use addition, or subtraction, or generation as appropriate. In
the latter case, we may chose to propagate the addition constraint or
to residualize: suspend the evaluation of the addition making it a
constraint, to be re-evaluated when variables become sufficiently
instantiated. Mercury, for example, allows us to write different
clauses for different modes of a predicate. There is a good reason why
such a predicate must be marked unsafe in Mercury, and why the
frequent use of var/1 is discouraged. In our paper, we specifically
disavowed any use of var/1, negation or other such (reflective)
facilities. We deliberately limited ourselves to Horn clauses, and
nothing else.

There is no doubt that theorem provers or constraint solving libraries
offer very sophisticated procedures for solving arithmetic
constraints. In any such procedures, to my knowledge, we must know
where all our variables are. But in our paper, we specifically do not.
We have no idea which arguments of our goals are or contain variables,
and we cannot tell. We disclaim any and all intensional analysis. Not
that there is anything wrong with it; we merely wanted to see how much
we can do without.

Our use of SLD resolution and its simple variants -- as widely
implemented and quite efficient -- was another self-imposed
restriction. One may quite rightfully say that we deliberately painted
ourselves into the corner. On the other hand, purity and minimalism,
however difficult to live with, often offer deep and general insights.

As to the relation to Presburger arithmetic: the latter can decide
arbitrary formulas within its domain. We can fully decide only base
predicates -- addition, multiplication, etc. -- but not their
conjunctions, or conjunctions with equality. Conjunctions of the
base predicates let us express arbitrary Diofantine equations, which
are not generally decidable.

Finally, the goal of this project was not to be useful but to be
insightful (although, quite surprisingly to us, a similar development
for Curry proved to be practically useful and has become part of a
Haskell Curry implementation).

Very interesting and insightful response to the questions and comments so far. It certainly clears up the motivation for the paper a lot more. Although what you've done so far is interesting research, I'm intrigued by your description of seeing "how far you can go" in horn clauses.

Possibly an open question, but given my examples above do you think it would be possible to handle them by relaxing your stress on purity, but without introducing contraints through deferring evaluation? In particular, if you allow negation-as-failure could you rule out (with finite failure) clauses of the form add(X,[u],X)? Obviously you could rule out such a single instance of an infinite set of tuples that are not in the add relation, but what is your opinion on how far you could go in ruling out families of invalid tuples? Ie Can pure prolog + negation-as-failure model addition exactly? If it can, then is \+ a sledge-hammer in this case, or is the minimum needed to model this relation?

http://lambda-the-ultimate.org/node/2697#comment-40470
http://lambda-the-ultimate.org/node/2697#comment-40512

This is indeed a very good question. Negation-as-failure of course
helps -- but it helps too much, because Prolog's built-in negation
predicate immediately gives us var/1 (spelled as vr/1 below),
using the well-known trick:

vr(X) :- \+ \+ (X=1), \+ \+ (X=2).

When arithmetic predicates are invoked with arguments that share logic
variables, we rather sooner, in my experience, come across a recursive
invocation of a goal whose arguments differ only in the names of free
variables from the arguments of the original invocation. That
indicates that tabling will give us finite failure in this case. I
don't know if tabling will give us finite failure in all the cases
where sharing of variables across arguments would have lead to
divergence. But is seems quite likely. Tabling and the XSB system thus
appear the most promising extension to look at.

Of course checking how much more can be implemented in lambda-Prolog
(where we do have quantifiers and more general formulas), and whose
variable-scoping mechanism offers a general way to prevent unsoundness
often occurring in negation (that is, when the negated formula binds
variables that were accessible outside negation). Alas, lambda-Prolog
doesn't seem to be actively developed, although the web page
http://teyjus.cs.umn.edu/ does
show a quite recent release, after a 2-year hiatus. Hopefully the
development will continue.

I haven't (yet) read The Reasoned Schemer, which extends Scheme with logical constructs, or looked at the logic programming monads for Haskell. Do these libraries fully macro-express logic programming features in these languages, or do they only simulate them?

For example, Scheme can macro-express coroutines in terms of call/cc, so they don't have to be included as a language primitive. On the other hand, Haskell cannot macro-express call/cc, only simulate it locally using the CPS monad. Adding coroutines as primitives to Scheme would not increase expressiveness, but adding true first-class continuations to Haskell would increase expressiveness.

To gain the full expressiveness of logic programming in a functional language do you have to add primitives - as Mercury and Curry do - or do libraries suffice?