I have been exploring some ideas about applying confluence techniques from term rewriting to programming-languages meta-theory, and I wanted to report about a really cool tool for confluence-checking, called ACP. This tool uses a barrage of advanced techniques to try to prove confluence of a first-order term rewriting system fully automatically. It was quite easy to set up and use. I followed these steps (explained on the web page), on Ubuntu:
- download SML heap image for ACP (first had to do “sudo apt-get install smlnj”, which gave me SML/NJ 110.67).
- download a minisat executable (I just grabbed an old pre-compiled executable).
- download yices2
- run the following command with a test file:
sml @SMLload=acp.x86-linux –minisat-path ~/provers/MiniSat_v1.14_linux –yices-path ~/provers/yices2smt09/bin/yices testfile.trs
The authors provide a tarball with a bunch of examples. From those, it was easy to construct an example for (typed) S,K,Y combinators (the types do not play a role here yet):
(VAR a b c A B C)
app(app(app(S(A,B,C),a),b),c) -> app(app(a,c),app(b,c))
app(app(K(A,B),a),b) -> a
app(Y(A),a) -> app(a,app(Y(A),a))
ACP reported immediately that this is confluent. Adding some other rules that I knew would break confluence resulted in ACP reporting non-confluence, again almost immediately. Very impressive.
[Update: Harley Eades has posted instructions in one of the comments on how to get ACP running on the Mac. ]