Term-Rewriting in K [0]
=======================
0. Preliminaries.
The scripts for this project implement simple unconditional term-rewriting [1] with examples from elementary logic (conversion to conjunctive normal form) and basic arithmetic.
Arthur Whitney contributed an elegant k6 implementation of limited symbolic unification.
Subsequent versions will add conditional and default rules and a syntax for list-matching. This should be enough to model a simple (but interesting!) fragment of K as a rewriting system [2].
1. Unconditional term-rewriting in K.
An unconditional term-rewriting system consists of the following components:
- a set of rules y of the form:
:
source_pattern s -> target_pattern t
:
- a set of x logical variables x, y, z ..
- a list c of those operators which are commutative, e.g. + and *.
The algorithm n for transforming an input expression e using x, y, and c is:
begin
try to match e with a source-pattern s in y
if no match or failure, exit
a match produces a substitution-map of the form
x -> sx
:
z -> sz
generate a new e by substituting sx .. sz for x .. z in t
continue until either failure or no match is found
sort the commutative components of the result based on c.
end
Test case (from v4.k):
Rules for transforming a boolean expression into conjunctive normal form:
y:+w''(("~~x" ;"x")
("~x|y" ;"(~x)&~y")
("~x&y" ;"(~x)|~y")
("x|y&z" ;"(x|y)&x|z")
("(y&z)|x" ;"(x|y)&x|z")
("x>y" ;"y|~x")
("x=y" ;"(x>y)&y>x"))
Up to three logical variables:
x:+,"xyz"
Commmutative functions:
c:+,"|&"
- All expressions use K syntax.
- Rules understand monads and dyads (e.g. x-y and -x).
Parse (w), normalize (n), sort (s), and print (p).
if trace is on (t=1) show pairs of the form:
source-pattern -> target-pattern
input-expression -> output-expression
Example:
p s n[x;y]w"r=(~((~q)|~p))>r"
(x=y)->((x>y)&(y>x))
(r=((~((~q)|(~p)))>r))->((r>((~((~q)|(~p)))>r))&(((~((~q)|(~p)))>r)>r))
(x>y)->(y|(~x))
(r>((~((~q)|(~p)))>r))->(((~((~q)|(~p)))>r)|(~r))
(x>y)->(y|(~x))
((~((~q)|(~p)))>r)->(r|(~(~((~q)|(~p)))))
(~(~x))->x
(~(~((~q)|(~p))))->((~q)|(~p))
(x>y)->(y|(~x))
(((~((~q)|(~p)))>r)>r)->(r|(~((~((~q)|(~p)))>r)))
(x>y)->(y|(~x))
((~((~q)|(~p)))>r)->(r|(~(~((~q)|(~p)))))
(~(~x))->x
(~(~((~q)|(~p))))->((~q)|(~p))
(~(x|y))->((~x)&(~y))
(~(r|((~q)|(~p))))->((~r)&(~((~q)|(~p))))
(~(x|y))->((~x)&(~y))
(~((~q)|(~p)))->((~(~q))&(~(~p)))
(~(~x))->x
(~(~q))->q
(~(~x))->x
(~(~p))->p
(x|(y&z))->((x|y)&(x|z))
(r|((~r)&(q&p)))->((r|(~r))&(r|(q&p)))
(x|(y&z))->((x|y)&(x|z))
(r|(q&p))->((r|q)&(r|p))
"((((p|r)&(q|r))&((~r)|r))&((((~p)|(~q))|r)|(~r)))"
A. Scripts.
The existing scripts are:
the current working (and preferred) version in k4 with native parsing and sorting of commutative operators:
http://www.nsl.com/k/term_rewriting/v4.k
Previous versions have been retained:
the original implementation in k3:
http://www.nsl.com/k/term_rewriting/u3.k
the very first implementation, in k6:
http://www.nsl.com/k/term_rewriting/u.k
the k6 version with dictionary rule-set:
http://www.nsl.com/k/term_rewriting/u6.k
a version in k4, with sorting of commutative operators:
http://www.nsl.com/k/term_rewriting/u4.k
Notes:
[0] Work in progress.
[1] http://www.meta-environment.org/doc/books/extraction-transformation/term-rewriting/term-rewriting.html
[2] see e.g. http://nsl.com/papers/rewritejoy.html