ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話

Presentation on theme: "ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話"— Presentation transcript:

1 ソフトウェア基礎科学 授業資料: 論理関係(logical relations)のお話
2006/1/13 住井 英二郎

2 復習: MLの多相関数 # let id x = x ;; val id : 'a -> 'a = <fun>
# let first x y = x ;; val first : 'a -> 'b -> 'a = <fun> # let second x y = y ;; val second : 'a -> 'b -> 'b = <fun>

3 MLの多相関数: その2 # let rec f x = f x ;; val f : 'a -> 'b = <fun>
# let rec g x = g (x + 1) ;; val g : int -> 'a = <fun> # let rec h x = assert false ;; val h : 'a -> 'b = <fun> # h 123 ;; Exception: Assert_failure ("", 2, -7).

4 多相関数のパラメタ性(Parametricity)
無限ループや副作用等がなければ、 .型の関数はすべてidと等価 ..型の関数はすべてfirstと等価 ..型の関数はすべてsecondと等価 ..型の関数は存在しない .int型の関数は存在しない etc.

5 どうやって証明するのか？ 「型に関する帰納法」の一種を利用
論理関係 (logical relations): 型を受け取って、型の式の組 (e1, ..., en)の集合を返す写像で、 「型に従って」定義されたもの n = 1でもよい ⇒ 関係(relation)というより述語(predicate)

6 パラメタ性を証明するための 論理関係(1/2)
型を受け取って、型の値の集合を返す 写像Pを、以下のように定義 ただしは型変数から値の集合への写像（後述） P(bool) = { true, false } P(int) = すべての整数の集合 一般に任意の基本型bについて、 P(b) = 型bを持つすべての値の集合 P(1  2) = { v | ├ v : 1  2 かつ 任意の v1P(1) について、 v v1 * v2 ならば v2P(2) }

7 パラメタ性を証明するための 論理関係(2/2)
P(1  2) = { (v1, v2) | v1P(1) かつ v2P(2) } P(1 + 2) = { InL(v1) | v1P(1) } ∪ { InR(v2 ) | v2P(2) } P() = () P(. ) = { v | ├ v : .  かつ 任意の閉じた型'と '型の値の任意の集合rについて、 vP,r() }

8 基本定理 (Fundamental Theorem）
├ v :  ならば vP() 証明の方針： ├ e :  の場合に一般化して、 ├ e :  の導出に関する帰納法を用いる

9 型.の値はすべて恒等関数 （無限ループや副作用等がなければ）
使い方の例1 型.の値はすべて恒等関数 （無限ループや副作用等がなければ） ├ v : . ならば、 基本定理より vP(.) よって任意の├ v1 : ' について、 r = {v1} とおくと vPr() よって v v1 * v2 ならば v2r すなわち v2 = v1

10 型.intの関数は存在しない （無限ループや副作用等がなければ）
使い方の例2 型.intの関数は存在しない （無限ループや副作用等がなければ） ├ v : .int ならば、 基本定理より vP(.int) よって r =  とおくと vPr(int) よって適当な整数を v1 とすると v v1 * v2 ならば v2r となるが それはありえない

11 パラメタ性以外への 論理関係の応用 停止性の証明 等価性の証明
秘密性の証明: f(x)がxを完全に秘密にする  任意のv, v'についてf(v)とf(v')が等価 抽象型, 暗号化, 情報流解析, etc.

12 停止性 主張： 再帰関数や再帰型等がプリミティブとして導入されていない型付き計算では、 ├ e :  ならば e * v なる v が存在

13 停止性を証明するための論理関係 簡単のために単純型についてのみ説明  ::= b | 1  2
T(b) = { e | ├ e : b かつ e * v なる v が存在 } T(1  2) = { e | ├ e : 1  2 かつ e * v なる v が存在、かつ 任意の e1T(1) について e e1T(2) }

14 基本定理 ├ e :  ならば eT() 証明の方針：下のように一般化し、 型導出についての帰納法で示す x1 : 1, ..., xn : n├ e :  ならば 任意の e1T(1), ..., enT(n) について [e1,...,en/x1,...,xn]eT()

15 等価性を証明するための論理関係 （単純型の場合）
R(b) = { (e, e') | ├ e : b かつ ├ e' : b かつ 任意のvについて e * v  e' * v } R(1  2) = { (e, e') | ├ e : 1  2 かつ ├ e' : 1  2 かつ 任意の(e1, e1')R(1)について (e e1, e' e1')R(2) }

16 ├ e :  ならば (e, e)R() 基本定理
証明の方針：一般化して型導出について帰納法 x1 : 1, ..., xn : n├ e :  ならば 任意の(e1,e1')T(1),...,(en,en')T(n)について ([e1,...,en/x1,...,xn]e, ([e1',...,en'/x1,...,xn]e)T()

17 系 (e1, e2)R() ならば、 任意の├ e :   bool について e e1 * true  e e2 * true 理由：基本定理より(e, e)R(  bool)だから。 つまり、 e1とe2はどんな関数eについても同値