Skip navigation

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:

  1. download SML heap image for ACP (first had to do “sudo apt-get install smlnj”, which gave me SML/NJ 110.67).
  2. download a minisat executable (I just grabbed an old pre-compiled executable).
  3. download yices2
  4. 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)
(RULES

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. ]

Advertisements

5 Comments

  1. This is great. How does it go about proving confluence for any arbitrary TRS? I bet critical pairs are in there somewhere.

  2. Yes, critical pairs are used, but there are many more advanced techniques that get used for these tools as well, like decreasing diagrams. But I do not know this literature well enough to try to summarize more.

  3. I just got ACP working on my laptop running Mac OS X Snow Leopard. I noticed there is literly no help on getting this up and running on a Mac. So I hope you don’t mind me posting it here. That way people searching for help will find it.

    First ACP itself is easy. Simply download the file from there site. Now to get things rolling you have to download and install yices. This is also easy. They provide a binary for the Mac. The hard part is getting Minisat working. Their current release does not build on the Mac.

    To get Minisat built apply the following patch:

    diff -ru minisat/utils/System.cc minisat_fixed/utils/System.cc
    — minisat/utils/System.cc 2010-07-10 11:07:36.000000000 -0500
    +++ minisat_fixed/utils/System.cc 2010-10-28 22:52:04.000000000 -0500
    @@ -88,7 +88,7 @@
    malloc_statistics_t t;
    malloc_zone_statistics(NULL, &t);
    return (double)t.max_size_in_use / (1024*1024); }

    +double Minisat::memUsedPeak(void) { return memUsed(); }
    #else
    double Minisat::memUsed() {
    return 0; }

    This prevents the linker from giving an error. After that just follow what Aaron has in his post.

    One more note. I noticed that the syntax used in the post is slightly different then ACP for the Mac. Just run `sml @SMLload=./acp.x86-darwin –help` to get the correct syntax.

    Anyway, maybe this will prevent someone from getting a headache.

    Harley

  4. I am wondering. Do you have any references on how to incorporate types into TRSs?


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: