let@token ·×»»µ

計算機科学
様相論理
佐藤雅彦
京都大学情報学研究科
数学基礎論
神戸大学
2015 年 8 月 20 日
素朴
何故計算機科学
疑問
様相論理
使
?
素朴
何故計算機科学
計算機科学
疑問
様相論理
中心課題 「計算」
使
行為 解析．
?
素朴
何故計算機科学
疑問
様相論理
使
?
計算機科学 中心課題 「計算」
行為 解析．
=⇒
「時間」 「空間」 中 置
「対象」(
) 動的 振舞
解析
必要
．
素朴
何故計算機科学
疑問
様相論理
使
?
計算機科学 中心課題 「計算」
行為 解析．
=⇒
「時間」 「空間」 中 置
「対象」(
) 動的 振舞
解析
必要
．
解析
有用
道具
．
，「適度 抽象度」 持
Kripke
素朴
何故計算機科学
疑問
様相論理
使
?
計算機科学 中心課題 「計算」
行為 解析．
=⇒
「時間」 「空間」 中 置
「対象」(
) 動的 振舞
解析
必要
．
解析
有用
道具
．
，「適度 抽象度」 持
Kripke
Kripke
「意味論的枠組」 様相論理 言語
用
「証明論」
形式的，論理的 解析
．(健全性 完全性 要求
)
素朴
何故計算機科学
疑問
様相論理
使
?
計算機科学 中心課題 「計算」
行為 解析．
=⇒
「時間」 「空間」 中 置
「対象」(
) 動的 振舞
解析
必要
．
解析
有用
道具
．
，「適度 抽象度」 持
Kripke
Kripke
「意味論的枠組」 様相論理 言語
用
「証明論」
形式的，論理的 解析
．(健全性 完全性 要求
)
□
(implicit
) 変数 適切 有効範囲 (scope)
提供
．
本講演 目標
計算機科学
紹介
．
1
証明
様相論理 応用
関連
変数
関連
共有)
(Reflective Proof Theory)
様相
意味論 (referential transparency)
文脈計算 (Explicit Environment)
環境
変数
3
事例 通
様相
知識 論理 (知識 改訂，知識
証明支援系, 構成的
2
，以下
関連
多段階計算
安全性 (
様相
権限，情報流解析)
McCarthy
「不貞 妻達
知識
公理化
」 問題設定．
王国 ，100 万組 夫婦
40 人 妻 不貞
日 (1 日目
)，王様 以下 宣告
．
一人 不貞 妻
1
夫 ，他 夫
2
3
4
妻
5
，自分
首 刎
知
夫
推論
妻 不貞
．
夫 毎朝誰
．
妻 不貞
今日
毎夜，
，自分 妻 不貞
妻 首 刎
．
．
自分 知識 用
．
推論
，翌朝
見 ．
知識
McCarthy
公理化 (続)
主要 構成要素 ，
1
空間 (王国)
時間 経過 ，
伴
2
(
夫)
知識 変化
，
3
知識
帰結
首
刎
，
形式論理 用
理 用
考
．McCarthy
[McCarthy-S-Hayashi-Igarashi 1978]
様相演算子 与
，
満
理体系 与
．
行為
解析
．
様相論
形式的 記述
Hilbert 流 公
[S 1977] ，体系 Gentzen 流 ，sequent calculus
定式化
，対応
Kripke 意味論
，健全性，強完全性 証明
形式的 解答 与
．
McCarthy
知識
公理化 (続)
形式体系 言語
王国 夫妻 k 組
，
(i = 1, . . . , k) 表 ，[Si ]n P
知
」
命題 表
夫
「Si
P
．
命題定数 pi (i = 1, . . . , k) 用意 ，
「Si
」
命題 表
．
ideal
Si
n 日目
妻 不貞
Fool 導入 ，O 表 ．
，[O]n P 「
夫 n 日目 P
知
命題 表
．common knowledge 表現
McCarthy 秀逸 工夫
．
」
McCarthy
知識
記法
1
A := {p1 , . . . , pk }.
2
S := {S1 , . . . , Sk , O}.
3
S
O
Si
4
P
A, S 上
(様相) 命題 表
5
⟨S⟩n P := ¬[S]n ¬P .
6
{S}n P := [S]n P ∨ [S]n ¬P .
表
．
公理化 (続)
McCarthy
公理化
各様相演算子 ，S5
知識
公理 (
公理化 (続)
)
[S]n P → P .
[S]n (P → Q) → [S]n P → [S]n Q.
[S]n P → [S]n [S]n P .
¬[S]n P → [S]n ¬[S]n P .
推論規則
．
満
，更 以下 公理 (
[S]n P → [S]m P (n < m).
[O]n P → [O]n [S]n P .
)
設
McCarthy
知識
公理化 (続)
Kripke
W 空
(可能世界 ) 集合
⟨W ; r, v⟩ 以下 条件 定
，W 上
1
r : S × N+ → ℘(W × W ).
2
r
3
m < n =⇒ r(S, m) ⊇ r(S, n).
4
r(O, n) ⊇ r(S, n).
5
v : A × W → {⊤, ⊥}.
W 上 同値関係．
，
1
2
Kripke
．
対応
W :=
{+, −}k
，
− {(−, . . . , −)}
，w = (ε1 , . . . , εk )
対
定 ，
[w] := ∧ki=1 pεi i
置 ．
知識
McCarthy
王様 宣告
体系
表現
王様 宣告 ，
夫
要求
，言語行為
王様 宣告 ，
．
宣告
自己言及的
問題
内容 知
，「
．
，各夫
．
上 従
．
夫 共有
夫 知識 毎日拡大
common knowledge
common knowledge
必要
．
公理化 (続)
知識
common knowledge
拡大
」
関係 正確 記述
McCarthy
王様 宣告 適切 表現
．
1
知識
公理化 (続)
論理式 集合 Γ
次
P ∈Γ
1 日目 common knowledge
各 w 成立
．
Γ
2
存在
夫 Si
n 日目 知識全体
集合 Bw (i, n) Γ 用
4
Γ
Bw (i, n)
定義
用
「定義」 Γ
不完全．
[O]1 P
仮定．
3
Bw (i, n)
定
集合
用
生成
deductive
定義．
特徴付
，
論理式
．
，Γ
McCarthy
知識
公理化 (続)
k
Γ = ∨ pi ∪ {{Si }1 pj | j ̸= i} ∪
i=1
{[w] → [O]n+1 [Si ]n pi | Bw (i, n) ⊢ pi } ∪
{[w] → [O]n+1 ¬[Si ]n pi | Bw (i, n) ̸⊢ pi } ∪
{[w] → [Si ]n P | Bw (i, n) ⊢ P }
w
Bw (i, 1) = [O]1 Γ ∪ {pj j | j ̸= i}
(1)
(2)
Bw (i, n + 1) =
Bw (i, n) ∪ {[Sj ]n pj | Bw (j, n) ⊢ pj } ∪
{¬[Sj ]n pj | Bw (j, n) ̸⊢ pj }
(1), (2), (3) 未知数 Γ, Bw (i, n) (i = 1, . . . , k, n ∈ N+ )
関
無限個 連立方程式系 見
．
(3)
McCarthy
知識
公理化 (続)
Theorem
方程式系 (1),(2),(3) 対
Γ
Bw (i, n) 唯一存在
．
無矛盾
解 Γ,
Theorem
上 解 Bw (i, n)
対応
，
P
Bw (i, n) ⊢ P ⇐⇒ w |= [Si ]n P
Kripke
一意的
定
．
，
McCarthy
前記
Kripke
知識
以下
公理化 (続)
定
．
W := {+, −}k − {(−, . . . , −)}.
(w, w′ ) ∈ r(i, n) ⇐⇒ w = w′
ei
n < max{||w||, ||w′ ||}.
含
r(O, n) := r(Si , n)
w ⊕ w′ =
最小 同値関係.
v(pi , (ε1 , . . . , εk )) = ⊤ ⇐⇒ εi = +.
以下 成立
．
1
wi = +
w |= [Si ]n pi ⇐⇒ ||w|| ≥ n.
2
wi = −
w |= [Si ]n ¬pi ⇐⇒ ||w|| > n.
Reflective Proof Theory
Aczel
定義 ，
1991]．
構造 「証明」 対象
追加
構造
上 自己反映的 証明 理論 (RPT) 展開
[S
構造 ，命題 (propositions)
題 (truths) 型 無 λ計算
一部
内部 実現
Aczel
，
「算術 基本法則
(Grundgesetze der Arithmetics)」集合 概念 外延
義
失敗
試
修復
．
RPT
対象
象 持
以下
RPT
構造 ，証明 対象
RPT 内部 言及
．
概略 紹介
．
真命
．
定
追加 ，更
構文的対
構成
RPT
，対 構成子 他 論理記号，等号，自然数等 定数
持 λ-計算
， Λ=
項
．
Λ
Λ= 対象 a, b 等
a=b 書 ．
Eq(a, b)
表 ，RPT
Λ= 上 ，自然数 i
2 項関係 Provesi (p, a)
1 項関係 Propi (a)
相互再帰的 定義
．
上
内部
関係 ，RPT
2
書
，|=i a
p ⊢i a
．
Λ= 関数適用
書 ．
App(f, a)
a = b, |=i a, p ⊢i a, f (a) 等
時 Λ= 対象 表 ．
表 ，RPT
RPT
f (a)
項
，同
特徴
RPT
1
RPT 扱 対象 ，
題 証明 含
．
2
RPT
与
3
意味論
4
形式的体系
．
，命題
，
中
命
証明 意味 意味論的
Martin-Löf 流 直観主義的意味論
与
，
，古典論理 上
集合論的意味論 与
．
，不完全性定理
RPT
，実用的 十分 形式化
5
全称量化，特称量化
6
証明 ，Curry-Howard
7
有限 対象
「
i
「⊢i a」
命題 a
Church
方法
同型 用
証明可能
i + 1 命題
完全 形式化
．
λ-項
表現
．
λ-項
表現
．
」
命題 ，
．
命題
Λ= 上
階層化
関係 Propi (a)
：
証明
階層
Provesi (p, a)
i
1
i<j
，Propi (a) =⇒ Propj (a).
2
i<j
，Provesi (p, a) =⇒ Provesj (p, a).
上
，RPT
以下
internalize
．
1
⊢ω ∀i, j. i, j ∈ N → i<j →|=i a →|=j a.
2
⊢ω ∀i, j, p. i, j ∈ N → i<j → p ⊢i a → p ⊢j a.
3
⊢ω ∀i, j. i, j ∈ N → i<j →⊢i a →⊢j a.
∃p. p ⊢i a
Remark. 項目 3
⊢i a
子
．⊢j , ⊢ω 同様．
略記
，様相演算
集合
RPT
RPT
集合 階層化
定義
，関連
記法 以下
．a
定
i 集合
．
σi (a) := ∀x. |=i a(x).
{x | A} := λx. A.
b ∈i a := σi (a) ∧ a(b).
，以下
RPT
成立
．
⊢i+1 ∀a. σi (a) → σi+1 (a).
⊢i+2 ∀a, x. σi (a) → x ∈i a ↔ x ∈i+1 a.
(Predication) ⊢i+1 ∀a, b. σi (a) →|=i b ∈i a.
(Comprehension) ⊢i+1 ∀a, x. σi (a) → x ∈i a ↔ a(x).
集合 (続)
RPT
V := {x | x = x}
成立
．
Russel set Ri
，⊢1 σ0 (V )
Ri := {x | x ̸∈i x}
Ri ∈i Ri ⇐⇒ σi (Ri )
．
，
⊢1 V ∈0 V
，
Ri (Ri )
σi (Ri )
，
Ri ∈i Ri ⇐⇒ Ri (Ri ) ⇐⇒ Ri ̸∈i Ri
値性
矛盾 得
．故 ¬σi (Ri )
．
，Ri ̸∈i Ri
．
議論 形式化
⊢i+1 Ri ̸∈i Ri
得
．
，上 同
指示透明性
命題 P
中
，代入原理
項a
出現 注目
P (a)
書 ．
P (a) a = b
P (b)
成 立
1961].
，文脈 P ( )
文脈 L( ) :=「( )
「明
明星」
右 成立
．
指示透明性 持
[Quine
生命 存在
」 ，a :=「宵 明星」
，b :=
．
，以下 左 推論 成立
，
L(a) → L(a) a = b
L(a) → L(b)
□(L(a) → L(a)) a = b
□(L(a) → L(b))
文脈 L(a) → L( ) 指示透明性 持
□(L(a) → L( )) 指示透明性 持
，様相的文脈
(referentially opaque).
言語
指示透明性
指示透明性 分析哲学由来 概念
性質 検証
概念
．
，計算機科学
等価変換 研究 有用
一般 ，変数
持
許 言語 指示透明性
値
代入 (assignment)
．文脈
x := x + 1; ( )
関
，以下
見
代入原理 成立
(x := x + 1; x) = (x := x + 1; x) x = 0
(x := x + 1; x) = (x := x + 1; 0)
．
代入
許
指示透明
言語
[S 1994]
RPT λ-計算 拡張 ，代入命令 持
透明 関数型言語 与
．
簡単 ，代入命令 常 代入
変数
let 文 有効範囲 中 出現
言語 文法 設計
指示
．
let x = 0(x := x + 1; x) = let x = 0(x := x + 1; x) x = 0
let x = 0(x := x + 1; x) = let x = 0(x := x + 1; x)
上 let 文中 x 束縛変数
x = 0 自由変数 x
無関係
．
，上 推論 2 目 前提
，代入原理 成立
環境
見
中心的
象
者
持 単純型付文脈計算
，「文脈」C( ) 参照透明性 概念
位置 占
．
，文脈自身 ，考察 対
言語 考察
存在
．
let 文 意味 考察
時的 保持
値 組 有限集合
．
，局所的 変数
一
「環境」 概念 重要
[S-Sakurai-Burstall 2001]，[S-Sakurai-Kameyama 2002]
環境
文脈 言語 一級 構成要素
型付 λ-計算 提案
，
参照透明性 持
示
．
λκϵ : 環境 持 単純型付文脈計算
[Sato-Sakurai-Kameyama 2002]
型 定義
体系 λκϵ
概要．
A, B, C ::= K | E | A → B | AE
K ::= atomic types
E ::= {xA , . . . , z C }
E = {xA , . . . , z C } 環境 型 ，変数 xA 等 名前 一部
型 持 ．AE 文脈 型．
Remark. AE [E]A 書
，文脈 型 様相命題
，Curry-Howard
．
同型
λκϵ : 環境 持 単純型付文脈計算
型付 規則
xA : A
b:B
→I
λxA . b : A → B
axiom
b:A→B a:A
→E
b(a) : B
a:A
文脈 I
κ{x, . . . , z}. a : A{x,...,z}
a : A ···
{a/xA , . . . , c/z C }
a : AE e : E
文脈 E
a·e:A
c:C
環境 I
: {xA , . . . , z C }
e : E a : AE
環境 E
e[[a]] : A
多段階計算
多段階計算 (staged computaion) 部分評価 (partial evaluation)
発展形
．
扱 ，
変形 段階 分
計
算
．
異
段階 間 関係 Kripke
対応
，
型付 様相論理 時相論理 設計
．
異 段階
変数 考
，
変数 形式化
．
参考文献
[McCarthy-S-Hayashi-Igarashi 1978] John, McCarthy, Masahiko
Sato, Takeshi Hayashi and Shigeru Igarashi, On the Model Theory
of Knowledge, Stanford Artificial Intelligence Laboratory, AIM-312,
1978.
http://i.stanford.edu/pub/cstr/reports/cs/tr/78/657/
CS-TR-78-657.pdf
[Quine 1961] Quine, W.V., Reference and Modality, In
W.V. Quine, From a Logical Point of View, second edition,
130-138. Harvard University Press.
[S 1977] A study of Kripke-type models for some modal logics by
Gentzen’s sequential method, Publ. RIMS, Kyoto U., 13, 381-468.
https://www.jstage.jst.go.jp/article/kyotoms1969/13/2/
13 2 381/ pdf
参考文献
[S 1991] Masahiko Sato, Adding Proof Objects and Inductive
Definition Mechanisms to Frege Structures, 1991, in T. Ito, A.R.
Meyer eds., Theoretical Aspects of Computer Science,
International Conference TACS’91 Proceedings, Lecture Notes in
Computer Sciecne 526, 53-87.
[S 1994] Masahiko Sato, A Purely Functional Lnaguage with
Encapsulated Assignment, 1994, in M. Hagiya, J.C. Mitchell eds.,
Theoretical Aspects of Computer Software, International
Symposium TACS’94 Proceedings, Lecture Noter in Computer
Science 789, 179-202.
[S-Sakurai-Burstall 2001] Masahiko Sato, Takafumi Sakuai, Rod
Burstall, Explicit Environments Fundamenta Informaticae vol. 45,
79–115, 2001.
[S-Sakurai-Kameyama 2002] Masahiko Sato, Takafumi Sakurai,
Yukiyoshi Kameyama, A Simply Typed Context Calculus with
First-Class Environments, Journal of Functional and Logic
Programming, Vol. 2002, No. 4, March 2002.