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

最近の状況

23日は時間があったのでニュートン運動方程式によって天体が相互作用するプログラムを書きました.
f:id:P_Equa_NP:20161024233122g:plain

交錯する人生の意義です.
f:id:P_Equa_NP:20161024233811g:plain

こちらは今日出力した画像です.
理解が捗っているときの脳内の様子を表現しました.
f:id:P_Equa_NP:20161024234038g:plain
f:id:P_Equa_NP:20161024234224g:plain

画像はご自由に転載していただいて構いません.

古典論理の推論規則から3値論理の演算を補完する

はじめに2値論理

通常の論理学は論理演算fに真(True),偽(False)いずれかの引数を2つ取り,同様に真偽のいずれかの値を1つ返します.

{ \displaystyle Bool := \{ True, False \} }
{ \displaystyle f \colon Bool \times Bool \to Bool }

以下に2値論理におけるEqual, NotEqual, And, Or, Implication, Notを表としてまとめます.左から左辺,右辺,評価結果と並んでいます.

Equal : x = y
TT T
TF F
FT F
FF T
NotEqual : x /= y
TT F
TF T
FT T
FF F
And : x ∧ y
TT T
TF F
FT F
FF F
And : x ∨ y
TT T
TF T
FT T
FF F
Impl : x ⇒ y
TT T
TF F
FT T
FF T
Not : ¬x
T F
F T

見やすいようにひとつのテーブルにまとめます.

LHSRHS
TT T T T F
TF F T F  
FT F T T T
FF F F T  

含意(Implication)についてはAndとNotを使った表現方法があり,以下と同値です.

{ \displaystyle A \Rightarrow B \iff \lnot A \lor B }

また,古典論理に限ってド・モルガンの法則を使って次のように変形できます.

{ \displaystyle A \Rightarrow B \iff \lnot ( A \land B ) }

2値論理における推論規則

推論とは「AならばB」のことで,推論規則とはImplicationの形で与えられる論理式の真偽を判定するための規則です.{ A \models B }と書きます.ただしここでは論理演算Implicationとは区別し,演算子の優先順位を1つ下げます.

古典論理における推論規則には以下の11があります.また,詳細は後述しますが,3値論理を導入する際に古典論理との整合性を保つためにこの推論規則から3値目の論理値の振る舞いを制約としてある程度決定することができます.

前件肯定:
{ \displaystyle P, P \Rightarrow Q \models Q }

後件肯定:
{ \displaystyle \lnot Q, P \Rightarrow Q \models \lnot P }

否定導入:
{ \displaystyle P \Rightarrow F \models \lnot P }

二重否定の除去:
{ \displaystyle \lnot \lnot P \models P }

二重否定の導入:
{ \displaystyle P \models \lnot \lnot P }

選言三段論法:
{ \displaystyle P \lor Q. \lnot P \models Q }

仮言三段論法:
{ \displaystyle P \Rightarrow Q, Q \Rightarrow R \models P \Rightarrow R }

導出:
{ \displaystyle L \lor P, \lnot L \lor Q \models P \lor Q }

普遍例化:
{ \displaystyle \forall x. P(x) \models P(a) }

存在汎化:
{ \displaystyle P(a) \models \exists x. P(x) }

後件肯定:
{ \displaystyle Q, P \Rightarrow Q \models P }

推論規則から3値目の値の振る舞いを決定する

前置きが長くなってしまいました.このエントリで本当に述べたかったことはここの節からです.

3値目の値をUとするならば,当然,その値の推論規則による振る舞いが決定されていなければなりません.そしてその振る舞いは古典論理の拡張であるならば自由に決定できるものではなく,制約を満たした上で決定されます.

その制約を得てみましょう.アルゴリズムは各推論規則に対し自由変数にUを代入して変数を消去することによって進行します.以下の通りです.

1. 推論{ LHS \models RHS }において,左辺に出現する自由変数にUを代入したときにRHSをTrueにする式の形から論理演算を決定する.

2. 推論{ A, B \models RHS }において,AをTrueにする変数の組み合わせがBへの制約条件となり,B中に存在する自由変数にUを代入する.そのあとの方針は1と同じ.

前件肯定:
前件肯定:
  P, P -> Q |- Q

  より
    T, T -> U |- U
  よって
    T -> U = T

後件否定:
  ¬Q, P -> Q |- ¬P
より
  ¬F, U -> F |- ¬U
よって
  U -> F = T

否定導入:
  P -> F |- ¬P
より
  U -> F |- ¬U
よって
  U -> F = T

二重否定の除去:
  ¬¬P |- P
より
  ¬U = x1
  ¬x1 = x2
  x2 -> U = T
より
  ¬U = F
ならば
  ¬U = F = x1
  ¬F = T = x2
  T -> U = T
よって
  ¬U = F -- 3

二重否定の導入:
  P |- ¬¬P
よって
  ¬U = F
  U -> ¬¬U
  = U -> ¬F
  = U -> T = T

選言三段論法:
  P ∨ Q, ¬P |- Q
より
  F ∨ U, ¬F |- U
よって
  F ∨ U = T
  T -> U = T

仮言三段論法:
  P -> Q, Q -> R |- P -> R
より

    U -> Q, Q -> R |- U -> R
  より
    U -> T, T -> T |- U -> T
  よって
    U -> T = T

    P -> U, U -> R |- P -> R
  より
    P -> U, U -> T |- P -> T
  より

    T -> U, U -> T |- T -> T
    F -> U, U -> T |- F -> T
    U -> U, U -> T |- U -> T
  よって
    U -> U = T
    U -> T = T

  P -> Q, Q -> U |- P -> U
より

    T -> T, T -> U |- T -> U
    T -> U, U -> U |- T -> U
    F -> T, T -> U |- F -> U
    F -> F, F -> U |- F -> U
    F -> U, U -> U |- F -> U
    U -> T, T -> U |- U -> U
    U -> F, F -> U |- U -> U
    U -> U, U -> U |- U -> U
  よって
    F -> U = T

導出:
  L ∨ P, ¬L ∨ Q |- P ∨ Q
より

    T ∨ T, ¬T ∨ U |- T ∨ U
  よって
    F ∨ U = T
    T ∨ U = T

    F ∨ T, ¬F ∨ U |- T ∨ U
  よって
    T ∨ U = T

    T ∨ U, ¬T ∨ T |- U ∨ T
  よって
    U ∨ T = T

    F ∨ U, ¬F ∨ T |- U ∨ T
  よって
    F ∨ U = T

    F ∨ U, ¬F ∨ F |- U ∨ F
  よって
    U ∨ F = T

後件肯定:
  Q, P -> Q |- P
より
  T, U -> T |- U
よって
  U -> T = T
  T -> U = T

以上の手続きから3値目の値に対する論理演算の一部が得られました.

前件肯定より
{ \displaystyle True \Rightarrow U = True }

後件否定より
{ \displaystyle U \Rightarrow False = True }

二重否定の除去より
{ \displaystyle \lnot U = True }

二重否定の導入より
{ \displaystyle U \Rightarrow T = True }

選言三段論法より
{ \displaystyle F \lor U = True }

仮言三段論法より
{ \displaystyle F \Rightarrow U = True }

仮言三段論法より
{ \displaystyle U \Rightarrow U = True }

導出より
{ \displaystyle T \lor U = True }
{ \displaystyle F \lor U = True }
{ \displaystyle U \lor T = True }
{ \displaystyle U \lor F = True }

実際には,古典論理からの互換性が必須でないため,論理演算の妥当性を優先するならば推論規則をいくつか棄却して制約条件を得なければなりません.