add simplification to the expansion mechanism, the basic idea

[Jan Burse]

Dear All,

I am looking for a name of the following idea. Some couple
of months ago I saw a term rewriting termination proof
paper that basically explained this idea. But I cannot
find it anymore.

The idea goes as follows. Lets assume that the
expansion + simplification pipeline produces normal
forms. So the signature of this pipeline is basically:

exp + simp : term -> norm

Where norm denotes the domain of normal forms. Now
the curcial step is to assume that inbetween exp and
simp we get semi-normal forms. So that we have:

exp : term -> semi-norm
simp : semi-norm -> norm

What is the domain of semi normal forms and why does
it matter. The definition is as follows. Semi normal
forms are compounds where all the arguments are already
in normal form, but the whole compound is not yet
necessarely in normal form:

semi-norm = f(norm,..,norm)

Take a little example from polynoms:

norm : 1 + 2*x
norm : 4 - 3*x
semi-norm: (1 + 2*x) + (4 - 3*x)
norm: 5 - 1*x

Why does it matter. Well transitioning semi-norms to
norms can of be considered a simpler problem than the
full normalization problem, since we have the invariant
that the arguments of the compound are already normalized.

How can we practially extend the term expansion mechanism
by a simplfication step and what would be the applications?
We can simply hook into the term expansion mechansim at
its end. This is the code skeleton of the term expansion
mechansim without simplification (only looking at goal
expansion right now, and sketch only):

expand_goal(X,Y) :-
goal_expansion(X,Z), !, expand_goal(Z,Y).
expand_goal(X,Y) :-
... check whether meta/special ... !,
... perform meta/special, will
call expand_goal for subterms ...
expand_goal(X,X).

Now for the simplication we also provide the positibility
to define hooks by the end user. So there are similar
verbs. Just compare:

expand_goal simplify_goal
goal_expansion goal_simplification

The simplification hooking looks a little bit different
from the expansion hooking. We do not provide a looping,
it will be the task of the simplification hook itself
to call simplification recursively:

simplify_goal(X,Y) :- goal_simplification(X,Y), !.
simplify_goal(X,X).

And the integration with the goal expansion
looks as follows. There are two places where
we have to inject the simplify_goal/2 predicate
at the end of the expand_goal/2 predicate:

expand_goal(X,Y) :-
goal_expansion(X,Z), !, expand_goal(Z,Y).
expand_goal(X,Y) :-
... check whether meta/special ... !,
... perform meta/special, will
call expand_goal for subterms ...
simplify_goal(Z,Y).
expand_goal(X,Y) :-
simplify_goal(X,Y).

What can be done with simplify_goal/2. Lot of nice
things, which are sometimes done natively in the
interpreter, can now be done in Prolog itself. And
there is no big performance overhead. Here is the
code how to flatten out conjunctions:

goal_simplification((A,_), _) :- var(A), !, fail.
goal_simplification(((A,B),C), (A,D)) :-
simplify_goal((B,C), D).

The above rule highly makes use of some normal form
assumptions. In the first argument we will get (norm,norm),
but the whole compound need not yet be in normal form.
If the first argument of the compound is in normal form
and has the form (A,B) then we know that A will not have
a conjunction in its root, so we can move it to the result
without any modification. Also if (A,B) is a normal form
then B is a normal form, so we can correctly invoke simplify
goal again. All that counts for the speed of the method.
It should be noted that the form of the normal form
is not prescribed, it emerges from exp+simp, but it is
a good praxis to think of it as predefined and then verify
your code against it.

I made a little test. Some the Prolog systems do
flattening of conjunction. But I guess it is done natively.
Here are some results:

SWI Prolog 6.0.0: Flattens (,)/2
?- [user].
:- dynamic p/0.
p :- (a,b),c.
^D
?- clause(p,((a,b),c)).
false

GNU Prolog 1.4.0: Does not flatten (,)/2
?- [user].
:- dynamic(p/0).
p :- (a,b),c.
^D
?- clause(p,((a,b),c)).
Yes

I don't know what the position of ISO Prolog is here, whether flatten
is allowed? I don't see some flattening in the definition of body
conversion. But anyway, here is a little experiment of flatting
of disjunction. The simplifications for this flattening are
analogous:

goal_simplification((A;_), _) :- var(A), !, fail.
goal_simplification(((A;B);C), (A;D)) :-
simplify_goal((B;C), D).

Here are some results:

SWI Prolog 6.0.0: Does not flatten (;)/2
?- [user].
:- dynamic q/0.
q :- (a;b);c.
^D
?- clause(p,((a;b);c)).
true

Jekejeke Prolog 0.9.3: Experimental flattening of (;)/2
?- [user].
:- dynamic q/0.
q :- (a;b);c.
^D
?- clause(q,((a;b);c)).
No

I am currently in the process of integrating simplification
into Jekejeke Prolog, this is driven by a couple of application
scenarios where a tight integration seems more useful than for
example a Prolog text rewriting technique.

Any Prolog systems around that also provide "simplification"
for the end-user?

Bye

[Jan Burse]

Dear All,

Was drawing from linear logic to solve some name clash.
Was looking for an operator that could serve me as an
indicator for multiple clauses during assert or consult,
as a result from term expansion.

It seems that multiplicative conjunction (x) and
multiplicative 1 from linear logic do a good job. They
have the following inference rules:

G, A, B |- C
--------------- (Left (x))
G, A (x) B |- C

G, |- A
--------- (Left 1)
G, 1 |- A

So they are a perfect fit and one can avoid clash with
(.)/2 (some Prolog systems allow lists to be returned
by term_expansion to indicate multiple clauses),
since (.)/2 is used in the consult shorthand [file1,
...,file2] as a goal functor, and there is also no
clash with (,)/2 which might have a meta definition.

I use ascii '&' for linear logic (x), and ascii 'unit' for
linear logic 1. So one can now do:

?- assertz((a&unit&b)).
?- listing.
:- dynamic a/0.
a.
:- dynamic b/0.
b.

The thing is scheduled for release 0.9.4 of Jekejeke Prolog.

Best Regards

SEP Entry on Linear Logic
http://plato.stanford.edu/entries/logic-linear/


Jan Burse schrieb:

> Dear All,
>
> I am looking for a name of the following idea. Some couple
> of months ago I saw a term rewriting termination proof
> paper that basically explained this idea. But I cannot
> find it anymore.
>
> The idea goes as follows. Lets assume that the
> expansion + simplification pipeline produces normal
> forms. So the signature of this pipeline is basically:
>
> exp + simp : term -> norm
>
> Where norm denotes the domain of normal forms. Now
> the curcial step is to assume that inbetween exp and
> simp we get semi-normal forms. So that we have:
>
> exp : term -> semi-norm
> simp : semi-norm -> norm
>

Jan Burse schrieb:
> Then we would have, that inside a file:
>
> p(a), p(b) :- q(c).
>
> Would be the same as:
>
> p(a) :- q(c). p(b) :- q(c).