Recently I’ve been trying to figure out how to cleanly place operators that take a database D to a database D’. In transactional logic we use a sequencing conjunction (and choice disjunction) in order to deal with lifting databases. This works fine as long as all programs that we write terminate. If we want non-terminating, server-like processes, than things become a little bit more complicated. In order to retain declarativeness we have to be a bit more careful. The reason is that we may have to backtrack through some effect if our computation fails. Lets look at a simple example.
P :- Q,P
We read the above statement as: “if Q and P can be proved then we will be able to prove P”. It is basically like saying Loop[Q] where Loop[] tests the truth of its argument arbitrarily many times until it happens to be false.
Of course normally this would be strictly false or bottom (non-terminating) after the first test, but if Q has effects, that is, if it lifts the total state of the database D into D’ and then D” etc. then Q could change its mind sometime in the future and it can then be either false or bottom. The difficulty comes in this eventual possible failure. Any effect that has occurred would then require us to backtrack over it and “undo” it such that we arrive back at the original state. This is not a very good way for a web-server to behave! Imagine if Yahoo! erased all memory of its e-mail users.
As I learned today on Lambda-The-Ultimate Mercury deals with this problem in declarative way (retaining declarativeness is extremely appealing to me). It works by declaring the mode of certain predicates to be “use once”. Its much like the idea of a linear resource AND the containing code must have a mode of “deterministic”, which means that the code will not under any circumstances fail. Of course that solves the whole problem about whether Q will fail, and now we don’t have to worry about backtracking.