sml-rewrite

First-order term rewriting in pure Standard ML: substitution, one-way matching, Robinson unification (with occurs-check), leftmost-outermost rewriting and normalisation, the lexicographic path order (LPO), critical pairs, and Knuth-Bendix completion.

A term is a variable or a function symbol applied to arguments:

datatype term = Var of string | App of string * term list

Constants are nullary applications (App ("e", [])). A substitution is an association list; a rule is a lhs -> rhs pair.

No dependencies, no FFI, no threads, no clock, no randomness: the same inputs always produce the same outputs under MLton and Poly/ML. Variable renaming for critical pairs and the canonicalisation of completed rules use a fixed deterministic scheme, so completed systems are reproducible.

API

structure Rewrite : sig
  datatype term = Var of string | App of string * term list
  type subst = (string * term) list
  type rule  = term * term
  type rules = rule list

  val toString : term -> string
  val termEq   : term -> term -> bool
  val vars     : term -> string list
  val size     : term -> int
  val isVar    : term -> bool

  val apply    : subst -> term -> term
  val match    : term -> term -> subst option    (* one-way *)
  val unify    : term -> term -> subst option     (* Robinson + occurs-check *)

  val rewrite1 : rules -> term -> term option     (* one leftmost-outermost step *)
  exception Loop
  val normalize        : rules -> term -> term
  val normalizeBounded : int -> rules -> term -> term option
  val joinable         : rules -> term -> term -> bool

  val lpoGt        : (string * string -> bool) -> term -> term -> bool
  val precedenceOf : string list -> (string * string -> bool)   (* highest first *)
  val criticalPairs : rule -> rule -> (term * term) list
  val complete : (string * string -> bool) -> int
                 -> (term * term) list -> rules option
end

Example

val zero = Rewrite.App ("0", [])
fun s t = Rewrite.App ("s", [t])
fun plus a b = Rewrite.App ("+", [a, b])
val peano =
  [ (plus zero (Rewrite.Var "y"), Rewrite.Var "y")
  , (plus (s (Rewrite.Var "x")) (Rewrite.Var "y"), s (plus (Rewrite.Var "x") (Rewrite.Var "y"))) ]

(* 2 + 3 normalises to 5 *)
val five = Rewrite.normalize peano (plus (s (s zero)) (s (s (s zero))))

complete runs Knuth-Bendix completion: it orients equations with the LPO induced by a symbol precedence, computes and joins critical pairs, and interreduces, returning a confluent terminating rewrite system that decides the word problem for the input theory.

Running examples/demo.sml with make example prints (note the classic ten-rule complete system for free groups):

Unification:
  f(x,b) =?= f(a,y) : x=a, y=b
  x =?= f(x)        : no unifier (occurs check)

Peano normalisation:
  2 + 3 = 5
  2 * 3 = 6

Knuth-Bendix completion of the group axioms (i > * > e):
  completed to 10 rules:
    *(e,x) -> x
    *(i(x),x) -> e
    *(*(x,y),z) -> *(x,*(y,z))
    *(i(x),*(x,y)) -> y
    i(e) -> e
    i(i(x)) -> x
    *(x,e) -> x
    *(x,i(x)) -> e
    *(x,*(i(x),y)) -> y
    i(*(x,y)) -> *(i(y),i(x))
  derived identities (equal normal forms):
    x*e = x        : true
    x*i(x) = e     : true
    i(i(x)) = x    : true
    i(x*y)=i(y)*i(x): true

Build & test

Requires MLton and/or Poly/ML.

make test        # build + run the suite under MLton
make test-poly   # run the suite under Poly/ML
make all-tests   # both
make example     # build + run the demo
make clean

Installing with smlpkg

smlpkg add github.com/sjqtentacles/sml-rewrite
smlpkg sync

Reference lib/github.com/sjqtentacles/sml-rewrite/rewrite.mlb from your own .mlb (MLton / MLKit), or feed sources.mlb to tools/polybuild (Poly/ML).

Layout

sml.pkg                                      smlpkg manifest
Makefile                                     MLton + Poly/ML targets
.github/workflows/ci.yml                     CI: MLton + Poly/ML
lib/github.com/sjqtentacles/sml-rewrite/
  rewrite.sig   REWRITE signature
  rewrite.sml   terms, unification, LPO, Knuth-Bendix completion
  sources.mlb / rewrite.mlb
examples/
  demo.sml      unification + Peano + group completion walkthrough
test/
  harness.sml / test.sml                     41 reference checks
  entry.sml / main.sml
tools/polybuild                              Poly/ML build wrapper

Tests

41 deterministic checks: term/toString/vars, one-way matching, Robinson unification (including occurs-check and symbol-clash failures), Peano addition/multiplication as a confluent terminating system, lexicographic path order facts, critical-pair computation, and Knuth-Bendix completion of the group axioms — verified through the word problem (the classic derived identities x*e = x, x*i(x) = e, i(i(x)) = x, i(x*y) = i(y)*i(x) all reduce to equal normal forms, while x*y and y*x do not), plus a check that every critical pair of the completed system is joinable. Run make all-tests to verify identical output under both compilers.

License

MIT. See LICENSE.