[stack] Prolog and Rewriting Strategies

Manfred's recent post about Prolog got me thinking about using a Polog
style language for term rewriting. For example, we could express the
fact that "swap swap" evaluates to a no-op below:

inverse(swap, swap) :- true
inverse('a add, 'a sub) :- true
$f $g | inverse($f, $g) == id

Hopefully the syntax is somewhat self explanatory? The last line reads
as "given two functions, where those functions are inverses, replace
with the function id".

I believe that this kind of term rewriting language could be a useful
a preprocessing language for a concatenative language.

I am hoping to be able to take advantage of the algebraic identities
expressed by Manfred in his paper "The Algebra of Joy" (
http://www.latrobe.edu.au/philosophy/phimvt/joy/j04alg.html )

The rest of this post contains a bunch of examples demonstrating how
such a language might work in practice:


// These are the relation definitions
assoc_comm($f) :- assoc($f), comm($f)
assoc_comm(add) :- true
assoc_comm(mul) :- true
assoc_comm(union) :- true
assoc_comm(intersection) :- true
assoc_comm(symm_diff) :- true
assoc_comm(and) :- true
assoc_comm(or) :- true
assoc_comm(xor) :- true
inverse(inc, dec) :- true
inverse(succ, pred) :- true
inverse('a add, 'a sub) :- true
inverse('a mul, 'a div) :- true
involutive($f) :- inverse($f, $f)
involutive($f) :- assoc_comm($f)
involutive(id) :- true
involutive(complement) :- true
involutive(neg) :- true
involutive(not) :- true
involutive(reverse) :- true
involutive(reciprocal) :- true
involutive(swap) :- true
comm($f) :- comm2($f, $f)
assoc(compose) :- true
assoc(gcd) :- true
assoc(lcm) :- true
distr(mul, add) :- true
distr(and, or) :- true
anticomm(sub) :- true
idempotent(abs) :- true
idempotent(ceil) :- true
idempotent(floor) :- true
idempotent(round) :- true
idempotent(trunc) :- true
demorgan(complement, union, intersection) :- true
demorgan(complement, intersection, union) :- true
demorgan(not, or, and) :- true
demorgan(not, and, or) :- true
demorgan(sqr, mul, mul) :- true
demorgan(log, plus, mul) :- true
distr_compose(map) :- true
comm_map(cdr) :- true
comm_map([$f] filter) :- true
comm_map('a drop) :- true
comm_map('a take) :- true

// These are the rewriting rules
[$f] eval == $f
[$f] [$g] compose == $f $g
[$f] [$g] compose | comm2($f, $g) == [$g] [$f] compose
'a 'b $f | comm($f) == 'b 'a $f
'a 'b $f 'c 'b $f $g | distr($f, $g) == 'a 'c $g 'b $f
'a 'b or not == 'a not 'b not and
'a 'b and not == 'a not 'b not or
'a $f 'b $f $g | demorgan($f, $g, $h) == 'a 'b $h $f
'a $f $g | inverse($f, $g) == 'a
$f:('A -> 'B) $g:('C -> 'D) == 'B = 'C
'A $f:('A -> 'B) == 'B
$f $f | idempotent($f) == $f
'a 'b or 'b and == 'b
'a 'b and 'b or == 'b
[$f] map $g | comm_map($g) == $g [$f] map
[$a] $f [$b] $f | distr_compose($f) == [$a $b] $f

Any thoughts?