Lambda the Ultimate

...so when the conditions change, the fact no longer holds. There have been various strategies for addressing this observation: truth maintenance, circumscription, and transaction logic, to name but a few. In AI and logic programming, these all fall under the rubric of "non-monotonic" reasoning, which cognitive philosophers call "defeasible reasoning." These Logic Programming and Non-Monotonic Reasoning '07 slides (PPT) provide an excellent historical overview, while the work of John L. Pollock represents, AFAICT, the current state of the art in cognitive philosophy, particularly as brought to bear upon the questions around artificial intelligence as a practical endeavor.

a claim from which, on the current evidence, it would be perverse to withhold provisional assent. The current evidence may change.

So, the way a forward logic programming language works is that you start with a database of facts, and a collection of rules, which are of the form "if FOO, then BAR". The engine will then nondeterministically select rules and try to see if the rule's hypotheses (FOO) are in the database. If they are, it will then add the consequences (BAR) into the database and repeat, until no more consequences can be added. Now, note that the engine has to take a rule and look through the database for facts. This means that as database grows, the time it takes to fire a rule will have to go up, because it has to search through more facts before deciding that a rule does or doesn't match.

If there are a bunch of redundant facts in your database, then you can end up doing a lot of useless work. If you can remove facts from the database as they become irrelevant, preventing the engine from ever considering useless paths.

For example, suppose we have a database with facts of the form "item(x)", and we want to write a program that collects all of them into a list (in some unspecified order). So we might add the fact that "list([])" holds, and then run the following one-rule program:

   item(x)
   list(xs)
------------------- 
   list(x::xs)
   delete list(xs)
   delete item(x)

So, the way to read this is that if we find "item(x)" and "list(xs)" in the database, we delete both of those facts and replace it with a new fact "list(x::xs)". This guarantees that the algorithm can run in linear time.

If we couldn't delete facts, then we'd have to write a more complex program:

   item(x)
   list(xs)
   not_member(x,xs))
----------------------
   list(x::xs)

So at each step, we have to run a linear-time membership test, which means that even in the best case where the search never picks the wrong list() atom, we still have quadratic complexity, and in the worst case we end up generating all n! permutations of the list.

An also-relevant point is that we're often interested in deductive databases with running rules to saturation - determining the least set of facts closed under the rules. If we don't delete facts (or use linear resources) in the program above, we have a tradeoff. With the not-member test, we cannot describe lists with multiple elements (a list with two "3"s, six "1"s and one "2" - though there are ways around this problem). Without the not-member test, we face the possibility that there is no way of reaching saturation, but the program with deletion will reach "saturation."

I use scare quotes because, as described in the paper Monadic Concurrent Linear Logic Programing, the point where no more rules is different in the presence of linear resources, and is referred to there as quiescence.

Some comments in the paper make it look like a nice way to handle mutual exclusion in a logic language. In prolog if you want to handle negation, or if-then-else constructs then you need to use cuts to prevent part of the SLD tree from being searched.

The ephemeral rules look like pebbles (thinking of Cook's 3-sat proof) - so they define mutual exclusion. Each one has a cut wrapped up inside it. When you produce an ephemeral rule as the result of an inferrence you are creating a resource. Different inference rules can then consume that resource but they cannot share the pebble - it's an atomic operation that locks (or commits) to proofs that follow from that derivation.

The background logic in Section 3.2 looks more powerful than this, but this would be an interesting starting point for a language as it may make reasoning about programs with mutual exclusion easier.