講義資料 - Toyama

2015 年度 情報論理学 講義資料 (1)
青戸等人
はじ めに
1
次の 3 つの等式を 満たす演算を も つ集合のこ と を 群と いう ．


 +(0, x) ≈ x

+(−(x), x) ≈ 0


+(+(x, y), z) ≈ +(x, +(y, z))
こ こ で， x, y, z は変数で， +, −, 0 は集合上の演算である ． (本講義では， = の代わり
に ≈ を 対象言語の等号に 用いる ． ) 通常， +, −, 0 は実数や整数の加算， 符号反転，
零に 使われる こ と が多いが， 群論では， こ れら に 限定せず， 一般に 上の等式が満た
さ れる も のすべて を 対象に し て ， ど んな 性質が成立する かを 調べる ．
こ のよ う な 等式の公理から ど のよ う な 等式が導かれる か， を 考え る 枠組みが等式
論理 (equational logic) と よ ばれる も のである ． 例え ば， 群の公理のモデルは” 群” と
よ ばれ， 他に も 束の公理のモデルは” 束” と よ ばれる ． 一般に ， こ のよ う な 等式公理
のモデルは代数と よ ばれ， そ の数学理論がいろ いろ 詳し く 調べら れて おり ， 例え ば
群や束であれば， 群論や束論と し て 知ら れて いる ．
こ の講義では， 等式理論にも と づく 計算モデルである 項書き 換え システム につい
て ， いく つかのト ピ ッ ク ス を 取り 上げ講義する ． 等式のみを 対象に する と いう こ と
はと て も 限定的な 気がする かも し れな いが， 項表現に 変数束縛を 導入する な ど し て ，
ラ ム ダ計算な ど を 含むよ う な ， よ り 表現力を 高めた項書き 換え シス テム に ついて の
研究も 精力的に 進めら れて いる ． ま た， 述語論理の自動証明な ど に おけ る 等式特有
の取り 扱いに おいて も 書き 換え シス テム の技術が応用さ れて いる ．
ま た， 表面的な 内容だけ でな く ， 細かい証明も 触れて も ら う し ， SML#1 を 用い
たプロ グラ ム を 作成し な がら ， 理解を 深めて も ら う ． 本文中のプロ グラ ム は， http:
//www.nue.riec.tohoku.ac.jp/user/aoto/15LogicG/ に置く 2． SML 言語につい
て は， いろ いろ な 教科書があ る と 思う が， [2], [3] だけ 挙げて おく ． 項書き 換え シス
テム について は， (お話的な ) 解説は [4] にある が， き ち んと し た教科書は日本語では
な い． 英語では [1] はき ち んと し た 内容で比較的読みやすいが， 内容はだいぶ古く ，
理論的な 本を 読み慣れて いな い人に はだいぶ難し い．
関数記号と 変数
2
演算を 表わす記号を 関数記号 (function symbol ) と よ ぶ． 関数記号は， そ れぞれ， 引
数の個数が決ま っ て いる も のと する ． こ の数を ア リ ティ と いう ． 関数記号 f のア リ
SML#は東北大学電気通信研究所大堀研究室で開発さ れて いる SML 言語のコ ン パイ ラ
http://www.pllab.riec.tohoku.ac.jp/smlsharp/ja/
2
プロ グラ ム はこ れを 参考に せずに /使わずに 書いて も ， ま っ たく 構わな い．
1
1
ティ を arity(f ) と 記す． 特に ， ア リ ティ は 0 でも よ いも のと する ． ア リ ティ が 0 の
関数記号と は， つま り ， 定数 (constant) のこ と に な る ．
等式公理を 表わすために は， 関数記号の他に ， 変数 (variable) が必要と な る ． ま
た， 変数は (可算) 無限個ある も のと する ． 従っ て ， 必要に な る たびに ， ま だ使われ
て いな い変数を いつでも 用意でき る ．
ま た， 同じ 記号が関数記号かつ変数にな る こ と はな いも のと する ． つま り ， 関数
記号の集合を F ， 変数の集合を V と する と き ， F ∩ V = ∅ が成立する ． 以下では， 特
に断わら な い限り ， 変数全体の集合を V と 記し ， 関数記号全体の集合を F と 表わす．
変数や関数記号を プロ グラ ム で扱う ために ， こ れら のデータ 型を 定義し よ う ．
ま ず， 変数に関する データ 型や関数を おく Var スト ラ ク チャ を 用意する ． 変数は
x1 や y2 のよ う に ， 変数名と 自然数のイ ン デッ ク ス の対から 構成さ れる も のと する ．
自然数のイ ン デッ ク スは変数を 新し いも のにする と き に便利． Var.name は変数名の
部分を ， Var.index はイ ン デッ ク ス を 取り 出す．
1
2
3
4
5
6
7
(* var.sml *)
signature VAR =
sig
eqtype key
val name: key -> string
val index: key -> int
end
8
9
10
11
12
13
14
structure Var : VAR =
struct
type key = string * int
fun name (x,i) = x
fun index (x,i) = i
end
同様にし て ， 関数記号に関する データ 型や関数を おく Fun スト ラ ク チャ を 用意す
る ． 関数記号の場合は， 関数名そ のも のを 関数記号と し よ う ．
1
2
3
4
5
(* fun.sml *)
signature FUN =
sig
eqtype key
end
6
7
8
9
10
structure Fun : FUN =
struct
type key = string
end
さ て ， 変数や関数記号を プロ グラ ム 上で入力する には， 文字列から 入力する のが
便利であ る ． そ こ で， “変数 ⇄ 文字列”， “関数記号 ⇄ 文字列” と いう 変換を 行う
プロ グラ ム を 用意し て おく ．
変数は， _[1-9][0-9]* (つま り ， ア ン ダース コ ア “_” に 1∼ 9 から 始ま る 数字列
が続いたも の ) が末尾にある と き ， こ の部分を 自然数のイ ン デッ ク スと し て 扱う こ と
2
にする (ただし ， その前の変数名の部分が空文字列のと き は例外と する )． そのよ う な
末尾がな いと き のイ ン デッ ク スは 0 と 定める ． 関数記号では， 文字列がそのま ま 関数
記号と 対応する ． toString 関数は， 変数や関数記号を 文字列へ変換し ， fromString
関数は， 文字列を 変数や関数記号へ変換する ．
1
2
3
4
5
6
7
(* var.sml *)
signature VAR =
sig
...
val toString: key -> string
val fromString: string -> key
end
8
9
10
11
12
13
14
structure Var : VAR =
struct
...
fun toString (x,i) = if i = 0 then x
else if Int.> (i, 0) then x ^ "_" ^ (Int.
toString i)
else raise Fail "Error: Var.toString: var index
out of range"
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
1
2
3
4
5
6
7
(* .+_[1-9][0-9]* と な っ て いれば末尾を index と する *)
fun fromString str =
let val ss = Substring.full str
val (body,index) = Substring.splitr Char.isDigit ss
val isProperIndexing = Int.> (Substring.size body, 1)
andalso Substring.sub (body, Substring.
size body - 1) = #"_"
andalso not (Substring.isEmpty index)
andalso Substring.sub (index, 0) <> #"0"
in if isProperIndexing
then (Substring.string (Substring.trimr 1 body),
valOf (Int.fromString (Substring.string index)))
else (str,0)
end
end
(* fun.sml *)
signature FUN =
sig
...
val toString: key -> string
val fromString: string -> key
end
8
9
10
11
12
structure Fun : FUN =
struct
...
fun toString key = key
3
13
14
fun fromString str = str
end
最後に ， 以上のプロ グラ ム の実行例を いく つか示す． ソ ース フ ァ イ ルを イ ン タ
プリ タ で扱う た めに は use ディ レ ク ティ ブを 使う ． いま は 2 つし かフ ァ イ ルがな い
(var.sml， fun.sml) が， こ れから 増え て く る と 何度も フ ァ イ ルを ロ ード する のは大
変な ので， 必要な すべて のソ ース フ ァ イ ルを 1 度に 読み込むた めに ， 以下の内容の
フ ァ イ ル use.sml を 用意し て おく ．
1
2
3
(* use.sml *)
_use "var.sml"
_use "fun.sml"
SML#では， use ディ レ ク ティ ブはイ ン タ プリ タ のト ッ プ環境でし か使え な いの
で， フ ァ イ ルの中では代わり に _use を 使う 必要がある ．
以下は， Unix 環境でイ ン タ プリ タ を 動かし た様子．
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
(* 実行例 *)
$ ls
(* シェ ル環境 *)
fun.sml use.sml var.sml
$ smlsharp
SML# version 1.2.0 (2012-11-14 18:25:26 JST) for x86-linux
# use "use.sml";
signature FUN =
...
...
...
# Var.fromString "x_12";
val it = ("x", 12) : string * int
# Var.fromString "x_012";
val it = ("x_012", 0) : string * int
# Var.fromString "_12";
val it = ("_12", 0) : string * int
# Fun.fromString "+";
val it = "+" : string
#
(* Ctrl-D で終了*)
$
(* シェ ル環境に 戻っ た *)
演習 1 SML#コ ン パイ ラ を イ ン スト ールせよ ． イ ン タ プリ タ で， val.sml, fun.sml
を 読み込み， テス ト せよ ．
3
項 (term)
等号はある 対象と ある 対象の間に 成立する 関係である ． こ の対象を 表わす記号列を
項と いう ． 群の公理に おけ る 等号の左辺や右辺は項である ．
定義 2 (項) 項 (term) を 以下のよ う に 帰納的に 定義する ．
(1) 変数は項である ．
(2) f を ア リ ティ n の関数記号， t1 , . . . , tn を 項と する と き ， f (t1 , . . . , tn ) は項である ．
4
特に ， (2) で， n = 0 のと き は f と 書く ．
定義から 明ら かな よ う に ， 項は変数全体の集合 V と 関数記号全体の集合 F から
定ま る ． つま り ， V と F は項集合のパラ メ ータ に な っ て いる から ， 項全体の集合を
T(F, V) と 記すこ と に する ．
例 3 (項の例) F = {+, −, 0} と する と ， −(0) や +(0, x0 )， −(+(0, x0 )) は， 項の例
である ．
項に 関する データ 型や関数を おく Term ス ト ラ ク チャ を 用意し よ う ．
1
2
3
4
5
6
7
(* term.sml *)
signature TERM =
sig
type var_key = Var.key
type fun_key = Fun.key
datatype term = Var of var_key | Fun of fun_key * term list
end
8
9
10
11
12
13
structure Term : TERM =
struct
type var_key = Var.key
type fun_key = Fun.key
datatype term = Var of var_key | Fun of fun_key * term list
項を 表わすデータ 型 term と し て は， 関数記号の下に ， 項のリ ス ト を 持て る よ う
にする ． プロ グラ ム 内では制約を 受け な いが， こ の項のリ スト の長さ は， (暗黙的に )
関数記号のア リ ティ と 対応する こ と と 約束する ．
演習 4 Term スト ラ ク チャ に， 与え ら れた項が変数かを 返す isVar:
およ び変数でな いかを 返す isFun: term -> bool を 追加せよ ．
term -> bool
演習 5 Term ス ト ラ ク チャ に ， args x = [ ]， args f (t1 , . . . , tn ) = [t1 , . . . , tn ] と な る
よ う な ， 与え ら れた項の引数を 返す関数 args: term -> term list を 追加せよ ．
定義 6 (根記号) 項 t の根記号 root(t) を 以下のよ う に 定める ．
x (t = x ∈ V の場合)
root(t) =
f (t = f (t1 , . . . , tn ) の場合)
例 7 root(+(x, +(y, 0))) = +．
項 t から root(t) を 計算する 関数を 書こ う ． root 関数を 用意する ために は， 変数
と 関数記号を 一緒に 扱う 必要があ る ． そ こ で， F ∪ V を 表わすた めのデータ 型と し
て ， Symbol ス ト ラ ク チャ を 用意し ， symbol 型を 定義し て おく ．
5
1
2
3
4
5
(* symbol.sml *)
signature SYMBOL =
sig
datatype symbol = V of Var.key | F of Fun.key
end
6
7
8
9
10
structure Symbol : SYMBOL =
struct
datatype symbol = V of Var.key | F of Fun.key
end
演習 8 Term ス ト ラ ク チャ に ， 与え ら れた 項の根記号を 返す関数 root:
Symbol.symbol を 追加せよ ．
term ->
定義 9 (項の変数集合) t を 項と する と き ， V(t) を 以下のよ う に 定義する ．
{x}
(t = x ∈ V の場合)
V(t) = S
1≤i≤n V(ti ) (t = f (t1 , . . . , tn ) の場合)
例 10 V(+(x, +(y, 0))) = {x, y}．
V(t) を 計算する 関数を 書こ う ． こ のために ， ま ず， ListUtil ス ト ラ ク チャ を 用
意し ， その中に， 集合演算を リ スト を 使っ て 実現する 関数を 用意する ． member x xs
は要素 x がリ ス ト xs に 含ま れて いる かを 判定する ． add x xs は要素 x が xs に 含ま
れて いな いと き だけ リ ス ト に x を 追加する ． つま り ， xs に 要素が 2 重に 含ま れて い
な いな ら ， 追加し た 後も 要素は 2 重に 含ま れな い． union xs ys は， 2 つのリ ス ト
xs と ys を ， 同じ 要素が重複さ れな いよ う に 結合する ．
1
2
3
4
5
6
7
(* list_util.sml *)
signature LIST_UTIL =
sig
val member: ’’a -> ’’a list -> bool
val add: ’’a -> ’’a list -> ’’a list
val union: ’’a list * ’’a list -> ’’a list
end
8
9
10
11
12
structure ListUtil : LIST_UTIL =
struct
fun member x [] = false
| member x (y::ys) = x = y orelse member x ys
13
14
15
(* 集合と し て の演算 *)
fun add x ys = if member x ys then ys else x::ys
16
17
...
18
19
end
6
演習 11 ListUtil ス ト ラ ク チャ に ， 関数 union を 補え ．
演習 12 Term ス ト ラ ク チャ に ， t から V(t) を 返す関数 vars:
list を 追加せよ ．
term -> var key
最後に ， 変数や関数記号に ついて 行っ たよ う に ， “項 ⇄ 文字列” の変換関数を 用
意する ．
ま ず， 変数と 関数記号を 区別する 必要がある が， 文字列のう ち ， 先頭に ?がつい
て いる も のを 変数と し ， そ う でな いも のは関数記号と する ．
1
2
3
4
5
6
7
(* symbol.sml *)
signature SYMBOL =
sig
...
val toString : symbol -> string
val fromString : string -> symbol
end
8
9
10
11
12
13
structure Symbol : SYMBOL =
struct
...
fun toString (V x) = "?" ^ (Var.toString x)
| toString (F f) = (Fun.toString f)
14
15
16
17
18
19
fun fromString str =
if String.isPrefix "?" str
then V (Var.fromString (String.substring (str, 1, (String.size
str) - 1)))
else F (Fun.fromString str)
end
文字列から 項を 得る に は， 字句解析・ 構文解析が必要に な る ． 字句解析では， 3
つ特殊文字 “(”,“)”， “,” を 切り 出すと と も に ， こ れら の特殊文字と 空白を 区切り と
し て 得ら れる 文字列の列に 分解する ． 構文解析は， 以下の項の構文に あっ て いる か
を チェッ ク する ． fsym， vsym は， そ れぞれ関数記号と な る 文字列， 変数と な る 文字
列を 表わす． プロ グラ ム の詳細は省略する ． lexical.sml に は字句解析のツ ール，
parsing.sml に は構文解析のツ ールが入っ て いる ．
1
2
3
4
1
2
3
4
5
6
term ::= fsym "(" termlist | atom
termlist ::= termseq ")"
termseq ::= term "," termseq | term
atom ::= fsym | vsym
signature TERM =
sig
...
val toString: term -> string
val fromString: string -> term
end
7
最後に ， 実行例を 示す．
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
4
$ ls
fun.sml lexical.sml list_util.sml parsing.sml symbol.sml
sml use.sml var.sml
$ smlsharp
SML# version 1.2.0 (2012-11-14 18:25:26 JST) for x86-linux
# use "use.sml";
functor Lexical
...
...
# val t0 = Term.fromString "?x";
val t0 = _ : Term.term
# val t1 = Term.fromString "+(s(?x),?x)";
val t1 = _ : Term.term
# Term.toString t0;
val it = "?x" : string
# Term.toString t1;
val it = "+(s(?x),?x)" : string
# Term.isFun t0;
val it = false : bool
# Term.isFun t1;
val it = true : bool
# Symbol.toString (Term.root t0);
val it = "?x" : string
# Symbol.toString (Term.root t1);
val it = "+" : string
# List.map Term.toString (Term.args t1);
val it = ["s(?x)", "?x"] : string list
# List.map Var.toString (Term.vars t1);
val it = ["x"] : string list
#
(* Ctrl-D で終了 *)
$
(* シェ ル環境に も ど っ た *)
term.
代入 (substitution)
変数は項で具体化さ れる ． こ れを 行う のが代入．
定義 13 関数 σ : V → T(F, V) で， 集合 {x | σ(x) 6= x} が有限であ る も のを 代
入 (substitution) と よ ぶ． 集合 {x | σ(x) 6= x} を 代入 σ の定義域 (domain) と よ び，
dom(σ) と 記す．
dom(σ) = {x1 , . . . , xn } であ る と き ， 特に ， σ を {x1 := σ(x1 ), . . . , xn := σ(xn )}
のよ う に も 書く ．
例 14 σ = {x := 0, y := +(x, z)} は代入． こ のと き ， σ(x) = 0， σ(y) = +(x, z) と
な る ． ま た， w ∈
/ {x, y} である 任意の変数 w に ついて は， σ(w) = w と な る ．
8
定義 15 代入 σ の準同型拡張と は， 以下のよ う に 定義さ れる 関数 σ̂ : T(F, V) →
T(F, V) を いう ．
σ(t)
t ∈ V のと き
σ̂(t) =
f (σ̂(t1 ), . . . , σ̂(tn )) t = f (t1 , . . . , tn ) のと き
代入 σ と そ の準同型拡張 σ̂ を 同一視し て ， σ̂ と 書く べき と き も σ を 用いる ．
例 16 σ = {y := +(x, z)} と する と ， σ(+(+(0, x), y)) = +(+(0, x), +(x, z)) と な り ，
σ(+(y, y)) = +(+(x, z), +(x, z)) と な る ．
こ のために 代入を 扱う ために ， 連想リ ス ト (association list) に 関する プロ グラ ム
を 用意する ．
連想リ スト は， (key, value) な る 対を 要素にも つよ う な リ スト で， 鍵 (key) から 値
(value) への対応を 保持し て おく ためのデータ 構造である ． 単な る 対のリ ス ト と 異な
り ， 1 つの鍵に 対応する 値は 1 つし か保持し な いと いう 制限がある ． つま り ，
条件： リ ス ト 中の任意の 2 つの異な る 要素 (x, n) と (y, m) に ついて ， x 6= y と な る
が成立する よ う に メ ン テナン ス を する ． な お， こ の条件は，
条件： リ ス ト 中の任意の要素 (x, n) と (y, m) に ついて ， x = y な ら ば n = m．
と も 書け る ．
ま ず， AssocList スト ラ ク チャ を 用意し ， その中に， 連想リ スト を 対のリ スト を
使っ て 実現する 関数を 用意する ． find k xs は k を 鍵と する 要素が連想リ スト xs に
含ま れて いる かを 判定し ， (k,v) が要素と な っ て いれば SOME v を ， k を 鍵と する 要
素がな け れば NONE を 返す．
add (k,v) xs は， 連想リ ス ト に (k,v) を 追加する ． も し (k,v) がすでに 要素と
な っ て いれば重複を 避け る た めに 実際に は追加し な いので， SOME xs を 返す． も し
(k,w) で， w が v と は異な る よ う な 要素が xs に 入っ て いた と き に は， (k,v) を 付け
加え る こ と は出来な い． こ のと き は NONE を 返す． 最後に ， k を 鍵と する よ う な 要素
が xs に含ま れて いな いと き には， (k,v) を リ スト に追加し て SOME ((k,v)::xs) を
返す．
1
2
3
4
5
6
(* assoc_list.sml *)
signature ASSOC_LIST =
sig
val find: ’’a -> (’’a * ’b) list -> ’b option
val add: (’’a * ’’b) -> (’’a * ’’b) list -> (’’a * ’’b) list
option
end
7
8
9
10
11
12
13
14
15
16
structure AssocList : ASSOC_LIST=
struct
fun find x [] = NONE
| find x ((k,v)::ys) = if x = k then SOME v else find x ys
fun add (k,v) ys = case find k ys of
SOME w => if v = w then SOME ys
else NONE
| NONE => SOME ((k,v)::ys)
end
9
最後に， 代入に関する 関数を 置く Subst スト ラ ク チャ を 用意する ． こ こ では， find
関数し か使っ て いな いが， add 関数は後に 用いる ． apply 関数は， 代入を 項に 適用
する 関数である ．
1
2
3
4
5
6
(* subst.sml *)
signature SUBST =
sig
type subst
val apply: subst -> Term.term -> Term.term
end
7
8
9
10
11
12
13
14
15
16
17
18
19
20
structure Subst: SUBST =
struct
local
structure AL = AssocList
structure L = List
structure T = Term
in
type subst = (Var.key * Term.term) list
fun apply sigma (T.Var x) = (case AL.find x sigma of
SOME t => t | NONE => T.Var x)
| apply sigma (T.Fun (f,ts)) = T.Fun (f, L.map (apply sigma) ts)
end (* of local *)
end
以下は代入の実行例．
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
$ ls
assoc_list.sml lexical.sml
parsing.sml symbol.sml use.sml
fun.sml
list_util.sml subst.sml
term.sml
var.sml
$ smlsharp
SML# version 1.2.0 (2012-11-14 18:25:26 JST) for x86-linux
# use "use.sml";
...
...
# val sigma = [(Var.fromString "x", Term.fromString "0"), (Var.
fromString "y", Term.fromString "+(?x,?y)")];
val sigma = [(("x", 0), _), (("y", 0), _)] : ((string * int) * Term.
term) list
# Subst.apply sigma (Term.fromString "+(s(?x),?y)");
val it = _ : Term.term
# Term.toString it;
val it = "+(s(0),+(?x,?y))" : string
#
(* Ctrl-D で終了*)
$
(* シェ ル環境に 戻っ た *)
10
References
[1] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University
Press, 1998.
[2] 大堀 淳. プロ グラ ミ ン グ言語 Standard ML 入門. 共立出版株式会社, 2001.
[3] L. C. Paulson. ML for the Working Programmer, 2nd ed. Cambridge University
Press, 1996.
[4] 外山 芳人. 項書き 換えシステム入門 -完備化によ る 定理自動証明-. http://www.
nue.riec.tohoku.ac.jp/lab-intro/TRS-intro/
11