1 述語論理とその意味論

推論計算モデル特論 2002 南出靖彦
述語論理とその意味論
1
1.1
述語論理 (predicate logic)
定義 1.1 (項 (term))
• 定数 c
• 変数 x
• f(t1 , . . . , tn ) (f が n 引数の関数記号)
定義 1.2 (論理式 (formula))
• p(t1 , . . . , tn ) (p が n 引数の述語記号) (原始論理式 (atomic formula))
• ¬P 否定 (negation)
• P ∨ Q 論理和, 選言 (disjunction), P ∧ Q 論理積, 連言 (conjunction)
• ∀x.P , ∃x.P
定義 1.3 (解釈 (interpretation)) M = (D, I)
• D: 空でない集合
• I(a) ∈ D
• I(f) ∈ D × . . . × D → D (f は, n 引数の関数記号)
• I(p) ∈ D × . . . × D → {T, F } (p は, n 引数の述語記号)
例 1.1 定数記号 zero, 関数記号 succ, 述語記号 even.
M = (N , I)
I(zero) =
I(succ)(x) =
I(even)(x) =
0
x+1
T x mod 2 = 0
F x mod 2 = 1
定義 1.4 付値 σ を変数の集合から D への関数とする.
• 項の解釈 M [[t]]: (V ar → D) → D
– M [[x]]σ = σ(x)
– M [[c]]σ = I(c)
– M [[f(t1 , . . . , tn )]]σ = I(f)(M [[t1 ]]σ, . . . , M [[tn]]σ)
• 論理式の解釈 M [[P ]]: (V ar → D) → {T, F }
– M [[p(t1 , . . . , tn )]]σ = I(p)(M [[t1 ]]σ, . . . , M [[tn]]σ)
1
– M [[P ∨ Q]]σ = M [[P ]]σ ∨ M [[Q]]σ
– M [[∀x.P ]]σ = ∀v ∈ D.M [[P ]]σ[v/x]
σ[v/x](y) =
v
σ(y)
(y ≡ x とき)
それ以外のとき
例 1.2 上の M = (N , I) を考える. また, 関数 σ が以下のように定義されているとする.
σ(x) = 1
σ(y) = 2
σ(v) = 0
それ以外の変数 v
以下の解釈を計算せよ.
M [[even(succ(x)) ∧ ¬even(succ(y)]]σ
M [[∀x.(¬even(x) ∨ even(succ(succ(x))))]]σ
補題 1.1 P を閉じた論理式ならば, P の解釈 M [[P ]]σ は, σ に依存しない.
定義 1.5 P, Q1, . . . , Qn を閉じた論理式とする.
• 論理式 P が充足可能 (satisﬁable) ⇔ ある解釈 M が存在して, P の解釈が T となる.
• 論理式 P が充足不能 (unsatisﬁable) ⇔ P の解釈が T となる解釈 M が存在しない.
• 論理式 P が論理式 Q1 , . . . , Qn の論理的帰結 ⇔ 任意の解釈 M に対して, Qi (1 ≤ i ≤ n) の
解釈が T ならば P の解釈が T .
Q1 , . . . , Qn |= P
例 1.3 Q1 , Q2 , P を以下の論理式とする.
Q1
Q2
P
= even(zero)
= ∀x.¬even(x) ∨ even(succ(succ(x)))
= even(succ(succ(zero)))
このとき
Q1 , Q2 |= P
1.2
標準形
定義 1.6
• リテラル (literal): 原始論理式または原始論理式の否定
• リテラルの 0 個以上の論理和を節 (clause) という.
– リテラルの 0 個の論理和を空節といい, と書く.
定義 1.7 論理式 P1 ∧ P2 ∧ . . . ∧ Pn を連言標準形 (conjunctive normal form) という.
• Pi は, リテラルの論理和.
補題 1.2
• ¬¬P ⇔ P .
2
• ¬(P ∨ Q) ⇔ ¬P ∧ ¬Q, ¬(P ∧ Q) ⇔ ¬P ∨ ¬Q. (De Morgan’s law)
• P ∨ (Q ∧ R) ⇔ (P ∨ Q) ∧ (P ∨ R), P ∧ (Q ∨ R) ⇔ (P ∧ Q) ∨ (P ∧ R).
例 1.4 (P ∨ ¬Q) ⇒ R
(P ∨ ¬Q) ⇒ R
⇐⇒
¬(P ∨ ¬Q) ∨ R
(1)
⇐⇒
(¬P ∧ Q) ∨ R
(2)
⇐⇒
(¬P ∨ R) ∧ (Q ∨ R)
(3)
定義 1.8 論理式 Q1 x1 Q2 x2 . . . Qn xn P を冠頭標準形 (prenex normal form) という.
• Qi は, ∀ または ∃.
• P は, ∀, ∃ を含まない.
補題 1.3 P を x を自由変数として含まない論理式とする.
• (P ∨ ∀x.Q) ⇔ ∀x.(P ∨ Q), (P ∧ ∀x.Q) ⇔ ∀x.(P ∧ Q).
• (P ∨ ∃x.Q) ⇔ ∃x.(P ∨ Q), (P ∧ ∃x.Q) ⇔ ∃x.(P ∧ Q).
• ∀x.¬Q ⇔ ¬∃x.Q
• ∃x.¬Q ⇔ ¬∀x.Q
定義 1.9 (スコーレム連言標準形)
∀x1 , . . . , xn.(C1 ∧ C2 ∧ . . . ∧ Cn )
C i は, 節.
例 1.5 ∃x.∀y.∀z.∃u.∀v.∃w.P (x, y, z, u, v, w) のスコーレム連言標準形.
∀y.∀z.∀v.P (c, y, z, f(y, z), v, g(y, z, v))
c は新しい定数記号, f, g は新しい関数記号.
例 1.6 以下の論理式のスコーレム連言標準形
• ∀x.∃y.(P (x, y) ∧ Q(x, y)) ∨ ∃x.R(x).
• ∀x.¬(∀y.P (x, y) ∨ ∃z.∀u.Q(x, z, u)).
定理 1.1 論理式 S を, 論理式 P のスコーレム連言標準形とする. P が充足不能であることと, S
が充足不能であることは同値である.
注意 1.1 P S
p(c) ⇒ ∃x.p(x)
∃x.p(x) ⇒ p(c)
定義 1.10 (代入, 例 (instance), 基礎例 (ground instance))
3
• [t1 /x1 , t2 /x2 , . . . , tn /xn ]
f(x, z)[a/x, f(b)/y, g(c)/z] ≡ f(a, g(c))
• 項 tθ を項 t の例という. (θ は代入)
• 論理式 P θ を論理式 P の例という. (θ は代入)
• 自由変数を含まない例を基礎例という.
定理 1.2 (エルブランの定理) S を節の有限集合とする. このとき, 以下の二つの性質は同値.
• S が充足不能.
• S に属する節の基礎例の有限集合が充足不能.
例 1.7 以下の節集合が充足不能であることを示す.
• {P (x), ¬P (f(a))}
• {¬P (x) ∨ Q(f(x), x), P (g(b)), ¬Q(y, z)}
定義 1.11 (エルブラン領域) H =
H0
Hi+1
=
=
∞
i=0
Hi
{c | c は定数記号 }
Hi ∪ {f(t1 , . . . , tn ) | tj ∈ Hi かつ f は n 変数の関数記号 }
定義 1.12 (エルブラン解釈) 以下の条件を満たす解釈 MH = (H, I) をエルブラン解釈という.
• I(c) = c
• I(f)(t1 , . . . , tn ) = f(t1 , . . . , tn )
アルゴリズム 1.1 (エルブランの定理の実装 (Gilmore 1960)) 節の集合 S が, 充足不能か調べ
る.
• Si : S の変数に Hi に属する項を代入した基礎例の集合
S0 , S1 , S2 , . . .
• Si が充足不能か調べる.
例 1.8 Gilmore のアルゴリズムで以下の節の集合が充足不能であることを示せ.
• {P (a), ¬P (x) ∨ Q(f(x)), ¬Q(f(a))}
• {P (x), Q(x, f(x)) ∨ ¬P (x), ¬Q(g(y), f(z))}
4
導出原理と Prolog
2
2.1
命題論理の導出原理
定義 2.1 L を命題変数, C1 , C2 を節とする. L ∈ C1 , ¬L ∈ C2 とする. この時, 節 (C1 \ {L}) ∪
(C2 \ {¬L}) を C1 と C2 の導出節 (resolvent) という.
例 2.1 P ∨ R と ¬P ∨ Q の導出節
R∨Q
例 2.2 ¬P ∨ Q ∨ R と ¬Q ∨ S の導出節.
定理 2.1 C を C1 と C2 の導出節とする. このとき, 以下が成り立つ.
C1 , C2 |= C
定義 2.2 S を節の集合, C, C1, . . . , Cn を節とする. 節の列 C1 , C2, . . . , Cn が以下の条件を満たす
とき, S からの C の導出という.
• Ci ∈ S, または Ci は, i 番目より前の節からの導出節
• Cn ≡ C
S からのの導出を, S の反駁 (refutation) という.
例 2.3 S = {¬P ∨ Q, ¬Q, P } とする. 以下の列は, S の反駁.
¬P ∨ Q, ¬Q, P, ¬P, 例 2.4 S = {P ∨ Q, ¬P ∨ Q, P ∨ ¬Q, ¬P ∨ ¬Q} の反駁を示せ.
2.2
単一化
定義 2.3
• 代入の合成 σ · θ は, t(σ · θ) = (tσ)θ で定義される.
– σ = [t1 /x1 , . . . , tn /xn ], θ = [s1 /y1 , . . . , sl /yl , u1 /z1 , . . . , um /zm ] とする. ただし, yi ∈
{x1 , . . . , xn } かつ zi ∈ {x1 , . . . , xn }. このとき,
σ · θ = [t1 θ/x1 , . . . , tn θ/xn , u1 /z1 , . . . , um/zm ]
• ある代入 σ が存在して, θ1 = θ2 · σ の時, θ2 は, θ1 より一般的 (more general) であるという.
例 2.5 代入 θ, λ を以下の代入とするとき, θ · λ を計算せよ.
θ
λ
=
=
[f(y)/x, z/y]
[a/x, b/y, y/z]
定義 2.4 E を項の対の集合とする.
• 任意の (s, t) ∈ E に対して, sθ ≡ tθ が成り立つ時, 代入 θ を E の単一化 (uniﬁer) という. E
の単一化が存在するとき, 単一化可能という.
5
• E の任意の単一化代入より一般的な E の単一化を mgu (most general uniﬁer) という.
記法 2.1 単一化を考えるとき, 項の対 (s, t) を s =? t と書くことにする.
例 2.6 E = {p(x, y) =? p(z, f(b))}.
• θ = [z/x, f(b)/y], λ = [a/x, f(b)/y, a/z] は, 共に E の単一化.
• θ は λ より一般的.
• mgu は θ.
アルゴリズム 2.1 (単一化 (unification) アルゴリズム) E を項の対の集合, θ を代入とする. こ
のとき, 以下の規則で E の mgu を求めることができる.
(E ∪ {t =? t}, θ)
⇒ (E, θ)
(E ∪ {x =? t}, θ)
⇒ (E[t/x], θ · [t/x])
(E ∪ {f(t1 , . . . , tn ) =? f(s1 , . . . , sn )}, θ)
(x ∈ F V (t))
⇒ (E ∪ {t1 =? s1 , . . . , tn =? sn }, θ)
定理 2.2 項の対の集合 E に対して, 以下は同値.
• E が単一化可能.
• ある θ に対して, (E, ∅) ⇒∗ (∅, θ).
(∅ は, どの変数も置き換えない代入. よって, t∅ ≡ t, ∅ · θ ≡ θ.)
このとき, 上の θ は, E の mgu である.
注意 2.1 以下は同値になる.
• 項の対の集合 E が単一化可能でない.
• (E, ∅) ⇒∗ (E , θ) となり, (E , θ) にはどの規則も適用でない. (E = ∅)
例 2.7 単一化アルゴリズムで, 以下の集合が単一化を持つか調べよ.
• {P (a, x, f(g(y))) =? P (z, f(z), f(u))}
• {f(x, x, g(x)) =? f(h(y), h(g(z)), g(h(u)))}
• {p(a, f(a)) =? p(x, x)}
• {f(g(x), y) =? f(y, x)}
2.3
一般単一化
定義 2.5
• L1 ∈ C1 , ¬L2 ∈ C2 とする. L1 と L2 が mgu σ を持つとする.
この時, 節 (C1 σ \ {L1 σ}) ∪ (C2 σ \ {¬L2 σ}) を C1 と C2 の 2 項導出節 (resolvent) という.
• 節 C の 2 個以上のリテラルが mgu σ を持つとき, Cσ を C の因子という.
6
• C1 と C2 の導出節
– C1 と C2 の 2 項導出節
– C1 の因子と C2 の 2 項導出節
– C1 と C2 の因子の 2 項導出節
– C1 の因子と C2 の因子の 2 項導出節
例 2.8 は, p(x) ∨ p(y) と ¬p(u) ∨ ¬p(v) の導出節.
• p(x) は, p(x) ∨ p(y) の因子
• ¬p(u) は, ¬p(u) ∨ ¬p(v) の因子
例 2.9 {¬p(x) ∨ q(y) ∨ r(x, f(x)), s(a), p(a), ¬r(r, x), ¬s(x) ∨ ¬q(x)} の反駁を示せ.
定理 2.3 S を節の集合とするとき, 以下は同値.
• S は, 充足不能.
• S の反駁が存在する.
アルゴリズム 2.2 P が P1 , . . . , Pn の論理的帰結か調べる.
• C1 , . . . , Cn を P1 , . . . , Pn のスコーレム連言標準形とする.
• C を ¬P のスコーレム連言標準形とする.
• C, C1, . . . , Cn の反駁が存在 ⇒ P は, P1 , . . . , Pn の論理的帰結.
– C, C1, . . . , Cn が充足不能.
– ¬P, P1 , . . . , Pn が充足不能.
– P1 , . . . , Pn の解釈が T ならば ¬P の解釈は F .
– P1 , . . . , Pn の解釈が T ならば P の解釈は T .
2.4
SLD 導出
定義 2.6 A, B1 , . . . , Bn を原始論理式とする.
• 下の形の節を確定節 (deﬁnite clause) と呼ぶ.
A ∨ ¬B1 ∨ . . . ∨ ¬Bn
確定節を以下のように書く.
A ← B1 , . . . , Bn
• 以下の形の節をゴール節という.
¬B1 ∨ . . . ∨ ¬Bn
ゴール節を以下のように書く.
← B1 , . . . Bn
定義 2.7
7
(n ≥ 0)
• 確定節 A ← B1 , . . . , Bm とゴール節 ← C1 , . . . , Cn の導出節.
← B1 θ, . . . , Bm θ, C2 θ, . . . , Cnθ
ただし, θ は A と C1 の mgu.
• 確定節の集合 P とゴール節 G からの Gn の SLD 導出
G1 , . . . , Gn
– Gi+1 は, P に含まれる確定節と Gi と導出節
– G1 ≡ G
定理 2.4 P を確定節の集合, Bi を原始論理式とする.
P |= ∃B1 ∧ . . . ∧ Bn ならば, P と ← B1 , . . . , Bn に対して SLD 反駁が存在する.
例 2.10 以下の確定節, ゴール節に対する SLD 反駁を示せ.
even(0)
even(succ(succ(x))) ← even(x)
← even(succ(y))
例 2.11 以下の確定節, ゴール節に対する SLD 反駁をすべて示せ.
add(x, 0, x)
add(x, succ(y), succ(z)) ← add(x, y, z)
← add(u, v, succ(succ(0)))
2.5
Prolog
• SLD 導出に基づくプログラミング言語.
• 深さ優先探索で SLD 反駁を探す.
– 確定節は, プログラムに現れる順番で順序付けられている.
例 2.12
• ファイル test.pl
even(0).
even(s(s(X))) :- even(X).
myappend([],Ys,Ys).
myappend([X|Xs],Ys,[X|Zs]):- myappend(Xs,Ys,Zs).
• ファイル test.pl を読み込む.
1 ?- [test].
Yes
2 ?- even(0).
Yes
8
3 ?- even(X).
X = 0 ;
X = s(s(0)) ;
X = s(s(s(s(0))))
Yes
4 ?- myappend(X,[3,4],[1,2,3]).
No
5 ?- myappend(X,[3,4],[1,2,3,4]).
X = [1, 2]
Yes
例 2.13 (停止性)
• ゴール節 myappend(X,[3,4],X) に対する導出は止まらない.
• 下のプログラムを考える.
even(s(s(X))) :- even(X).
even(0).
ゴール節 even(X) に対する導出は止まらない.
• 下のプログラムを考える.
myreverse([X|Xs],Zs) :- myreverse(Xs,Ys), append(Ys,[X],Zs).
myreverse([],[]).
myreversex([X|Xs],Zs) :- append(Ys,[X],Zs), myreversex(Xs,Ys).
myreversex([],[]).
– ゴール節 myreverse(X,[1,2]) に対する導出は止まらない.
– ゴール節 myreversex(X,[1,2]) に対する導出は止まる.
ラムダ計算と高階単一化
3
3.1
ラムダ計算
例 3.1 (ラムダ式) • 数学で関数を導入する時には, 以下のような定義で名前の付いた関数 f を導入する.
f x= x+1
• 同じ関数を付けずに表すために, λ 式の記法が用いられる.
λx.x + 1
• 関数適用
(λx.x + 1)2 = 2 + 1 = 3
9
定義 3.1 (ラムダ計算の構文)
• 変数は, ラムダ式.
• x が変数, t がラムダ式ならば, λx.t はラムダ式.
• t1 と t2 がラムダ式ならば, t1 t2 はラムダ式.
t ::= x | λx.t | tt
• 略記
t1 t2 t3 . . . tn ≡ (. . . ((t1 t2 )t3 ) . . . tn )
λx.t1 t2 ≡ λx.(t1 t2 )
定義 3.2 (自由変数 (free variable))
F V (x) =
F V (t1 t2 ) =
{x}
F V (t1 ) ∪ F V (t2 )
F V (λx.t) =
F V (t) \ {x}
定義 3.3 (アルファ同値) 束縛変数の名前の付け替えで, 同じ式と考えられる式をアルファ同値で
あるという.
λx.t =α λy.(t[y/x])
y ∈ F V (t)
• 以下, アルファ同値な式を同一視する.
例 3.2
λx.λy.xyz =α λy.λx.yxz
λx.λy.xyz =α λy.λz.yzz
定義 3.4 (代入 (substitution))
x[s/x] ≡ s
y[s/x] ≡ y
(x ≡ y)
(t1 t2 )[s/x] ≡ t1 [s/x]t2 [s/x]
(λx.t)[s/x] ≡ λx.t
(λy.t)[s/x] ≡ λy.(t[s/x])
(x ≡ y, y ∈ F V (s))
定義 3.5 (簡約 (reduction))
• β 簡約
(λx.t)s → t[s/x]
• η 簡約
λx.tx → t
ただし, x ∈ F V (t).
• t →∗β t : β 簡約を 0 回以上適用することで, t から t が得られる.
t →∗βη t : β 簡約, η 簡約を 0 回以上適用することで, t から t が得られる.
• t →β t となる式 t が存在しないとき, ラムダ式 t が β 正規形であるという. βη 正規形も
同様.
10
例 3.3
(λx.xx)(λx.xx) →β (λx.xx)(λx.xx) →β . . .
zλx.yx →η zy
例 3.4 (チャーチ数 (Church numeral)) 自然数 m を以下のラムダ式で表す.
m
= λx.λf.f(. . . (fx))
• 加算
add = λn.λm.λx.λf.(n(mxf)f)
• 乗算
mul = λn.λm.λx.λf.(nx(λz.mzf))
例 3.5 add 1 2 を簡約せよ.
定理 3.1 (Church-Rosser) t →∗ t1 かつ t →∗ t2 ならば, あるラムダ式 s が存在して, t1 →∗ s
かつ t2 →∗ s.
3.2
型付ラムダ計算
定義 3.6 (型付ラムダ計算の構文)
型
式
τ
t
::= b | τ → τ
::= c | x | λx.t | tt
ここで, c は定数記号.
定義 3.7 (型体系) Γ を以下の形式の変数と型の対応とする.
Γ ::= x1 : τ1 , . . . , xn : τn
• Γ t : τ は, 式 t が型 τ を持つことを意味する.
c ∈ Cτ
Γc:τ
x:τ ∈Γ
Γx:τ
Γ, x : τ1 t : τ2
Γ λx.t : τ1 → τ2
Γ t1 : τ1 → τ2 Γ t2 : τ1
Γ t1 t2 : τ2
例 3.6 ラムダ式 λx.λy.xy は, 型 (b → b) → b → b を持つ.
x : b → b, y : b x : b → b x : b → b, y : b y : b
x : b → b, y : b xy : b
x : b → b λy.xy : b → b
λx.λy.xy : (b → b) → b → b
例 3.7 m : b → (b → b) → b.
11
定義 3.8 (型体系 2) 各変数の型が決まっている場合.
c ∈ Cτ
c:τ
x ∈ Varτ
x:τ
x ∈ Varτ1 t : τ2
λx.t : τ1 → τ2
t1 : τ1 → τ2 t2 : τ1
t1 t2 : τ2
例 3.8 x ∈ V arb→b , y ∈ V arb とする.
x:b→b y:b
xy : b
λy.xy : b → b
λx.λy.xy : (b → b) → b → b
補題 3.1 ラムダ式が β 正規形でならば, 以下の形をしている.
• λx1 . . . xm .v t1 . . . tn .
• v は, 変数か定数.
• ti は, β 正規形.
定理 3.2
• β 簡約は, 強正規化性を持つ. (t1 →β t2 →β . . . となる無限列は存在しない.)
• βη 簡約は, 強正規化性を持つ.
3.3
高階単一化
記法 3.1 自由変数を大文字のアルファベット F, X, Y, . . . で表す.
• 正しいラムダ式
λx.F x
• 間違ったラムダ式
λx.xy
問題 3.1 (高階単一化) 単純型付ラムダ計算のラムダ式 t,s に対して, 以下を満たす代入 θ が存在
するか?
tθ =βη sθ
注意 3.1 =β η は, →β η の対称反射推移閉包.
例 3.9 自由変数 X の型を b → (b → b) → b とする.
λz.Xz(λy.y) =? λz.z
解は, 無限にある.
{X → λx.λf.x}
{X → λx.λf.fx}
{X → λx.λf.f(. . . (fx))}
代入 [t1 /X1 , . . . , tn /Xn ] を, {X → t1 , . . . , Xn → tn } と書くことにする.
12
定理 3.3
• 高階単一化問題は, 決定不能.
• 高階単一化問題は, semi-decidable.
定義 3.9 (long-βη 正規形) 以下の条件を満たすとき, λx1 ...xn.vs1 . . . sm は, long-βη 正規形で
あると言う.
• v : τ1 → . . . → τm → b. ただし, v は変数, または, 定数.
• si は, long-βη 正規形.
補題 3.2 βη 正規形のラムダ式 t に対して, long-βη 正規形のラムダ式 t が存在して以下が成り
立つ.
t →∗η t
例 3.10 変数 x の型が b → b, 変数 y の型が b の時.
λx.x =η λx.λy.xy
定数 f の型が b → (b → b) → b の時.
λy.fy =η ?
定義 3.10 λx1 . . . xk .v t1 . . . tn の形のラムダ式を考える.
• v が自由変数の場合, ﬂexible であると言う.
• それ以外の場合, rigid であると言う.
補題 3.3 ﬂexible なラムダ式の対は, 常に単一化を持つ.
λx1 . . . xk .F t1 . . . tm と λx1 . . . xk .G s1 . . . sn を考える.
{F → λx1 . . . xm .a, G → λx1 . . . xn .a}
例 3.11 ﬂexible なラムダ式と rigid なラムダ式の単一化. 例として F a =? a の単一化を考える.
• Projection
{F → λx.x}
• Imitation
{F → λx.a}
アルゴリズム 3.1 (高階単一化) E を long-βη 正規形のラムダ式の等式の集合, θ を代入とする.
E と θ の対の変換 (E, θ) ⇒ (E , θ ) の規則を以下のように定める.
• Deletion
(E ∪ {t =? t}, θ) ⇒ (E, θ)
• Elimination
(E ∪ {F =? t}, θ) ⇒ (E[t/F ], θ · [t/F ])
ただし, F ∈ F V (t).
13
• Decomposition: v は, 定数または束縛変数.
(E ∪ {λxk .vt1 . . . tn =? λxk .vt1 . . . tn }, θ) ⇒ (E ∪
{λxk .ti =? λxk .ti }, θ)
1≤i≤n
• Imitation: v は, 定数または束縛変数.
(E∪{λxk .F t1 . . . tn =? λxk .vt1 . . . tm }, θ) ⇒ (E∪{F =? t, λxk .F t1 . . . tn =? λxk .vt1 . . . tm }, θ)
ここで, t = λyn .v (H1 y1 . . . yn ) . . . (Hm y1 . . . yn )
• Projection
– ラムダ式 ti は, 型 τ1 → . . . → τj → τ を持つ.
– v は, 定数または束縛変数.
(E∪{λxk .F t1 . . . tn =? λxk .v t1 . . . tm }, θ) ⇒ (E∪{F =? t, λxk .F t1 . . . tn =? λxk .v t1 . . . tm }, θ)
ここで, t = λyn .yi (H1 y1 . . . yn ) . . . (Hj y1 . . . yn ).
例 3.12 f ∈ Cb→b , a ∈ Cb とする.
({F (f a) =? f(F a)}, ∅)
⇒ ({F =? λx.f(Y x), F (f a) =? f(F a)}, ∅)
⇒ ({f(Y (f a)) =? f(f(Y a))}, [λx.f(Y x)/F ])
⇒ ({Y (f a) =? f(Y a)}, [λx.f(Y x)/F ])
Imitation
Elimination
Decomposition
⇒ ({Y =? λx.x, Y (f a) =? f(Y a)}, [λx.f(Y x)/F ]) Projection
Elimination
⇒ ({f a =? f a}, [λx.f x/F, λx.x/Y ])
例 3.13 f, g : b → b → b, F : b → b, x, G, G1, G2 : b とする.
{λx.F (fxG) =? λx.g(fxG1 )(fxG2 )}
定理 3.4 (完全性) s =? t が単一化 θ を持つならば, 以下の条件を満たす F ,δ が存在する.
({s =? t}, ∅) ⇒∗ (F, δ)
• F は ﬂexible なラムダ式の等式の集合.
• δ は, θ より一般的.
例 3.14 単一化を持たない場合は, 止まるとは限らない.
X a =? f (Xa)
代入 [λx.f(Hx)/X] を考える.
f (H a) =? f (f (Ha))
14
3.4
高階単一化の決定不能性
定理 3.5 (Hilbert の第 10 問題) 係数が自然数の多項式 P (X1 , . . . , Xn ),Q(X1 , . . . , Xn ) に対し
て, 下の性質を満たす自然数 m1 , . . . , mn が存在するか判定する問題は, 決定不能.
P (m1 , . . . , mn ) = Q(m1 , . . . , mn )
多項式 P (X1 , . . . , Xn ),Q(X1 , . . . , Xn ) を以下のラムダ式で表現する.
p(X1 , . . . , Xn )
q(X1 , . . . , Xn )
ラムダ式 t が以下の等式の解ならば, t はチャーチ数
λz.Xz(λy.y) = λz.z
以下の等式の解を考える.
4
p(X1 , . . . , Xn ) =
q(X1 , . . . , Xn )
λz.X1 z(λy.y) =
..
.
λz.Xn z(λy.y) =
λz.z
λz.z
自然演繹 (Natural Deduction)
定義 4.1 (論理式 (formula))
• p(t1 , . . . , tn ) (p が n 引数の関数記号) (原始論理式 (atomic formula))
• ¬P ,P ∨ Q, P ∧ Q, P ⇒ Q, ∀x.P , ⊥, ∃x.P
定義 4.2 (自然演繹による証明) Γ を論理式の集合とする.
ΓP
ΓP ΓQ
∧I
ΓP ∧Q
ΓP ∧Q
∧E
ΓP
Γ, P Q
⇒I
ΓP ⇒Q
ΓP
∨I
ΓP ∨Q
(P ∈ Γ)
ΓQ
∨I
ΓP ∨Q
ΓP ∧Q
∧E
ΓQ
ΓP ⇒Q ΓP
⇒E
ΓQ
ΓP ∨Q
Γ P ∀I (x ∈ F V (Γ))
Γ ∀x.P
Γ, P R Γ, Q R
∨E
ΓR
Γ ∀x.P (x)
∀E
Γ P (t)
Γ, P ⊥
¬I
Γ ¬P
Γ P Γ ¬P
¬E
Γ⊥
Γ P (t)
∃I
Γ ∃x.P (x)
Γ ∃x.P (x) Γ, P (x) Q
∃E (x ∈ F V (Γ, Q))
ΓQ
Γ⊥
⊥
ΓP
Γ, ¬P ⊥
RAA
ΓP
15
• 古典論理 (classical logic): 上の規則を使って Γ P が導出できる時, Γ NK P と書く.
• 直観主義論理 (intuitionistic logic), 構成的論理 (constructive logic): RAA 以外の上の規則
を使って Γ P が導出できる時, Γ NJ P と書く.
注意 4.1 I の付いた規則を導入 (introduction) 規則といい, E の付いた規則を除去 (elimination)
規則という.
例 4.1
A∧B A∧B A∧B A∧B
A∧B B
A∧B A
A∧B B∧A
A∧B ⇒B∧A
例 4.2
• (A ⇒ B) ⇒ ((C ⇒ A) ⇒ (C ⇒ B)) の証明図.
• (P ∨ Q) ⇒ ((P ⇒ Q) ⇒ Q) の証明図.
• ∀x.P (x) ∨ Q ⇒ ∀x.(P (x) ∨ Q) の証明図. (ただし, x ∈ F V (Q)).
注意 4.2 ∀I の制限を取り除くと健全な証明にはならない.
x=0x=0
x = 0 ∀x.(x = 0)
x = 0 ⇒ ∀x.(x = 0)
∀x.(x = 0 ⇒ ∀x.(x = 0))
0 = 0 ⇒ ∀x.(x = 0)
例 4.3 NK では成り立つが, NJ で成り立たない性質.
• NK ¬¬P ⇒ P
¬¬P, ¬P ¬¬P ¬¬P, ¬P ¬P
¬¬P, ¬P ⊥
¬¬P P
¬¬P ⇒ P
• 排中律が NK で成り立つ. NK P ∨ ¬P , R = P ∨ ¬P
¬R, ¬¬P ¬¬P
¬R, ¬P ¬P
¬R, ¬¬P P
¬R, ¬¬P R
¬R, ¬¬P ¬R ¬R, ¬P R ¬R, ¬¬P ¬R
¬R, ¬¬P ⊥
¬R, ¬P ⊥
¬R ¬P
¬R P
¬R ⊥
P ∨ ¬P
• NK ¬(P ∧ Q) ⇒ ¬P ∨ ¬Q
• NK ¬∀x.P ⇒ ∃x.¬P
16
4.1
NJ の性質
定理 4.1 (disjunction property) NJ で P ∨ Q が証明可能ならば, P または Q が NJ で証明
可能.
定理 4.2 (existence property) NJ で ∃x.P が証明可能ならば, ある項 t が存在して, P [t/x] が
NJ で証明可能.
注意 4.3 NK では, 成立しない.
• P ∨ ¬P .
• ∃x.∀y(P (y) ⇒ P (x)).
4.2
Gödel の翻訳
定義 4.3 論理式から論理式への変換 P ◦ を以下のように定義する.
⊥◦
p(t1 , . . . , tn )◦
=
=
¬¬⊥
¬¬p(t1 , . . . , tn )
P ∧ Q◦
P ∨ Q◦
P ⇒ Q◦
∀x.P ◦
=
=
=
=
P ◦ ∧ Q◦
¬(¬P ◦ ∧ ¬Q◦ )
P ◦ ⇒ Q◦
∀x.P ◦
∃x.P ◦
=
¬∀x.¬P ◦
定理 4.3 Γ NK P と Γ◦ NJ P ◦ は, 同値である.
4.3
証明の簡約
例 4.4 ∧I と ∧E の組, ⇒ I と ⇒ E の組など I 規則と E 規則の組が証明に現れているとき証明
を簡約できる.
P, Q P P, Q Q
∧I
P, Q P ∧ Q
∧E
P, Q Q
P, Q P
∧I
P, Q Q ∧ P
P, Q Q P, Q P
∧I
P, Q Q ∧ P
P, Q, P ∧ Q P ∧ Q P, Q, P ∧ Q P ∧ Q
P, Q, P ∧ Q (P ∧ Q) ∧ (P ∧ Q)
P, Q P P, Q Q
⇒I
P, Q (P ∧ Q) ⇒ (P ∧ Q) ∧ (P ∧ Q)
P, Q (P ∧ Q)
⇒E
P, Q (P ∧ Q) ∧ (P ∧ Q)
P, Q P P, Q Q P, Q P P, Q Q
P, Q (P ∧ Q)
P, Q (P ∧ Q)
P, Q (P ∧ Q) ∧ (P ∧ Q)
注意: 簡約した証明が必ずしも小さくなるとはいえない.
17
例 4.5 ∧I と ∧E の組はないが, 簡約できる.
P ∨P P ∨P
P ∨ P, P P P ∨ P, P P
∧I
P ∨ P, P P ∧ P
P ∨P P ∧P
∧E
P ∨P P
P ∨P P ∨P
4.4
P ∨ P, P P
P ∨P P
P ∨ P, P P P ∨ P, P P
∧I
P ∨ P, P P ∧ P
∨E
P ∨ P, P P
Curry-Howard 同型対応
定義 4.4 (NJ のサブセット)
P ::= A | P ∧ Q | P ⇒ Q
A は, 命題変数.
定義 4.5 (型付ラムダ計算の構文)
型
式
τ ::= A | τ → τ | τ × τ
t ::= x | λx.t | tt | t, t | π0 (t) | π1 (t)
ここで, A は型変数.
(注意：ここでは, 定数を考えない)
Γ t0 : τ0 Γ t1 : τ1
Γ t0 , t1 : τ0 × τ1
Γ t : τ0 × τ1
Γ π0 (t) : τ0
Γ t : τ0 × τ1
Γ π1 (t) : τ1
簡約規則
π0 (t0 , t1 ) → t0
π1 (t0 , t1 ) → t1
例 4.6
x : (A → B) × A x : (A → B) × A x : (A → B) × A x : (A → B) × A
x : (A → B) × A π0 (x) : A → B
x : (A → B) × A π1 (x) : A
λx.π0 (x)π1 (x) : (A → B) × A → B
例 4.7
(λx.π0 (x)π1 (x))λy.y, v
→ π0 (λy.y, v)π1 (λy.y, v)
→ (λy.y)π1 (λy.y, v)
→ (λy.y)v
→ v
定義 4.6 (Curry-Howard の対応 (論理式と型))
Φ(A)
Φ(P ∧ Q)
=
=
A
Φ(P ) × Φ(Q)
Φ(P ⇒ Q)
=
Φ(P ) → Φ(Q)
18
定義 4.7 (Curry-Howard の対応 (証明と項)) 以下は同値.
• 論理式 P が証明可能.
• 型 Φ(P ) を持つ閉じたラムダ式が存在.
Γ t0 : Φ(P ) Γ t1 : Φ(Q)
Γ t0 , t1 : Φ(P ) × Φ(Q)
ΓP ΓQ
∧I
ΓP ∧Q
Γ t0 : Φ(P ) → Φ(Q) Γ t1 : Φ(P )
Γ t0 t1 : Φ(Q)
ΓP ⇒Q ΓP
⇒E
ΓQ
例 4.8 以下の証明図に対応するラムダ式: λx.π1 (x), π0 (x).
A∧B A∧B A∧B A∧B
A∧B B
A∧B A
A∧B B∧A
A∧B ⇒B∧A
例 4.9 (A ⇒ B) ⇒ ((C ⇒ A) ⇒ (C ⇒ B)) の証明図に対応するラムダ式.
定義 4.8 (Curry-Howard の対応 (証明と項の簡約)) 証明と項の簡約が対応している.
例 4.10 x : P , y, Q, z : P ∧ Q とする.
• P, Q Q ∧ P の証明の簡約
y, π0 x, y → y, x
• P, Q (P ∧ Q) ∧ (P ∧ Q) の証明の簡約
(λz.z, z)x, y → x, y, x, y
高階論理と Logical Framework
5
5.1
高階論理 (Higher Order Logic)
定義 5.1 (直観主義高階論理)
• 型: b は基本型, prop は論理式の型
τ ::= b | prop | τ → τ
• 項
t ::= c | x | ∀x : τ.t | τ ⇒ τ | tt | λx.t
c ∈ Cτ
c:τ
x ∈ V arτ
x:τ
x ∈ V arτ1 t : τ2
λx.t : τ1 → τ2
t1 : τ1 → τ2 t2 : τ1
t1 t2 : τ2
t1 : prop t2 : prop
t1 ⇒ t2 : prop
型 prop の項をメタ変数 φ,ψ で表す.
19
x ∈ V arτ t : prop
∀x.t : prop
例 5.1
• 数学的帰納法 P : nat → prop, x : nat
∀P.((P 0) ⇒ ∀x.(P x ⇒ P (x + 1)) ⇒ ∀x.P x)
• 関係が推移的. R : τ → τ → prop, x, y, z : τ .
λR.∀x.∀y.∀z.(Rxy ⇒ Ryz ⇒ Rxz)
定義 5.2 高階論理による証明を定義する. Γ φ は, Γ を仮定して φ が証明できることを意味し
ている.
φ∈Γ
axiom
Γφ
Γ φ ψ =β φ
conv
Γψ
Γ, φ ψ
⇒I
Γφ⇒ψ
Γφ⇒ψ Γφ
⇒E
Γψ
Γ φ x ∈ F V (Γ)
∀I
Γ ∀x.φ
Γ ∀x.φ
t : τ x ∈ V arτ
∀E
Γ φ[t/x]
例 5.2 x : b → b, y, c : b とする.
∀x.∀y.P (xy) ∀x.∀y.P (xy)
∀E
∀x.∀y.P (xy) ∀y.P ((λy.y)y)
∀E
∀x.∀y.P (xy) P ((λy.y)c)
P ((λy.y)c) = P c
conv
∀x.∀y.P (xy) P c
例 5.3 以下のように他の論理結合子を定義できる.
φ∧ψ
::= ∀x.(φ ⇒ ψ ⇒ x) ⇒ x
φ ∨ ψ ::= ∀x.(φ ⇒ x) ⇒ (ψ ⇒ x) ⇒ x
⊥ ::= ∀x.x
¬φ ::= φ ⇒ ⊥
ただし, x : prop.
• φ∧ψ φ
φ ∧ ψ, φ, ψ φ
⇒I
φ∧ψ φ∧ψ
φ ∧ ψ, φ ψ ⇒ φ
∀E
⇒I
φ ∧ ψ (φ ⇒ ψ ⇒ φ) ⇒ φ
φ∧ψ φ ⇒ ψ ⇒ φ
⇒E
φ∧ψ φ
• φ φ ∨ ψ, ⊥ φ
5.2
Logical Framework としての高階論理
注意 5.1 Logical Framework : 論理体系を形式化する体系
• メタ論理 : 高階論理
• オブジェクト論理 : 一階述語論理
20
定義 5.3 NJ の論理式を以下の形式に制限した体系を考える.
P ::= p(t1 , . . . , tn ) | ⊥ | P ⇒ Q | ∀x.P
この体系の証明を Γ N P を書くことにする.
定義 5.4 述語論理を以下のようにして, 高階論理に埋め込む.
• 基本型: o (オブジェクト論理の論理式の型)
• 定数記号 c に対して, c ∈ Cb .
• n 引数の関数記号 f に対して, f ∈ Cb→...→b→b
• n 引数の述語記号 p に対して, p ∈ Cb→...→b→o
• 高階論理の定数として以下のものを考える.
imp
: o→o→o
forall : (b → o) → o
false : o
Φ(x) =
Φ(c) =
Φ(f(t1 , . . . , tn ))
Φ(p(t1 , . . . , tn ))
Φ(P ⇒ Q)
Φ(∀x.P )
=
=
=
=
x
c
f Φ(t1 ) . . . Φ(tn )
p Φ(t1 ) . . . Φ(tn )
imp Φ(P ) Φ(Q)
forall(λx.Φ(P ))
例 5.4 ∀x.p(x, x) ⇒ p(f(y), f(y)) の埋め込み.
imp(forall(λx.p x x))(p(f y)(f y))
例 5.5 ∀x.p(x) ⇒ ∀y.q(x, y) の埋め込み.
補題 5.1 t を一階述語論理の項, P を一階述語論理の論理式とする.
• Φ(t) : b
• Φ(P ) : o
定義 5.5 (証明の埋め込み) 以下の型をもつ定数 nd を用いて, P が証明で可能であることを表す.
nd : o → prop
注意: 以下が同値になるようにしたい.
• P が一階述語論理で証明できる.
• nd(Φ(P )) が高階論理で証明できる.
21
定義 5.6 (推論規則の埋め込み) 以下の公理を高階論理に入れることで, 推論規則を埋め込む.
(nd(φ) ⇒ nd(ψ)) ⇒ nd(imp φ ψ)
nd(imp φ ψ) ⇒ nd(φ) ⇒ nd(ψ)
∀x.nd(φ) ⇒ nd(forall(λx.φ))
nd(forall(λx.φ)) ⇒ nd(φ[t/x])
nd(false) ⇒ nd(φ)
この公理の集合を N D とする. (x ∈ V arb ).
例 5.6
P, P ⇒ ⊥ N P ⇒ ⊥ P, P ⇒ ⊥ N P
⇒E
P, P ⇒ ⊥ N ⊥
⇒I
P N (P ⇒ ⊥) ⇒ ⊥
⇒I
N P ⇒ ((P ⇒ ⊥) ⇒ ⊥)
Γ A3
HOL
Γ
Γ nd(Q)
nd(P ) ⇒ nd(false)
Γ HOL nd(P )
N D, nd(P ), nd(Q) HOL nd(false)
N D, nd(P ) HOL A2
N D, nd(P ) HOL nd(Q) ⇒ nd(false)
N D, nd(P ) HOL nd(impQfalse)
N D HOL A1
N D HOL nd(P ) ⇒ nd(impQfalse)
N D HOL nd(imp P (impQfalse))
Q ≡
Γ
A1
A2
A3
≡
≡
≡
≡
imp P false
N D, nd(P ), nd(Q)
(nd(P ) ⇒ nd(impQfalse)) ⇒ nd(imp P (impQfalse))
(nd(Q) ⇒ nd(false)) ⇒ nd(impQfalse)
nd(imp P false) ⇒ nd(P ) ⇒ nd(false)
注意: A1 , A2 , A3 は, N D に含まれる公理.
例 5.7 以下の証明を高階論理に埋め込め.
∀x.p(x) ∀x.p(x)
∀x.p(x) p(f(y))
∀x.p(x) ∀y.p(f(y))
N ∀x.p(x) ⇒ ∀y.p(f(y))
定理 5.1 (Adequacy) 以下は同値.
• N D HOL nd(Φ(P ))
• N P
22
Isabelle のメタ論理
5.3
定義 5.7 (Isabelle の記法)
• 型
高階論理
Isabelle
----------------------------------prop
prop
nat → nat
nat => nat
nat → nat → nat
[nat,nat] => nat
• 項
高階論理
Isabelle
----------------------------------λx.λy.xy
%x.%y.xy
P ⇒Q
P ⇒Q⇒R
∀x.P (x)
P ==> Q
[|P; Q|] ==> R
!!x.P(x)
自由変数
?x, ?P
定義 5.8 (Isabelle による論理の定義) 直観主義一階述語論理の定義の一部
theory IFOL = Pure
typedecl o
judgment
Trueprop
:: "o => prop"
consts
-->
:: "[o, o] => o"
All
axioms
impI:
mp:
allI:
spec:
(infixr 25)
:: "(’a => o) => o"
"(P ==> Q) ==> P-->Q"
"[| P-->Q; P |] ==> Q"
"(!!x. P(x)) ==> (All (%x. P(x)))"
"(All (%x. P(x))) ==> P(x)"
end
例 5.8 (Isabelle による証明)
theory foltest = IFOL:
lemma "P --> ((P --> false) --> false)"
apply (rule impI)
23
apply (rule impI)
apply (rule mp)
apply (assumption)
apply (assumption)
done
end
例 5.9 (Isabelle による証明)
lemma "P --> ((P --> false) --> false)"
proof (rule impI)
assume P
show "(P --> false) --> false"
proof (rule impI)
assume "P --> false"
show "false"
proof (rule mp)
show "P --> false"
by assumption
show "P"
by assumption
qed
qed
qed
5.4
Isabelle の推論規則
定義 5.9 (ゴール) 証明すべきことは, 以下の形をしたサブゴールのリストで与えられる.
!!x1...xn.[| P1; P2; ....; Pn |] ==> P
P は, 原始論理式 (!!,==>を含まない).
注意: 以下は同値
• P ⇒ ∀x.Q(x)
• ∀x.P ⇒ Q(x)
ただし, x ∈ F V (P ).
定義 5.10 (推論規則: 仮定 (assumption))
• ゴール: [| P1; P2; ....; Pn |] ==> P
• P と Pi が単一化を持つ.
• このゴールは, 証明できた.
(他のゴールに単一化を適用する必要がある. ）
例 5.10
24
lemma "P(f (x)) ==> P(?y)"
apply (assumption)
done
上の証明で以下の定理が証明されたことになる.
P(f(x)) ==> P(f(x))
P はどんな論理式でも, f, x はどんな項でもいいので, 以下の補題が証明できたことになる
lemma ?P(?f(?x)) ==> ?P(?f(?x))
定義 5.11 (導出原理に基づく推論: rule)
• ゴール: P
• 定理 : [| Q1; Q2; ...
; Qn |] ==> Q
• P と Q が単一化 θ を持つ
• 新ゴール: Q1’,Q2’,....,Qn’
Qi’ は Qi に代入 θ を適用した論理式
例 5.11 導出 (rule impI)
• ゴール: P --> ((P --> false) --> false)
• 定理 : (?P ==> ?Q) ==> ?P--> ?Q
• 新ゴール : P ==> ((P --> false) --> false)
定義 5.12
• ゴール: P1 ==> P
• 定理: [| Q1; Q2; ...
; Qn |] => Q
• P と Q が単一化 θ を持つ: ゴールと以下の論理式の導出
[| P1 ==> Q1; P1 ==> Q2... ; P1 ==> Qn |] ==> (P1 ==> Q)
• 新ゴール: P1’ ==> Q1’,P1’ ==> Q2’,....,P1’ ==> Qn’
P1’ は P1 に代入 θ を適用した論理式 Qi’ は Qi に代入 θ を適用した論理式.
例 5.12 導出 (rule mp)
• ゴール: [| P; P --> false |] ==> false
• 定理 : [|?R; ?R --> ?Q |]==> ?Q
[|[| P; P --> false |] ==> ?R;
[| P; P --> false |] ==> ?R --> ?Q |]==> ([| P; P --> false |] ==> ?Q)
• 新ゴール :
– [| P; P --> false |] ==> ?R
– [| P; P --> false |] ==> ?R --> false
25
定義 5.13 (Isabelle のインストール)
• 以下の URL を参照して Isabelle をインストールしてください.
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html
• 以下のコマンドで FOL 一階述語論理を使えるようにしてください.
% cd /usr/local/Isabelle
% ./build FOL
• xemacs が必要です.
• 以下のコマンドで, 一階述語論理を使った証明を, ファイル foltest.thy に作成できます.
/usr/local/Isabelle/bin/Isabelle -l FOL foltest.thy
6
Isabelle/HOL
6.1
Isabelle の推論規則
例 6.1 (Isabelle の実行)
• 以下のコマンドは, 論理 FOL を用いて foltest.thy というファイルに証明を書くことを意
味している.
/usr/local/Isabelle/bin/Isabelle -l FOL foltest.thy
• 一行検証を進めるには, C-c C-n.
• 一行戻るには, C-c C-u.
theory foltest = IFOL:
lemma "All (%x. P(x)) --> All (%y. P(f(y)))"
apply (rule impI)
apply (rule allI)
apply (rule spec)
apply (assumption)
done
– 一行目は, このファイルに作る理論 (theory) の名前が foltest であり foltest が理論
IFOL に基づいていることを示している.
定義 6.1 (導出原理の基づく推論 (rule))
• ゴール: !!x.P
• 定理: [|Q ?y; R ?y |]=> S ?y
[|!!x.Q (?y x); !!x.R (?y x)|]=> !!x.S (?y x)
26
• %x.P と%x.S (?y x) の単一化を考えて導出.
例 6.2 導出 (rule spec)
• ゴール: !!y.All (%x.P(x)) ==> P(f(y))
• 定理 spec : (All (%z.
?Q(z))) ==> ?Q(?z)
[|!!y. All (%x.P(x)) ==> (All (%x. ?Q y x)) |]
==> (!!y.All (%x.P(x))==> ?Q y (?z y))
• %y.P(f(y)) と%y.?Q y (?z y) には, 3 つ単一化が存在する.
• 新ゴール
– ?Q = %ab.P(f a) の場合
!!y. All (%x.P(x)) ==> (All (%x. P(f(y))))
– ?Q = %ab.P(f b),?z = %a.a の場合
!!y. All (%x.P(x)) ==> (All (%x. P(f(x))))
– ?Q = %ab.Pb,?z = % a.fa の場合
!!y. All (%x.P(x)) ==> (All (%x. P(x))))
例 6.3 ラムダ式に書き直すと λy.p(f(y)) と λy.Q y(Z y) の単一化の問題
Q
Q
= λab.p(fa)
= λab.p(fb),
Z
= λa.a
Q
= λab.P b,
Z
= λa.fa
• Imitation: Q = λab.p(Rab)
λy.f(y) =? λy.Ry(Zy)
– Imitation: R = λab.f(Sab)
λy.y =? λy.Sy(Zy)
∗ Projection: S = λab.a
∗ Projection: S = λab.b, Z = λa.a
– Projection: R = λab.b, Z = λa.fa
例 6.4 (別の単一化による導出)
lemma "All (%x. P(x)) --> All (%y. P(f(y)))"
apply (rule impI)
apply (rule allI)
apply (rule spec)
back
back
次の単一化による導出
例 6.5 (定理に対する代入)
27
lemma "All (%x. P(x)) --> All (%y. P(f(y)))"
apply (rule impI)
apply (rule allI)
定理 spec の一つ目の自由変数に P を代入
apply (rule spec[of P])
単一化は一種類
6.2
HOL
定義 6.2 (チャーチの高階論理 (HOL))
• 型
τ ::= o | i | τ → τ
• 項
t ::= c | x | tt | λx.t | t ⇒ t | t = t | t
– (λx.t)(Hilbert の演算子) の意味. x は, τ 型とする.
∗ t を満たす要素 x が存在するとき. t を満たす τ 型の任意の元.
(λx.x > 1)
∗ t を満たす要素 x が存在しないとき. τ 型の任意の元.
c ∈ Cτ
c:τ
x ∈ V arτ
x:τ
x ∈ V arτ1 t : τ2
λx.t : τ1 → τ2
t1 : τ1 → τ2 t2 : τ1
t1 t2 : τ2
t1 : τ t2 : τ
t1 = t2 : o
t1 : o t2 : o t : τ → o
t1 ⇒ t2 : o
t : o
定義 6.3 (HOL の証明規則)
φ∈Γ
axiom
Γφ
Γ (λx.t1 )t2 = t1 [t2 /x]
Γt=t
refl
Γ t = t Γ s[t/x]
subst
Γ s[t /x]
beta
Γφ⇒ψ Γφ
⇒E
Γψ
Γ, φ ψ
⇒I
Γφ⇒ψ
例 6.6 以下のように他の論理結合子を定義できる.
::= (λx.x) = (λx.x)
∀φ ::= φ = (λx.)
∃φ ::= ∀ψ.(∀x.φx ⇒ ψ) ⇒ ψ
⊥
φ∧ψ
φ∨ψ
::= ∀φ.φ
::= ∀x.(φ ⇒ ψ ⇒ x) ⇒ x
::= ∀x.(φ ⇒ x) ⇒ (ψ ⇒ x) ⇒ x
¬φ ::= φ ⇒ ⊥
28
定義 6.4 (公理)
∀φ.∀ψ.(φ ⇒ ψ) ⇒ (ψ ⇒ φ) ⇒ (φ = ψ)
∀φ.(φ = ) ∨ (φ = ⊥)
∀φ.∀x.φx ⇒ φ((φx))
6.3
Isabelle/HOL
定義 6.5 (オブジェクト論理の文法)
HOL
Isabelle/HOL
----------------------------------
True
⊥
P ⇒Q
P ∧Q
P ∨Q
False
P --> Q
P & Q
P | Q
¬ P
~P
∀(λx.P (x))
∃(λx.P (x))
!x.P(x)
? x.P(x)
----------------------------------例 6.7 (Isabelle/HOL の使い方)
• コマンド: Isabelle holtest.thy (ディフォルトの論理は, HOL)
theory holtest = Main:
lemma "P --> ((P --> false) --> false)"
apply (rule impI)
apply (rule impI)
apply (rule mp)
apply (assumption)
apply (assumption)
done
定義 6.6 (Isabelle/HOL の論理)
impI:
mp:
(P ==> Q) ==> P-->Q
[| P-->Q;
P |] ==> Q
notI: (P ==> False) ==> ~P
notE: [| ~P; P |] ==> R
conjI: [| P; Q |] ==> P & Q
conjunct1: P & Q ==> P
29
conjunct2: P & Q ==> Q
conjE: [| P & Q; [| P; Q |] ==> R |] ==> R
disjI1: P ==> P | Q
disjI2: Q ==> P | Q
disjE: [| P | Q; P ==> R; Q ==> R |] ==> R
allI:
spec:
allE:
(!!x. P x) ==> ALL x. P x
ALL x. P x ==> P x
[| ALL x. P x; P x ==> R |] ==> R
exI: P x ==> EX x. P x
exE: [| EX x. P x; !!x. P x ==> Q |] ==> Q
FalseE: False ==> P
ccontr: (~ P ==> False) ==> P
消去規則
6.4
例 6.8
• ゴールの形: [| A | B; C1; ...; Cn|] ==> D
• ゴールの仮定の中の|を消去する推論を行う.
Γ, P R Γ, Q R
Γ, P ∨ Q R
[| ?P | ?Q; ?P ==> ?R; ?Q ==> ?R |] ==> ?R
定義 6.7 (導出原理に基づく推論: erule)
• ゴール: P1 ==> P
• 定理 : [| Q1; Q2 => ?R|] ==> ?R
• ゴールと定理で導出
• 中間ゴール
P1 ==> Q1
[| P1;Q2|] ==> P
• P1 ==> Q1 を assumption で証明.
• 中間ゴール
[| P1’;Q2’|] ==> P’
• 新ゴール: erule では, 仮定 P1’ を消去して以下の形のゴールが残る.
30
Q2’ ==> P’
例 6.9
lemma disjexch: "P | Q ==> Q | P"
apply (erule disjE)
apply
apply
apply
apply
(rule disjI2)
(assumption)
(rule disjI1)
(assumption)
done
disjexch がこの補題の名前になる.
例 6.10 以下を Isabelle/HOL で証明せよ.
• (A ⇒ B) ⇒ ((C ⇒ A) ⇒ (C ⇒ B)).
• (P ∨ Q) ⇒ ((P ⇒ Q) ⇒ Q).
• ∀x.P (x) ∨ Q ⇒ ∀x.(P (x) ∨ Q). (ただし, x ∈ F V (Q)).
• ¬¬P ⇒ P .
例 6.11 (自動証明)
lemma "(P | Q) --> (P --> Q) --> Q"
apply (auto)
例 6.12 (定数の定義)
constdefs
xor :: "[bool, bool] => bool"
"xor A B == (A & ~B) | (~A & B)"
xor_def という名前で, 上の定義が定理として登録される.
例 6.13 (定義の展開) 証明法 simp は, ゴールを書き換えによって単純化する.
lemma "xor A (~A)"
apply (simp only: xor_def)
apply (auto)
done
• :only xor_def は, xor_def のみを書き換えに用いることを示している.
例 6.14
• ... の部分を埋めて, myand, myall を完成せよ.
constdefs
myand :: "[bool, bool] => bool"
"myand == ..."
myall :: "(’a => bool) => bool"
"myall == ..."
31
上の myall のように多相型を持つ定数を定義できる.
• 下の補題を証明せよ.
lemma "myand P Q --> P"
lemma "myall (%x. P x) ==> P t"
定義 6.8 (Hilbert の演算子)
• Isabelle/HOL での記法 Eps.
Eps(%x. P x) を SOME x.P x と書く.
• 公理
someI: "P (x::’a) ==> P (SOME x. P x)"
例 6.15 (Hilbert の演算子)
• 逆関数の定義
constdefs
inv :: "(’a => ’b) => (’b => ’a)"
"inv(f :: ’a => ’b) == %y. SOME x. f x = y"
• 下の補題を証明せよ.
lemma "inv (%x. x) = (%x. x)
以下の HOL の公理を用いてよい.
ext:
"(!!x::’a. (f x ::’b) = g x) ==> (%x. f x) = (%x. g x)"
refl:
"t = (t::’a)"
例 6.16 (選択公理 (axiom of choice) の証明) 「任意の集合の集合 a に対して, a から
の関数 f が存在して, x ∈ a かつ x = ∅ ならば f(x) ∈ x」
lemma "(!x. ? y. Q x y) --> (? f. ! x. Q x (f x))"
Q:’a -> ’b -> bool を集合の集合と考えられる.
課題 6.1 以下の補題を証明せよ.
lemma "~(P & Q) --> (~P |~Q)"
lemma "(~ (!x. P x)) --> (? x.~(P x))"
Isabelle/HOL: データ型、原始帰納関数、帰納法
7
7.1
自然数と原始帰納関数
例 7.1 (自然数)
• 型: nat
32
aへ
• 定数: 0:nat, Suc:nat => nat
• 関数: +, -, *
• 関係: <, <=
例 7.2 (自然数に関する証明)
lemma "Suc(0) <= Suc(Suc(0)) + Suc(0)"
apply (simp)
done
定義 7.1 (原始帰納関数)
f(x1 , . . . , xn, 0) = g(x1 , . . . xn )
f(x1 , . . . , xn, y + 1) = h(x1 , . . . , xn , y, f(x1 , . . . , xn , y))
関数 g, h は, 既に定義されている関数.
例 7.3 (原始帰納関数)
consts
add :: "[nat, nat] => nat"
primrec
"add 0 y = y"
"add (Suc x) y = Suc (add x y)"
上の定義が, ディフォルトの書き換え規則に加えられる.
lemma "add (Suc 0) (Suc 0) = Suc (Suc 0)"
apply (simp)
done
例 7.4 (数学的帰納法による証明)
lemma "add x (add y z) = add (add x y) z"
apply (induct x)
apply (simp)
x に関する帰納法
apply (simp)
done
例 7.5
• 乗算を定義せよ. 加算を用いる場合は, +を用いること.
consts
mul :: "[nat, nat] => nat"
• 以下の定理を証明せよ.
lemma "mul x (y + z) = (mul x y) + (mul x z)"
課題 7.1 以下の定理を証明せよ. 幾つか補題を証明しておく必要がある.
lemma "add x y = add y x"
33
7.2
リストと帰納法
定義 7.2 (リストの定義) Isabelle/HOL では, 以下のようにリストが定義されてりる.
datatype ’a list = Nil
("[]")
| Cons ’a "’a list" (infixr "#" 65)
#を, 0#[] のように中置記法の演算子として使えるように定義されている.
例 7.6 Main では, 既にリストが定義されているので, 以下のようにして PreList をベースにし
てリストを定義する.
theory MyList = PreList:
datatype ’a list = Nil
("[]")
| Cons ’a "’a list" (infixr "#" 65)
定義 7.3 (原始帰納関数の定義)
consts
app :: "[’a list, ’a list] => ’a list" (infixr "@" 65)
rev :: "’a list => ’a list"
primrec
"[]@ ys = ys"
"(x#xs)@ys = x#(xs@ ys)"
primrec
"rev [] = []"
"rev (x#xs) = (rev xs)@(x#[])"
例 7.7 (リストに関する帰納法)
lemma app_Nil2: "xs@[] = xs"
apply (induct xs)
apply (simp)
apply (simp)
done
以下のようにすると, この定理が simp で標準的に使われる書き換えの規則に加えられる.
lemma app_Nil2[simp]: "xs@[] = xs"
例 7.8 以下の補題を証明せよ.
lemma app_assoc: "(xs@ys)@zs = xs@(ys@zs)"
lemma rev_app: "rev (xs@ys) = rev ys @ rev xs"
lemma "rev (rev xs) = xs"
課題 7.2 リストの反転を別の方法で以下のように定義する.
consts
itrev :: "[’a list, ’a list] => ’a list"
primrec
"itrev [] ys = ys"
"itrev (x#xs) ys = itrev xs (x#ys)"
34
このとき, 以下の定理を証明せよ.
lemma "itrev xs [] = rev xs"
注意: 補助的な補題が必要になる.
データ型を定義するとなにが起こるか
7.3
例 7.9
• データ型 nat を定義すると nat_rec が定義される.
datatype nat = 0 | Suc nat
コマンド term nat_rec の型を調べられる.
"nat_rec" :: "[’a, [nat, ’a] => ’a, nat] => ’a"
nat.recs という名前で, 以下の定理が加えられる.
nat_rec ?f1.0 ?f2.0 0 = ?f1.0
nat_rec ?f1.0 ?f2.0 (Suc ?nat) = ?f2.0 ?nat (nat_rec ?f1.0 ?f2.0 ?nat)
例 7.10 constdefs
myadd ::
"myadd x
mymul ::
"mymul x
"[nat, nat] =>
y == nat_rec y
"[nat, nat] =>
y == nat_rec 0
nat"
(%a.%b. Suc b) x"
nat"
(%a. %b. myadd b y) x"
例 7.11 (帰納法) データ型を定義すると帰納法の定理が加えられる.
• nat.induct
[| ?P 0; !!n. ?P n ==> ?P (Suc n) |] ==> ?P ?n
nat.induct を直接使うこともできる.
lemma "add x (add y z) = add (add x y) z"
apply (rule nat.induct [of _ x])
apply (simp)
apply (simp)
done
7.4
集合
定義 7.4 (集合の記法)
• t set: t 型の集合
35
数学
Isabelle/HOL
---------------------------------∅
{}
x∈A
A⊂B
A∪B
A∩B
x:A
A <= B
A Un B
A Int B
A\B
{x}
A - B
{x}
例 7.12
lemma "(A Un B) Int C = (A Int C) Un (B Int C)"
apply (auto)
done
lemma "x : (A Un {y}) --> (x : A | x = y)"
apply (auto)
done
7.5
例: 式の評価
定義 7.5
• 以下の文法で定義される式の評価を考える.
e ::= i | x | e + e | e − e
– i は, 自然数の定数
– x は, 変数
• σ を変数から自然数への関数とする.
[[i]]σ
[[x]]σ
[[e1 + e2 ]]σ
[[e1 − e2 ]]σ
=
=
=
=
例 7.13
• 式の形式化
types var = nat
datatype exp =
|
|
|
NatExp nat
VarExp var
PlusExp exp exp
MinusExp exp exp
注意: 変数を自然数で表している.
36
i
σ(x)
[[e1 ]]σ + [[e2 ]]σ
[[e2 ]]σ − [[e2 ]]σ
• 評価
consts
eval :: "[exp, var => nat] => nat"
primrec
"eval
"eval
"eval
"eval
(NatExp i) env = i"
(VarExp x) env = env x"
(PlusExp e1 e2) env = eval e1 env + eval e2 env"
(MinusExp e1 e2) env = eval e1 env - eval e2 env"
例 7.14
• 自由変数の定義
consts
fv :: "exp => var set"
primrec
"fv (NatExp i) = {}"
"fv (VarExp x) = {x}"
"fv (PlusExp e1 e2) = fv e1 Un fv e2"
"fv (MinusExp e1 e2) = fv e1 Un fv e2"
• 証明
lemma "!env. (!x. (x:fv exp --> env1 x = env2 x)) --> eval exp env1 = eval exp env2"
apply (induct exp)
apply (auto)
done
7.6
集合の帰納的定義
例 7.15
• 偶数の集合の定義
consts
even :: "nat set"
inductive even
intros
even_base: "0 : even"
even_step: "x : even ==> Suc (Suc x) : even"
• 導入規則: even_base,even_step が定理になる.
• even.induct: 帰納法の定理が自動的に生成される
[| ?xa : even; ?P 0; !!x. [| x : even; ?P x |] ==> ?P (Suc (Suc x)) |]
==> ?P ?xa
37
例 7.16 even.induct による証明.
lemma "x : even --> y : even --> x + y : even"
apply (rule impI)
apply
apply
apply
apply
(erule even.induct)
(simp)
(rule impI)
(simp)
apply (rule even_step)
apply (assumption)
done
例 7.17
• 下の集合を帰納法で定義せよ.
{2n 3m | n, m ∈ N }
• 下を定理を証明せよ.
lemma "x : twothree --> y : twothree --> x * y : twothree"
注意: 乗算の結合律を以下の形で使う.
apply (simp add: mult_assoc)
8
8.1
多相型, 依存型
System F
定義 8.1 (多相ラムダ計算 (Polymorphic lambda calculus,System F))
型
項
x:τ ∈Γ
Γx:τ
τ ::= α | τ → τ | ∀α.τ
t ::= x | λx : τ.t | tt | Λα.t | t[τ ]
Γ, x : τ1 t : τ2
Γ λx : τ1 .t : τ1 → τ2
Γ t : τ α ∈ F T V (Γ)
Γ Λα.t : ∀α.τ
Γ t1 : τ1 → τ2 Γ t2 : τ1
Γ t1 t2 : τ2
Γ t : ∀α.τ
Γ t[τ ] : τ [τ /α]
例 8.1 (λx : ∀α.α → α.(x[β → β])(x[β]))(Λα.λx : α.x) : β → β
x : ∀α.α → α x[β → β] : (β → β) → (β → β) x : ∀α.α → α x[β] : (β → β)
x : ∀α.α → α (x[β → β])(x[β]) : β → β
λx : ∀α.α → α.(x[β → β])(x[β]) : (∀α.α → α) → (β → β)
Λα.λx : α.x : ∀α.α → α
(λx : ∀α.α → α.(x[β → β])(x[β]))(Λα.λx : α.x) : β → β
例 8.2 型を list(τ ) で拡張する.
nil : ∀α.list(α)
cons : ∀α.α → list(α) → list(α)
38
• cons[nat]1(nil[nat]) : list(nat)
• Λα.λf:β → α.λx:β.cons[α](fx)(nil[α]) の型を示せ.
定義 8.2 (簡約)
(λx : τ.t)s →β t[s/x]
(Λα.t)[τ ] →β t[τ /α]
例 8.3
(λx : ∀α.α → α.(x[β → β])(x[β]))(Λα.λx : α.x)
→β
→β
→β
→β
(Λα.λx : α.x)[β → β]((Λα.λx : α.x)[β])
(λx : β → β.x)((Λα.λx : α.x)[β])
(λx : β → β.x)(λx : β.x)
(λx : β.x)
定義 8.3 (高階命題論理)
• 論理式
φ ::= x | ∀x.φ | φ ⇒ φ
• 証明
Γ, φ ψ
⇒I
Γφ⇒ψ
φ∈Γ
axiom
Γφ
Γ φ x ∈ F V (Γ)
∀I
Γ ∀x.φ
• 他の論理演算子
Γφ⇒ψ Γφ
⇒E
Γψ
Γ ∀x.φ
∀E
Γ φ[ψ/x]
φ∧ψ
::= ∀x.(φ ⇒ ψ ⇒ x) ⇒ x
φ∨ψ
⊥
::= ∀x.(φ ⇒ x) ⇒ (ψ ⇒ x) ⇒ x
::= ∀x.x
例 8.4 型 (∀α.(A → B → α) → α) → A のラムダ式を見つけよ. A ∧ B ⇒ A の証明をラムダ式
として書くことになる.
8.2
依存型
例 8.5 (依存型 (dependent type))
• 長さが 10 のリストの型
list(10)
• 長さが x のリストに対して, 長さが 2x のリストを返す関数
λx.x@x : list(x) → list(2x)
定義 8.4 (依存型ラムダ計算)
• 構文
型
κ ::= ∗ | Πx : τ.κ
τ ::= b | Πx : τ.τ | τ t
項
t ::= x | λx : τ.t | tt
カインド
注意: 直観的には, カインドは型の型. 通常の型のカインドは ∗.
カインドの例: list : Πx : nat.∗.
依存型の例: Πx : nat.Πy : list(x).list(x + 1).
39
• 判定 Γ κ
Γ, x : τ κ
Γ Πx : τ.κ
Γ∗
• 判定 Γ τ : κ
Γ τ : Πx : τ .κ Γ t : τ Γ τ t : κ[t/x]
Γ, x : τ1 τ2 : ∗
Γ Πx : τ1 .τ2 : ∗
b ∈ Tκ
Γb:κ
Γ τ : κ κ =β κ
Γτ :κ
• 判定 Γ t : τ
Γ t1 : Πx : τ1 .τ2 Γ t2 : τ1
Γ t1 t2 : τ2 [t2 /x]
Γ, x : τ1 t : τ2 Γ Πx : τ1 .τ2 : ∗
Γ λx : τ1 .t : Πx : τ1 .τ2
c ∈ Cτ
Γc:τ
x:τ ∈Γ
Γx:τ
Γ t : τ τ =β τ Γt:τ
記法 8.1
• x ∈ F V (τ2 ) のとき, Πx : τ1 .τ2 を τ1 → τ2 と書く.
• x ∈ F V (κ) のとき, Πx : τ.κ を τ → κ と書く.
定義 8.5 (代入)
∗[t/x] = ∗
(Πx : τ.κ)[t/x] = Πx : τ [t/x].(κ[t/x])
b[t/x] = b
(Πx : τ1 .τ2 )[t/x] = Πx : τ1 [t/x].(τ2[t/x])
(τ t1 )[t/x] = (τ [t/x])(t1 [t/x])
c[t/x] = c
(λx : τ.t1 )[t/x] = λx : (τ [t/x]).(t1[t/x])
(t1 t2 )[t/x] = (t1 [t/x])(t2 [t/x])
定義 8.6 (簡約)
(λx : τ.t1 )t2 →β t1 [t2 /x]
例 8.6
(λy : nat.λx : (Πz : list(y).list(y)).x)0 →β λx : (Πz : list(0).list(0)).x
注意 8.1 この体系は, LF の体系とほぼ同じ. ただし, LF では, =β の代わりに =βη を考える.
例 8.7 list : nat → ∗ とし, list(n) が, 長さが n のリストの型とする.
• 定数の型
nil : list(0)
cons : Πn : nat.Πx : nat.Πy : list(n).list(n + 1)
40
• 上の記法を使うと下のように単純化できる
cons : Πn : nat.nat → list(n) → list(n + 1)
• 例: cons 0 3 nil : list(1)
例 8.8 型定数として nat : ∗, T : nat → ∗, 定数として 0 : nat, S : nat → nat, t : Π.x : nat.T (x)
を考える.
• 下の式の型の導出を示せ. また, 簡約せよ.
(λg : cnat.t(g 0 S))(λx : nat.λf : nat → nat.f(fx)) : T (S(S(0)))
ただし, cnat は, nat → (nat → nat) → nat を省略したものとする.
• 下の式の型の導出を示せ. また, 簡約せよ.
(λg : cnat.λx.T (g 0 S).x)(λx : nat.λf : nat → nat.f(fx))
例 8.9 (述語論理との対応)
• カインドを以下の形式に拡張する.
κ ::= Prop | Set | Πx : τ.κ
• τ : Set ならば, τ は値の型.
– 関数記号の型: b → . . . → b → b.
• τ : Prop ならば, τ は論理式に対応
– 述語記号のカインド: b → . . . → b → Prop.
例 8.10 nat : Set, P : nat → Prop とする. ∀x : nat.P (x) を下のラムダに対応させることがで
きる.
Πx : nat.P x : Prop
例 8.11 ∀x : nat.Q(x, y) ⇒ Q(t, y) をラムダ式で表現する. Q : nat → nat → Prop とする.
(Πx : nat.Q x y) → Q t y : Prop
証明
(λz : (Πx : nat.Qxy).zt) : (Πx : nat.Qxy) → Qty
8.3
CC (Calculus of Construction)
定義 8.7 (CC)
• 構文
型
s ::= Prop | Set
κ ::= s | Πx : τ.κ | Πx : κ.κ
τ ::= b | Πx : τ.τ | Πx : κ.τ | τ t | λx : τ.τ | λx : κ.τ | τ τ
項
t ::= x | λx : τ.t | λx : κ.t | tt | tτ
ソート
カインド
41
• 判定 Γ κ
Γ, x : τ κ
Γ Πx : τ.κ
Γs
Γ, x : κ1 κ2
Γ Πx : κ1 .κ2
• 判定 Γ τ : κ
Γ τ : Πx : τ .κ Γ t : τ Γ τ t : κ[t/x]
Γ, x : τ1 τ2 : s
Γ Πx : τ1 .τ2 : s
Γ, x : κ τ : s
Γ Πx : κ.τ : s
x:κ∈Γ
Γx:κ
b ∈ Tκ
Γb:κ
Γ τ : κ κ =β κ
Γτ :κ
• 判定 Γ t : τ
Γ, x : τ1 t : τ2 Γ Πx : τ1 .τ2 : s
Γ λx : τ1 .t : Πx : τ1 .τ2
Γ t1 : Πx : τ1 .τ2 Γ t2 : τ1
Γ t1 t2 : τ2 [t2 /x]
Γ, x : κ t : τ Γ Πx : κ.τ2 : s
Γ λx : κ.t : Πx : κ.τ
Γ t1 : Πx : κ.τ1 Γ τ2 : κ
Γ tτ2 : τ1 [τ2 /x]
c ∈ Cτ
Γc:τ
x:τ ∈Γ
Γx:τ
Γ t : τ τ =β τ Γt:τ
例 8.12
• Sysmte F
Λα.λx : α.x : ∀α.α → α
• CC
λy:Set.λx:y.x
: Πy:Set.Πz:y.y
: Πy:Set.y → y
注意: 型変数と変数を区別しない.
定義 8.8 (簡約 (reduction))
(λx : τ.t)s →β t[s/x]
(λx : κ.t)τ →β t[τ /x]
(λx : τ .τ )t →β τ [t/x]
(λx : κ.τ )τ →β τ [τ /x]
定理 8.1 (Church-Rosser) t →∗β t1 かつ t →∗β t2 ならば, あるラムダ式 s が存在して, t1 →∗β s
かつ t2 →∗β s.
定理 8.2 β 簡約は, 強正規化性を持つ.
42
• Γ t : τ ならば, t は強正規化性を持つ.
(t →β t1 →β t2 →β . . . となる無限列は存在しない.)
• Γ τ : κ ならば, τ は強正規化性を持つ.
• Γ κ ならば, κ は強正規化性を持つ.
定理 8.3 Γ t : τ が成り立つかは, 決定可能.
例 8.13 list : Set → nat → Set とし, list(x)(n) が, 要素の型 x, 長さが n のリストの型とする.
• 定数の型
nil : Πx : Set.list(x)(0)
cons : Πx : Set.Πn : nat.x → list(x)(n) → list(x)(n + 1)
• 例: cons nat 0 3 (nil nat) : list(nat)(1).
例 8.14 型定数として nat : Set,T : nat → Set, 定数として 0 : nat, S : nat → nat, t : Π.x :
nat.T (x) を考える.
• 下の式の型の導出を示せ. また, 簡約せよ.
(λg : cnat.t(g nat 0 S))(λy : Set.λx : y.λf : y → y.f(fx)) : T (S(S(0)))
ただし, cnat は, Πx : Set.x → (x → x) → x を省略したものとする.
• 下の式の型の導出を示せ. また, 簡約せよ.
(λg : cnat.λx.T (g nat 0 S).x)(λy : Set.λx : y.λf : y → y.f(fx))
例 8.15 R : nat → nat → Prop とする.
• 関係 R が対称的 ∀x : nat.∀y : nat.R(x, y) → R(y, x)
Sym(R) ≡ Πx : nat.Πy : nat.Rxy → Ryx
• 関係 R が推移的 ∀x : nat.∀y : nat.∀z : nat.R(x, y) → R(y, z) → R(x, z)
T rans(R) ≡ Πx : nat.Πy : nat.Πz.nat.Rxy → Ryz → Rxz
• 関係が R が対称的, 推移的, さらに Rxy ならば Rxx.
ΠR : nat → nat → Prop.Sym(R) → T rans(R) → Rxy → Rxx
証明
λR : nat → nat → Prop.λA : Sym(R).λB : T rans(R).λC : Rxy.BxyxC(AxyC)
例 8.16 R : nat → Prop を自然数上の集合と考える.
• A ⊆ B は以下のように定義できる.
Πx : nat.Ax → Bx
• (A ⊆ B) ⇒ (B ⊆ C) ⇒ (A ⊆ C) を型として定義せよ.
• 上の型を持つ式を見つけるることで, 上の性質を証明せよ.
43
Coq のインストール
8.4
例 8.17 (Coq のインストール)
• 下の URL から Coq をダウンロードしインストールする.
http://coq.inria.fr/distrib-eng.html
9
Coq
9.1
Coq による証明
定義 9.1 (Coq の文法)
CC
Coq
----------------------------------Πx : A.B
(x:A)B
λx : A.B
[x:A]B
A→B
A -> B
P ⇒Q
P -> Q
----------------------------------例 9.1
Coq < Section example1.
Coq < Variable P:Prop.
Coq < Lemma example1 : P -> ((P -> False) -> False).
1 subgoal
============================
P->(P->False)->False
example1 < Intro.
1 subgoal
導入規則で証明
H : P
============================
(P->False)->False
example1 < Intro H1.
1 subgoal
H1: 生成される仮定の名前
H : P
H1 : P->False
============================
False
44
example1 < Apply H1.
1 subgoal
仮定 H1 を適用
H : P
H1 : P->False
============================
P
example1 < Assumption.
Subtree proved!
example1 < Qed.
Intro.
仮定を用いて証明
証明の終わり
Intro H1.
Apply H1.
Assumption.
example1 is defined
• コマンド Print で完成した証明に対応するラムダ式を表示することができる.
Coq < Print example1.
example1 = [H:P; H0:(P->False)](H0 H)
: P->(P->False)->False
これは, λH : P.λH0 : (P → False).H0 H に対応している.
• セクションを閉じる. Variable で導入した仮定を無効にする.
Coq < End example1.
定義 9.2 (Intro) Π の導入規則による証明
• A → B を証明
AB
A→B
A を仮定して, B を証明.
• Πx : A.B すなわち, ∀x : A.B を証明
x:AB
Πx : A.B
x が A 型の変数であることを仮定して, B を証明.
定義 9.3 (Apply) Π の消去規則による証明
• 定理 (仮定)Πx : Set.B を使って, B[C/x] を証明.
Πx : Set.B
B[C/x]
注意: 高階単一化を用いる. B[C/x] と B の単一化で, C を決定.
45
• 定理 (仮定)A → B を使って, B を証明.
A→B A
B
新ゴール A.
例 9.2 下の定理を証明せよ.
Section example1’.
Variable A:Prop.
Variable B:Prop.
Variable C:Prop.
Lemma example1’ : (A -> B) -> (C -> A) -> (C -> B).
...
Qed.
End example1’.
例 9.3
Section example2.
Variable A:Set.
Variable P:A -> Prop.
Variable f:A -> A.
Lemma example2 : ((x:A)(P x)) -> (y:A)(P (f y)).
Intro.
Intro.
Apply H.
Qed.
End example2.
例 9.4 Apply の引き数として, 式を書くことができる.
Section example2’.
Variable A:Set.
Variable P:A -> Prop.
Variable f:A -> A.
Lemma example2’ : ((x:A)(P x)) -> (y:A)(P (f y)).
Intro.
Intro.
Apply (H (f y)).
Qed.
End example2’.
H:(x:A)(P x) かつ (f y):A なので, (H (f y)) は P (f y) 型を持つ.
例 9.5
Section example4.
Definition sym := [R:nat->nat->Prop](x,y:nat)(R x y) -> (R y x).
Definition trans := [R:nat->nat->Prop](x,y,z:nat)
46
(R x y) -> (R y z) -> (R x z).
Lemma example4: (R:nat->nat->Prop)(sym R) -> (trans R) ->
((x,y:nat)(R x y) -> (R x x)).
....
End example4.
Definition により, sym や trans を定義の右辺と同一視できる.
9.2
帰納的な型の定義
例 9.6 (帰納的データ型の定義)
Coq < Inductive nat : Set :=
nat is defined
nat_rect is defined
nat_ind is defined
O : nat | S : nat -> nat.
nat_rec is defined
Coq < Check nat_ind.
nat_ind
: (P:(nat->Prop))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)
Coq < Check nat_rec.
nat_rec
: (P:(nat->Set))(P O)->((n:nat)(P n)->(P (S n)))->(n:nat)(P n)
同時に ι 規則と呼ばれる書き換え規則が導入される.
nat_rec P f1 f2 O → ι f1
nat_rec P f1 f2 (S x) → ι f2 x (nat_rec f1 f2 x)
例 9.7 (再帰関数の定義)
Fixpoint plus [n:nat] : nat -> nat :=
[m:nat]Cases n of
O => m
| (S p) => (S (plus p m))
end.
例 9.8 乗算 mult を定義せよ.
Fixpoint mult [n:nat] : nat -> nat :=
....
定義 9.4 Elim n: n に関する帰納用による証明.
例 9.9
Lemma plusassoc: (x,y,z:nat)(plus x (plus y z)) = (plus (plus x y) z).
Intros.
Elim x.
Simpl.
47
Apply refl_equal.
Intros.
Simpl.
Rewrite H.
Apply refl_equal.
Qed.
• Simpl: β 及び帰納的関数定義 (ι 規則) を用いた書き換え.
• Rewrite H: 定理 (仮定)H を用いたゴールの書き換え.
• refl equal :
x = x
例 9.10 (自然数のリスト)
Inductive list : Set := nil : list | cons : nat -> list -> list.
Fixpoint app [l:list] : list -> list
:= [m:list]Cases l of
nil => m
| (cons a l1) => (cons a (app l1 m))
end.
Infix RIGHTA 7 "^" app.
以下の定理を証明せよ.
Lemma app_associative: (l,m,n : list)((l^m)^ n)=(l^(m^n)).
課題 9.1 リストの反転 rev を定義し, 下の定理を証明せよ.
Fixpoint rev [l:list] : list :=
...
Lemma revrev: (xs:list)((rev (rev xs)) = xs).
9.3
帰納的定義による論理記号の定義
定義 9.5
Inductive and [A,B:Prop] : Prop := conj : A -> B -> (and A B).
Inductive or [A,B:Prop] : Prop
:= or_introl : A -> (or A B)
| or_intror : B -> (or A B)
例 9.11 次の定理を証明せよ.
Lemma orexample: (P,Q:Prop)(or P Q) -> ((P -> Q) -> Q).
48
9.4
依存型
例 9.12 長さが n のリスト:nlist n.
• 型の定義
Inductive nlist : nat -> Set
:= niln : (nlist O)
| consn : (l:nat)nat -> (nlist l) -> (nlist (S l)).
• リストの連結の定義
Fixpoint napp [a,b:nat; l:(nlist a)] : (nlist b) -> (nlist (plus a b))
:= [m:(nlist b)]
<[d:nat](nlist (plus d b))> Cases l of
niln => m
| (consn c x l1) => (consn (plus c b) x (napp c b l1 m))
end.
9.5
その他の証明法
定義 9.6 (Assert) A → B を A → C と C → B から示す.
Lemma assertexample: (A:Prop;f:nat->nat;x,y:nat)A -> (A -> (x = y))
-> ((f x) = (f y)).
Intros.
Assert H1: x = y.
Apply H0.
Assumption.
Rewrite H1.
Apply refl_equal.
Qed.
Assert H1: x = y.
これは, H1 という名前で, 仮定 x = y を追加し, 証明すべきゴールとして x = y を追加する.
課題 9.2
• 式を以下のデータ型で定義する.
Inductive exp
:= NatExp :
| VarExp :
| AddExp :
: Set
nat -> exp
nat -> exp
exp -> exp -> exp.
• eval,fv を定義せよ.
Fixpoint eval [e:exp]:(nat->nat) -> nat :=
...
Fixpoint fv [e:exp]:(nat -> Prop)
...
49
• 次の定理を証明せよ.
Lemma fveval: (e:exp;env1,env2:nat->nat)
((x:nat)((fv e x) -> ((env1 x) = (env2 x)))) ->
((eval e env1) = (eval e env2)).
参考文献
[1] H. Barendregt and H. Geuvers.
Proof-assistants using dependents type systems.
In
A. Robinson and A. Voronkov eds., Handbook of Automated Reasoning, Vol. 2, chapter 18.
Elsevier, 2001.
[2] C.-L. Chang and R. C.-T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic
Press, 1973.
[3] J. H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving.
Harper & Row, Publishers, 1986.
[4] M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment
for higher order logic. Cambridge University Press, 1993.
[5] G. P. Huet. A uniﬁcation algorithm for typed λ-calculus. Theoretical Computer Science,
1(1), 1975.
[6] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL. 2002. LNCS 2283.
[7] L. C. Paulson. Isabelle: A Generic Theorem Prover. 1994. LNCS 828.
[8] F. Pfenning. Logical frameworks. In A. Robinson and A. Voronkov eds., Handbook of
Automated Reasoning, Vol. 2, chapter 17. Elsevier, 2001.
[9] A. Robinson and A. Voronkov eds. Handbook of Automated Reasoning. Elsevier, 2001.
[10] W. Snyder and J. Gallier. Higher-order uniﬁcation revisited: Complete sets of transformations. Journal of Symbolic Computation, 8(1), 1989.
[11] D. van Dalen. Logic and Structure, Third Edition. Springer-Verlag, 1991.
[12] 小野寛晰. 情報科学における論理. 日本評論社, 1994.
[13] 大堀淳. プログラミング言語の基礎理論. 共立出版, 1997.
[14] 有川節夫, 原口誠. 述語論理と論理プログラミング. オーム社, 1988.
[15] 龍田真. 型理論. 近代科学社, 1992.
[16] 林晋. 数理論理学. コロナ社, 1989.
50

Download Report