A partial evaluator runs the parts of a program whose inputs are known and leaves the rest as smaller “residual” code. This example specializes a tiny expression language: known variables are substituted, constant arithmetic is folded, and branches with a known condition are chosen in advance.
Run it in the playground · Source
Suppose x is known to be 10 but y will only arrive at run time. Then
x * y + (x + 3) can already be simplified to 10 * y + 13. A conditional
whose test is known can lose its other branch entirely.
Partial evaluation is the idea behind specializing interpreters into compilers. Here it is shown at the smallest useful scale.
program(poly_y,
add(mul(var(x), var(y)), add(var(x), const(3))),
[bind(x, const(10))]).
program(static_branch,
if(bool(true), add(var(x), const(1)), mul(var(y), const(999))),
[bind(x, const(10))]).
program(dynamic_branch,
if(var(flag), add(var(x), const(1)), mul(var(y), const(2))),
[bind(x, const(10))]).
Expressions are ordinary terms. The environment lists the variables whose values are known; everything else is dynamic.
pe(Env, var(Name), Value) :- known_var(Env, Name, Value).
pe(Env, var(Name), var(Name)) :- unknown_var(Env, Name).
pe(Env, add(Left, Right), const(Sum)) :-
pe(Env, Left, const(A)),
pe(Env, Right, const(B)),
(Sum is A + B).
pe(Env, add(Left, Right), add(Left_residual, Right_residual)) :-
pe(Env, Left, Left_residual),
pe(Env, Right, Right_residual),
\+ ((Left_residual = const(_A)), (Right_residual = const(_B))).
pe(Env, Expr, Residual) relates an expression to its specialized form. Fold
when both operands became constants; otherwise keep the operation as residual
code. The negated test makes the two cases exclusive, so each expression has
exactly one residual.
eyeprolog examples/partial-evaluator.pl
partialEvalAnswer(residual(poly_y), add(mul(const(10), var(y)), const(13))).
partialEvalAnswer(residual(static_branch), const(11)).
partialEvalAnswer(residual(dynamic_branch), if(var(flag), const(11), mul(var(y), const(2)))).
partialEvalAnswer(note, "static inputs are folded while dynamic variables remain as residual code").
poly_y becomes 10 * y + 13. The static branch collapses to the constant
11, and the unused 999 branch disappears. The dynamic branch keeps its
conditional, but each branch is specialized.
step(pe([bind(x, const(10))], add(var(x), const(3)), const(13)),
rule(12),
['Env' = [bind(x, const(10))],
'Left' = var(x),
'Right' = const(3),
'Sum' = 13,
'A' = 10,
'B' = 3],
[pe([bind(x, const(10))], var(x), const(10)),
pe([bind(x, const(10))], const(3), const(3)),
13 is 10 + 3]).
step(\+ known_var([bind(x, const(10))], y, __anon3), absent, [], []).
x + 3 folds to 13 because x specializes to 10, the constant 3 stays 3, and
13 is 10 + 3. The second step records why y stays residual: it is not a
known variable. That is a negation, recorded as an absent step.
condition('C1', resolution, ok, 28).
condition('C6', boundary_consistency, ok, 2).
obligation(absent, theory_scoped, \+ known_var([bind(x, const(10))], y, A)).
trusted(5).
claims(4).
verdict(checked_with_obligations).
28 steps replay against the program, and the checker decides two ground negations again itself. Five negations remain: each says that some goal has no proof, for any value of its open variables. They are listed as obligations. The checker still tested two of them against the evidence it had and found none contradicted (C6), so the verdict is valid given those obligations.
bind(y, const(2)) to the poly_y environment and predict the residual.
It should fold all the way to a constant.flag to bool(false) in dynamic_branch and check which branch
survives.sub/2 to the language with its own folding and residual clauses.Learn more in The Art of EyeProlog, Chapter 23.