Software Engineering Lecture s03

Lambda Calculus and Natural Deduction

今回の参考文献は、Proofs and Types, Jean-Yves Girard, Yves Lafont, Paul Taylor です。

Lambda Calculus

Natural Deduction

Natural Deduction は Gentzen によって作られた論理と、その証明システム。ここでは、論理式の記号として命題変数と ∧(かつ)と->(ならば)と∀x(すべてのx)だけを使う。他にも¬(否定)や∨(または)や⊥(矛盾)や∀x(すべてのx)∃x(あるx)があるが、ここでは扱わない。

論理式は推論によって作られたり分解されたりする。これが証明である。

      :
      A

は、さまざまな推論によって A が証明されたことを示す。証明は木構造を持ち根が証明された論理式で、証明の葉は仮定である。仮定である葉には dead と alive の二つの状態がある。

A という仮定から推論して B という論理式が得られたとする。

     A
     :
     B

A は alive 生きている仮定である。

 ->I という推論規則によって、->を導入する。
     A
     :
     B
 -------------
   A -> B

線の上の証明があれば、 A -> B は真である。ここで、A は、この論理式に含まれている。この仮定は解消(discharge)されたので死んで、dead になる。それを [A] と書く。

    [A]
     :
     B
 ---------- ->I
   A -> B

すべての仮定が discharge されれれば、証明された式は仮定無しで真な論理式となる。どの推論により、どの仮定が解消されたかの対応付けを番号で行うと良い。

残りの推論規則は、以下の通り。

Introduction 導入

 
                       [A]
   :      :             :             
   A      B             B            
 ------------- ∧I    ------- ->I     
    A ∧ B              A->B

Elimnation 除去

     :                :             :        :      
   A ∧ B            A ∧ B           A      A -> B      
  ------- ∧1E      ------- ∧2E    --------------- ->E 
     A                B                 B

ここで、A[t/x] は A の中の x を、これまでに現れてない別な記号 t で置き換えたもの。

問題 4.1

Excercise 4.1 以下の論理式を Natural Dection の証明図を使って証明せよ。

   (1)  A -> A
   (2)  A -> (B -> A)
   (3)  (A ∧ (A -> B)) -> B
   (4)  B -> (B ∧ (A -> B))

Lambda Calculus

ここでは、Haskell の式をそのまま使う。

Types

1. a,b,c などは型である。Haskell の Integer や Char も型である。

2. U,V が型なら U -> V も型である。(関数)

3. U,V が型なら (U , V) も型である。(Pair、直積)

ここでは、これらによって作られる型のみを考える。

Term

Term は以下の規則によって型と一緒に構築される。

1. Haskell の変数 x,y,z は項。つまり let a = ... で宣言された小文字で始まる記号。対応する型(変数で指定された)を持つ。

    1 や 'a' も対応する型を持つ項である。

2. u が型U、v が型V を持てば、(u,v) は型(U,V)を持つ項である。

3. 型(U,V)を持つ項 t に対して、fst t は型U を持つ項、snd t は型 V を持つ項である。

4. v が型V を持つ項で、x0,x1,...,xn が型Uを持てば、 \x0 x1 ..., xn -> v は項である。

    Haskell によって変数の名前のスコープは適切に扱われるとする。

5. t が型 U->V を持ち、u が型U を持てば、 t u は型V を持つ項である。

これら項は、Haskell によって評価される。これらは変換規則と提供する。

1. 変数は変数の値

2. (u,v) は pair

3. fst と snd は pair の最初と次を取ってくる関数

4. lambda 式は、与えられた引数により変数の置き換えを行う

5. 関数の適用を行う。

等式

    fst (x,y) == x
    snd (x,y) == y
    (\x y -> v) u == v

さらに

   ((fst v),(snd v))==v
   (\x t x) = t

正則形 (Normal form)

Haskell の計算は、これらの項をなるべく簡単に変換していくもの。

    fst (u,v)
    snd (u,v)
    (\x -> v) u

のような形が式に含まれていなければ、式はこれ以上計算できない。

逆に含まれていれば、次のように変換できる。

    fst (u,v)       -> u
    snd (u,v)       -> v
    (\x -> v) u     -> v[u/x]   (v の中のxをuで置き換える)

置き換えによって、さらに計算が進む場合もある。

問題4.2

Excercise 4.2 以下の式を計算せよ

    (\x -> (snd x,fst x))  (1,2)

以下の式は Haskkel がエラーを出す。

    (\x -> (snd x,fst x))  ((\x -> t 3 ),2)

適切に実行されるように t に関する修正を加えよ。

Curry Howard 対応

さて、長い道のりだけど、あと少し。

Natural Dection の推論には、Lambda 式が対応する。

仮定 A は大域変数v。

                    
   :      :        
   A      B       
 ------------- ∧I
    A ∧ B

これは、u, v から (u,v) という項作る操作。

      [A]
       :             
       B            
    ------- ->I     
     A -> B

これは、変数 v を含む式Bから、(\v -> u) を作る操作。v は局所変数となる。

     :                :         
   A ∧ B            A ∧ B        
  ------- ∧1E      ------- ∧2E  
     A                B

これは、v から fst v, snd v を行う操作。

     :        :      
     A      A -> B      
    --------------- ->E 
          B

(\x v) u に対応する。

問題 4.3

Excercise 4.3 以下の論理式の証明図に対応する Lambda 式を作れ。

   (1)  A -> A
   (2)  A -> (B -> A)
   (3)  (A ∧ (A -> B)) -> B
   (4)  B -> (B ∧ (A -> B))

作成した Lambda 式の型が、上の式に一致するはずである。

Curry Howard 対応を使った証明支援系

証明したい論理式が与えられた時に、それを Haskell の型で表す。

その型を生成する Lambda 式を作成する。

すると、その Lambda 式が証明に対応している。

Sum

排他的論理和 disjunctin とも呼ばれる。

     :                :         
     A                B        
  ------- ∨1I      ------- ∧∨I  
   A ∨ B            A ∨ B

は良いが、

    A ∨ B       
 ------------- ∨E-bad
   A      B

とは、残念ながらならない。帰結は一つにするルールだった。

              [A]      [B]  
               :        :
    A ∨ B      C        C
 ------------------------------ ∨E
              C

とすると良い。これは、Haskell の case of に相当する。

    data Sum a  = Left a | Right a
    case x of
         Left  a -> a
       ; Right a -> a
    Prelude> :t ( \x -> case x of   Right y -> y  ;  Left z -> z  )

これに相当するλ式の記法は、

     ∨1I   ι1
     ∨2I   ι2
     ∨E    δ x.u y.v t

それぞれ、

      ι1              : A -> A ∨ B
      ι2              : B -> A ∨ B
      δ x.u y.v t     : (A -> C) -> (B -> C) -> (A ∨ B) -> C

という型を持つ。そして、その型の証明図を生成している。

問題 4.4

Excercise 4.4 以下の論理式の証明図に対応する Lambda 式を作れ。

   (1)  A -> A ∨ B  
   (2)  B -> A ∨ B  
   (3)  A ∨ A  -> A
   (4)  (A -> B) ∨ (A -> C)  -> A -> ( B ∨ C )