ソフトウェア基礎科学授業資料: 論理関係(logical relations)のお話 2006/1/13 住井英二郎復習: 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> 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). 多相関数のパラメタ性 (Parametricity) 無限ループや副作用等がなければ、  .型の関数はすべてidと等価  ..型の関数はすべてfirst と等価  ..型の関数はすべて secondと等価  ..型の関数は存在しない  .int型の関数は存在しない etc. どうやって証明するのか？「型に関する帰納法」の一種を利用論理関係 (logical relations): 型を受け取って、型の式の組 (e1, ..., en)の集合を返す写像で、「型に従って」定義されたもの – n = 1でもよい ⇒ 関係(relation)というより述語(predicate) パラメタ性を証明するための論理関係(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) } パラメタ性を証明するための論理関係(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() } 基本定理 (Fundamental Theorem） ├ v :  ならば vP() 証明の方針： ├ e :  の場合に一般化して、 ├ e :  の導出に関する帰納法を用いる使い方の例1 型.の値はすべて恒等関数（無限ループや副作用等がなければ） ├ v : . ならば、基本定理より vP(.) よって任意の├ v1 : ' について、 r = {v1} とおくと vPr() よって v v1 * v2 ならば v2r すなわち v2 = v1 使い方の例2 型.intの関数は存在しない（無限ループや副作用等がなければ） ├ v : .int ならば、基本定理より vP(.int) よって r =  とおくと vPr(int) よって適当な整数を v1 とすると v v1 * v2 ならば v2r となるがそれはありえないパラメタ性以外への論理関係の応用  停止性の証明  等価性の証明 – 秘密性の証明: f(x)がxを完全に秘密にする  任意のv, v'についてf(v)とf(v')が等価  抽象型, 暗号化, 情報流解析, etc. 停止性主張：再帰関数や再帰型等がプリミティブとして導入されていない型付き計算では、 ├ e :  ならば e * v なる v が存在停止性を証明するための論理関係簡単のために単純型についてのみ説明  ::= 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) } 基本定理 ├ e :  ならば eT() 証明の方針：下のように一般化し、型導出についての帰納法で示す x1 : 1, ..., xn : n├ e :  ならば任意の e1T(1), ..., enT(n) について [e1,...,en/x1,...,xn]eT() 等価性を証明するための論理関係（単純型の場合） 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) } 基本定理 ├ 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() 系 (e1, e2)R() ならば、任意の├ e :   bool について e e1 * true  e e2 * true 理由：基本定理より(e, e)R(  bool)だから。つまり、 e1とe2はどんな関数eについても同値