Implement demand/magic sets transformation

[robsimmons]

I need to better understand how this relates to the "demand" or "magic sets" transformation, but I really think the right move for Dusa is to declare certain predicates to be demand-driven, and then automatically do the magic-sets transformation on them.

In Dusa, it seems reasonable to connect this with the functional predicate transformation: for a predicate d X Y is Z, the only mode you get is d + + is -. That is, the stuff to the left of the “is” is input, the stuff to the right of the “is” is output. It is not particularly orthogonal language design to tie functional predicates to a demand transformation like this, but, well, my hunch is that this will be a lot simpler, and my experience from Advent of Code was that this was the only version that it was painful to do without, and the only one that I wanted.

As a example that's simple but silly because we already have integer addition, we might want to implement unary addition in Dusa:

add z N is N.
add (s N) M is (s P) :- add N M is P.

b P :- a N, a M, add N M is P, c P.

This doesn't work for two reasons:

1. The first rule isn't range restricted.
2. The second rule, if it can fire at all, will fire in an unrestricted manner.

The demand/magic sets transformation introduces a new predicate, needAdd. It uses the invariant that we will only introduce a fact of the form add t1 t2 is X if the database already includes a fact of the form needAdd t1 t2. Uses of the demanded add relation in premises require us to add new rules that derive needAdd:

add z N is N :-
   needAdd z N.

needAdd N M :-
   needAdd (s N) M.
add (s N) M is (s P) :-
   add N M is P.

needAdd N M :-
   a N, a M.
b P :-
   a N, a M, add N M is P, c P.

This transformation has the same vibe as the one that translates ASP to Dusa - a negated premise represents a "demand that this attribute potentially be ff"

Note on the literature: I thought "magic sets" and "demand transformation" were the same thing, but according to the "Datalog: concepts, history, and outlook" paper they are different. Possibly they're the same when restricted to operating with functional predicates in the way I'm proposing.

[robsimmons]

In Masto conversations with Kris Micinski I was again reminded of how badly I want this feature for a number of examples.

First example: type synthesis

This whole thing would be vastly more clear, I think, written as follows:

#magic lookup
lookup (cons X V Rho) X is V.
lookup (cons Y Vy Rho) X is V :-
   Y != X,
   lookup Rho X is V.

#magic typeOf
typeOf Gamma (var X) is T :-
   lookup Gamma X is T.
typeOf Gamma (lam X T1 E) is (arr T1 T2) :-
   typeOf (cons X T1 Gamma) E is T2.
typeOf Gamma (app E1 E2) is T2 :-
   typeOf Gamma E1 is (arr T1 T2),
   typeOf Gamma E2 is T1.
typeOf Gamma (num N) is nat.
typeOf Gamma (addOne E) is nat :-
   typeOf Gamma E is nat.

addTwo is (lam "x" nat (addOne (addOne (var "x")))).
applyThrice is 
   (lam "f" (arr nat nat) 
      (lam "x" nat
         (app (var "f") (app (var "f") (app (var "f") (var "x")))))).
problem is (app (app applyThrice addTwo) (num 5)).
demand_typeOf nil problem.
aa_answer is T :- typeOf nil problem is T.

Second example, CBV evaluation of lambda calculus

Again, the program I want to be able to write is shorter and, I think, much clearer. The extra stuff needed to make this ^^ program work doesn't aid understanding at all.

#builtin NAT_SUCC s.

#magic lookup
lookup (cons X V Rho) X is V.
lookup (cons Y Vy Rho) X is V :-
   Y != X,
   lookup Rho X is V.

#magic eval
eval (var X) Rho is V :-
   lookup Rho X is V.
eval (lam X E) Rho is (clo X E Rho).
eval (app Ef Ea) Rho is V :-
   eval Ef Rho is (clo X Eb RhoLam),
   eval Ea Rho is Va, 
   eval Eb (cons X Va RhoLam) is V.
eval (num N) Rho is (num N).
eval (addOne E) Rho is (num (s N)) :-
   eval E Rho is (num N).

# Example 1: trying and failing to compute omega
aa_omega_eval is V :-
  eval
    (app 
      (lam "x" (app (var "x") (var "x")))
      (lam "y" (app (var "y") (var "y"))))
    nil
    is V.

# Example 2: computing thirty with church numerals
zero is (lam "f" (lam "x" (var "x"))).
succ is (lam "n" (lam "f" (lam "x" 
       (app (var "f") (app (app (var "n") (var "f")) (var "x")))))).
mult is (lam "m" (lam "n" (lam "f" (lam "x"
       (app (app (var "m") (app (var "n") (var "f"))) (var "x")))))).
five is (app succ (app succ (app succ (app succ (app succ zero))))).
problem is 
   (app 
   (app 
   (app (app mult five) (app succ five)) 
      (lam "x" (addOne (var "x")))) 
      (num 0)).
aa_thirty is X :- eval problem nil is X.

[robsimmons]

Honestly, one of the reasons I've delayed on this is that I slightly regret the #forbid / #demand syntax naming, because I think the "demand transformation" is very clear about what these transformed predicates are doing, and I'd like to be able to say #demand eval, but that's a name clash.

As a first step, I think #magic eval as described above is good enough as a spec of what's supposed to happen here.

[robsimmons]

Concrete proposal: add a #lazy directive for the demand-driven transformation

#lazy eval

This directive

• Introduces a new predicate, $force-eval, which is not visible or available to the user ($ is how the implementation currently designates elaboration-introduced predicates)
• Adds a check: eval can only be the head of a closed rule with a single value. (Can't write eval X Y is { 1, 2 }.)
• Changes the groundness checker:
  • when eval X Y is Z appears in the head of a rule, the rule is checked for groundness as if X and Y are initially ground by an invisible first premise.
  • when eval X Y is Z appears in a premise, both X and Y must be bound by previous premises
• Changes program elaboration by adding two steps that appear one at a time:
  • when eval X Y is Z appears in the head of a rule, rewrite the rule to add a new first premise $force-eval X Y.
  • when eval X Y is Z appears as the _n_th premise of a rule, create a new rule that duplicates the first n-1 premises of the rule and has the conclusion $force-eval X Y.

[robsimmons]

Correctness statements. Initial program is P, transformed program is P'.

First statement: if P passes the modified mode checker, P' would pass an unmodified mode checker.

Second statement:
Rob is confident: [[P']] <= [[P]]
Rob speculates: [[P']] and [[P]] have a bijective correspondence with each element in [[P']] being a subset of the corresponding element in [[P]].