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)では完備化できなかったことを意味します.