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?
Christopher Diggins <cdiggins@...> wrote:
> I believe that this kind of term rewriting language could be a usefulI would expect it to be quite useful (although of course one would
> a preprocessing language for a concatenative language.
have to be careful about lists, but I understand Cat is careful).
Another thing to watch out for would be types. add and sub may be
inverses (kind of, if they were reversible), but just because their
stack effect is empty doesn't mean they can appear on any stack -- a
stack with two pointers on top can't be added.
-Billy
On 26/3/07 6:35 PM, "Christopher Diggins" <cdiggins@...> wrote:
> Manfred's recent post about Prolog got me thinking about using a PologWell, yes, one could do the term rewriting in a style as you propose:
> 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
>
> [..]
>
Give names to various relations between functions (or operators),
and then use the relations as preconditions for rewriting. But where
you wrote
>that is taken to mean: provided $f is idempotent, $f $f == $f
> $f $f | idempotent($f) == $f
>
which I would have written in Prolog as
(F,F) == F :- idempotent(F)
But you will need to give one definition of idempotency, and a list of those
functions which are idempotent. That list will be exactly as long as saying,
for each function, that they satisfy the defining property of being
idempotent. So it is a choice between ³idempotent (abs)² and ³abs abs ==
abs², and similarly for all the other idempotent functions. It may be that
rewriting is easier your way, but maybe it isn¹t. Certainly, giving names
to the laws adds some complexity to the rewriting system which may not
pay off in the long run. But I am not sure at all. My only experience with
(tree-)rewriting has been with simple desk-calculator evaluators in
teaching,
and later with Joy, which is essentially rewriting a program using a stack
to keep track of where rewriting occurs. (I have said several times that
I do not regard the stack as essential for a concatenative language).
Anyhow, I am just not sure whether the naming simplifies the rewriting.
Nice idea, though. I seem to remember the expression ³conditional rewriting
systems²
in the literature. That might be worth googling for.
- Manfred
[Non-text portions of this message have been removed]
Manfred Von Thun <m.vonthun@...> wrote:
> to keep track of where rewriting occurs. (I have said several times thatI believe Enchilada has proven this point. I personally didn't expect
> I do not regard the stack as essential for a concatenative language).
that to be at all efficient, but it is.
> - Manfred-Billy