Cadmium - ACD Term Rewriting

Δ Cadmium

Cadmium is an implementation of Associative Commutative Distributive Term Rewriting (ACDTR); a generalization of Constraint Handling Rules and Term Rewriting.

Cadmium was developed during my time at NICTA working for the G12 project. The rights were later transferred to Opturion, who have decided to release a standalone version of Cadmium under a permissive MIT license.

Δ Overview

Cadmium is similar to Constraint Handling Rules (CHR), except that (1) there are no propagation rules, and (2) Cadmium rules can rewrite arbitrary terms as opposed to just constraints. For example, the following rules define a length/1 function:

    length([]) <=> 0.
    length([X|Xs]) <=> 1 $+ length(Xs).
Here $+ is the built-in integer addition function.

Cadmium can also rewrite constraints (similar to CHR), e.g.

    leq(X, Y) /\ leq(Y, X) <=> X = Y.

Cadmium supports AC-matching for associative-commutative operators, i.e. any operator (+) that satisfies the following axioms:

(a + b) = (b + a)
(a + (b + c)) = ((a + b) + c)
Therefore the rule:
    1 + X <=> inc(X).
will match any of the terms 1+2, 3+1, 5+((2+1)+4), etc. All of the operators (/\), (\/), (+), and (*) are AC by default.

Conjunction is also a special distributive operator, meaning that the simpagation rule:

    p(X) \ q(X) <=> r(X).
will match wherever a term match p(X) distributes to a term matching q(X). For example, the above rule will rewrite:
    p(1) /\ f(1, 2, q(1) /\ q(2))
    p(1) /\ f(1, 2, r(1) /\ q(2))

Δ Downloads

© Copyright 2014, all rights reserved