Maxcompをインストールした

Maxcompはknuth-bendixのアルゴリズムないしmkbtt(多重完備化)とは別の完備化アルゴリズムおよび,それのデモプログラムです.JAISTで公開されています.
http://www.jaist.ac.jp/project/maxcomp/
個人的に完備化したい項書き換え系があったのでインストールしました.

オーダーはlpo,rpo,kboが指定できます.ただしこれについては専門的な知識が必要です.詳しい説明はTerm Rewriting and All Thatを読むなどして調べてください.

Ubuntuで動作します.今回はUbuntu 16.04上で作業しました.

1. Yices 1.0.40をインストールする

MaxcompはYices 1.0.40を利用しています.Yicesの現行バージョンは2系列なので,最新のバージョンをインストールしないよう注意してください.

http://yices.csl.sri.com/old/download-yices1-full.shtmlの「Yices with GMP dynamically linked」から「 Linux/x86_64 (64bit AMD/Intel and compatible)」を選択しDLしてください.

DLしたyices-1.0.40-x86_64-unknown-linux-gnu.tar.gzを展開したあと,libディレクトリに移動しaファイルとsoファイルをインストールします.

$ tar xvf yices-1.0.40-x86_64-unknown-linux-gnu.tar.gz
$ cd ./yices-2.5.1/lib
$ sudo install ./libyices.a ./libyices.so /usr/local/lib

2. libgmp10のインストール

こちらは公式にある手順通りに行います.
$ sudo apt-get install libgmp10 libgmp10-dev
$ sudo /sbin/ldconfig -v

3. maxcompのページからBinary Package for Ubuntu 12.04 64bitをDLする

Binary Packageが公式で公開されています.
http://www.jaist.ac.jp/project/maxcomp/

4. 3でDLしたPackageをdpkgでインストールする

$ sudo dpkg -i ./maxcomp_1.0-1_amd64.deb

インストールする手順は以上です.これでTermからmaxcompが動かせるようになっているはず.

動かしてみる

成功例として群を完備化してみます.

$ vim group.trs

(VAR x y z)
(RULES
  *(*(x, y), z) -> *(x, *(y, z))
  *(x, e) -> x
  *(x, i(x)) -> e
)

$ maxcomp -s lpo group.trs

EQUATIONS: 
times(times(x,y),z) = times(x,times(y,z))
times(x,e()) = x
times(x,i(x)) = e()

COMPLETE TRS:
RULES:
times(times(x,y),z) -> times(x,times(y,z))
times(x,e()) -> x
times(x,i(x)) -> e()
times(e(),x) -> x
i(i(x)) -> x
times(i(x),x) -> e()
times(i(x),times(x,y)) -> y
times(y,times(i(y),x)) -> x
i(e()) -> e()
i(times(y,x)) -> times(i(x),i(y))

SUCCESS
Search time: 0.05 seconds

COMPLETE TRSとSUCCESSのメッセージが表示されれば成功です.

次に失敗例として環を完備化してみます.

$ vim ring.trs

(VAR x y z)
(RULES
  +(+(x, y), z) -> +(x, +(y, z))
  +(x, 0) -> x
  +(x, -(x)) -> 0

  *(*(x, y), z) -> *(x, *(y, z))
  *(x, 1) -> x
  *(x, /(x)) -> 1

  *(x, +(y, z)) -> +(*(x, y), *(x, z))

  *(x, 0) -> 0
)

$ maxcomp -s lpo ring.trs

EQUATIONS: 
plus(plus(x,y),z) = plus(x,plus(y,z))
plus(x,0()) = x
plus(x,minus(x)) = 0()
times(times(x,y),z) = times(x,times(y,z))
times(x,1()) = x
times(x,slash(x)) = 1()
times(x,plus(y,z)) = plus(times(x,y),times(x,z))
times(x,0()) = 0()

Fatal error: exception Maxcomp.Fail("I'm giving up")

"I'm giving up"と表示されれば完備化の失敗です.maxcomp + (lpo | rpo | kbo)では完備化できなかったことを意味します.