論理関係は(型環境について)単調

お勉強

ATTAPL続き．

論理関係とは

論理関係は λ計算の項の間の2項関係で, 型でインデックスがついている(つまり型を含めれば3項関係).
論理関係は「論理的」な関係である(Curry-Howard的な意味で).
すなわち，論理関係とは R(s1, t1, T1->T2) かつ R(s2, t2, T1) ならば R(s1 s2, t1 t2, T2) であるような関係．
追記．logical relation という名前については，id:sumiiさんのLogical relationはなぜlogicalなのか 参照．

なぜ論理関係？

そもそもなぜ 論理関係が必要か．

λ計算の項の等価関係は ≡ を導出する規則で定義される最大の関係だが，これはあくまで数学的な定義なので，項の等価性を判定するアルゴリズムをが必要． このアルゴリズムは 健全であることはもちろん 完全でなければならない．

健全性の証明はわりと普通らしい．が，項の等価性を導出するアルゴリズム(s⇔t : T) の完全性(つまり，s≡t:Tならばs⇔t : T)の証明は直接的には難しい． アルゴリズムが作る関係は「論理的」でないため，らしい．そこで証明テクニックとして，論理的な「論理関係」を間にはさんで証明する．

ある論理関係 R(_, _, _) をつくって

  1. R(s, t, T) ならば，アルゴリズムで2項が等価と判定される (s⇔t : T)
  2. s≡t : T ならば， R(s, t, T)

という流れで証明する．

論理関係と単調性

ここで型環境については言及しなかったが，openな項を扱うためには型環境も必要になる．
論理関係の例として，次の(型環境を含む)関係 Γ |- s is t : T という 4項関係を考える．

どのような関係かは本文を参照するとして，本文では， この関係は (型環境について) 単調でなければならないと書いてある．
単調とは，型環境の拡大について単調ということだ．型環境が広がっても，項は関連づけられなければならない，すなわち Γ |- s is t : T かつ Γ ⊆ Γ' ならば Γ' |- s is t : T でなければならない．

でないと完全性の証明の (1) で失敗する.

これを示すため，完全性の証明について考える．型の構造に関する帰納法を使う．
いきなりinduction step だが T=T1->T2 の場合を考える．Γ |- s is t : T1 -> T2 ならば Γ |- s⇔t:T1->T2 を示す．

  • Γ |- s⇔t:T1->T2 と アルゴリズムの (QAT-ARROW) より，Γ,x:T |- s x ⇔ t x : T2 が示せればよい
  • これを示すには，帰納法の仮定より Γ,x:T |- s x is t x : T2 を示せばよい
  • _ |- _ is _ : _ は論理関係なので 論理関係の定義より Γ,x:T |- x is x : T1 かつ Γ,x:T |- s is t : T1 -> T2 が示せればよい

ここで単調性が必要, つまり 前提となる Γ |- s is t : T1 -> T2 から Γ,x:T |- s is t : T1 -> T2 が導けなければならない．

単調性をもたない論理関係の例

テキトーに論理関係をつくると 単調性をもたないものができてしまう(p.236)．

(p.234) Γ |- s is t : T1 -> T2 if forall s', t', if Γ |- s' is t' : T1 then Γ |- s s' is t t' : T2 のようにすると，単調性の証明に失敗する．


単調性の証明を試す．例によって 型の構造に関する帰納法．
induction step, T=T1->T2 の場合で， Γ |- s is t : T1 -> T2 ならば Γ,x:T |- s is t : T1 -> T2 を示そうとしてみる．

  • 定義より, Γ,x:t |- s' is t' : T1 ならば Γ,x:t |- s s' is t t' : T2 がいえればよい
  • ここで帰納法の仮定より単調性があるから Γ |- s s' is t t' : T2 がいえればよい
  • がしかし これを示すには Γ |- s' is t' : T1 を示さねばならないが， s' か t' が xを含む場合にこれは成り立たない．

これを防ぐため， s', t' が動ける範囲を拡大し， Γ |- s is t : T1 -> T2 if forall s', t', if Γ ⊆ Γ' and Γ' |- s' is t' : T1 then Γ |- s s' is t t' : T2 のようにする(6.7.1)．

雑感

分かったような，分からんような． おそらく単調性云々の前に 論理関係がなぜ必要かについていまいち納得してないのがまずいんだろう．