Lazy predicates (experimental)

WARNING: this is an unusually experimental feature introduced in 0.1.3 and is likely to break, change, or be removed in future releases.

Lazy predicates allow a limited form of “backward-chaining,” or “Prolog-style,” or “top-down” logic programming in Dusa. Normally, a program like this one will never terminate, because you can always generate new nat facts once you start generating them:

nat z.
nat (s N) :- nat N.

However, by making nat a “lazy” predicate, we only derive the nat facts that we absolutely need to run other parts of our program.

#lazy nat
nat z.
nat (s N) :- nat N.

p (s (s z)).
p "hello".
p 4.

q X :- p X, nat X.

Explore this example

Dusa implements lazy predicates by applying a program transformation called the “magic sets” or “demand” transformation. It’s helpful to have a bit of a mental model of how this transformation actually works. The program above is transformed into (more or less) this program by the demand transformation:

#lazy nat
nat z :- demand_nat z.
nat (s N) :- demand_nat (s N), nat N.
demand_nat N :- demand_nat (s N).

p (s (s z)).
p "hello".
p 4.

q X :- p X, nat X.
demand_nat X :- p X.

Inputs and outputs

The simple lazy transformation currently implemented treats the arguments to a lazy predicate as “inputs”, which means that whenever they appear in a premise they have to be bound by previous premises. The exception is the value of a functional predicate, which is treated as an output. That allows for the writing of (some) Prolog-style logic programs that compute values, like this:

#lazy plus
plus z N is N.
plus (s N) M is (s P) :- plus N M is P.

#demand plus (s (s (s (s z)))) (s (s (s z))) is N.

Explore this example

Lazy predicates can refer to other lazy predicates, which enables this Prolog-style implementation of quicksort:

#lazy sort
sort nil is nil.
sort (cons X Xs) is Sorted :-
 partition X Xs is (tuple As Bs),
 append (sort As) (cons X (sort Bs)) is Sorted.

#lazy partition
partition X nil is (tuple nil nil).
partition X (cons Y Ys) is (tuple (cons Y As) Bs) :-
 partition X Ys is (tuple As Bs),
 Y <= X.
partition X (cons Y Ys) is (tuple As (cons Y Bs)) :-
 partition X Ys is (tuple As Bs),
 Y > X.

#lazy append
append nil Ys is Ys.
append (cons X Xs) Ys is (cons X (append Xs Ys)).

Explore this example