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 version in k4 with native parsing and sorting of commutative operators:

    http://www.nsl.com/k/trw/v4.k

a revised version in k3 with non-native parsing and sorting of commutative operators:

    http://www.nsl.com/k/trw/trw.k

Previous versions have been retained:

the original implementation in k3:

    http://www.nsl.com/k/trw/old/u3.k

the very first implementation, in k6:

    http://www.nsl.com/k/trw/old/u.k

the k6 version with dictionary rule-set:

    http://www.nsl.com/k/trw/old/u6.k

a version in k4, with sorting of commutative operators:

    http://www.nsl.com/k/trw/old/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