型付きλ計算とHaskell

Haskell を動かしながら、型付きλ計算を理解しよう。

項の構築

primitive data type がいくつかあり、それは項(term)である。

    1
    'a'

次に、変数を導入する。変数は項である。変数には primitive data が入る。例えば整数とか、例えば文字列とか。あるいは、任意の項とか。

    x = 'a'

(Haskell では let x = 'a' を使う)

次にλ式を導入する。変数 x を含む(あるいは含まない)項 R x があった時に、 \ x -> R x は項である。項なので変数に代入することができる。

　　id = \ x -> x

\x -> R x は入力を一つ受け取る関数である。関数を作る方法はここまでではこれしかない。

ある項からλ項を作るのは、項の変換になる。これを以下のように横線を使って書く。この作り方を→Iと名付ける。I は introduction である。

  　　R  x
 ------------------   →I
    \ x -> R x

関数fを呼び出すには、関数の項に後ろに引数となる項xを書く。

f x

ここまでで、項は、primitive data type と変数とλ式しかない。これらを組み合わせたものが項になる。

α変換

λ式 \ x -> R x に引数 'a' を渡すと、後ろの項の x を、その値で置き換えた R 'a' を返す。これをα変換という。あるいは、λ式の関数適用である。これが、λ式の意味だと思っても良い。(操作的意味)

これは二つの項から一つの項を作る、つまり、項を減らす操作になる。これを以下のように書く。この作り方を→Eと名付ける。E は Elimination である。

    ( \ x -> R x )   y
 --------------------------- -→E
         R y

ここで R x は変数xを含む、あるいは含まない任意の項である。あるいは、その項を表すメタ変数である。

    id '1'

を Haskell で実行してみよう。また、

   ( \ x -> x ) '1'

を実行してみよう。

型の構築

型は、λ計算の整合性を保証するために必要となる。まず、primive な data 型がある。ある値が型を持つことを :: で表す。

    'a' :: Char

二つの型 a b があった時に、a を入力として b を返す関数の型を、

    a -> b

と書く。二つの入力 a と b があって、型 c を返す場合は、

    a -> b -> c

と書く。

    a -> ( b -> c )

これは、a を受けとって、b -> c という関数を返す関数である。

    ( a -> b ) -> c

これは、関数を受けとって、c という型を返す関数である。この関数の入力は一つである。

型 a を持つ項 x を含む型 b を持つ項 R x : b に対して、λ式を作ると、a -> b が作られる。

           b
 -----------------------------------   →I
         a -> b

a -> b は関数で、これに型 a の値を引数として与えると、

         a -> b      a
 -----------------------------------   →E
           b

となる。これは→の導入と削除になっている。

型と項は同時に操作される

この操作は、型と値と両方同時に起きている。つまり、

    x : a  と      r x : b

から、

     \ x -> r x  : a -> b

が作られる。あるいは、

     \ x -> r x  : a -> b と y : a

から、

     r y : b

が作られる。

id : a -> a という型を持つ項を作りたいとする。その項をλ項として構築するのを以下のように記述する。

    id : a -> a
    id = \x -> x

これは Haskell のプログラムそのものである。

論理式としての型

型 a を命題変数だと思う。

     a -> b

は「a ならば b 」である。

b が成立していれば、

    a -> b

が常に正しい。つまり、

           b
 -----------------------------------   →I
         a -> b

また、a -> b が常に正しくて、a が正しければ b が成立する。

         a -> b      a
 -----------------------------------   →E
           b

ここまでの範囲で、λ計算の型と論理式のとが対応していることがわかる。この変換はλ項の構築に対応しているので、論理式の証明がλ項の対応することになる。

　　論理式 ⇔ 型　　証明 ⇔ λ項

しかし、∧とかが出てこない。この対応を維持したまた、論理を拡張できるのかというのが問題になる。

直積

∧ は型を二つとる二項演算子である。a と b が型なら、 a ∧ b も型になる。

       a          b
 -----------------------------------   ∧I
         a  ∧  b

もし、a ∧ b が正しければ、 a は正しい

         a  ∧  b
 -----------------------------------   ∧E1
            a

b の方もある。

         a  ∧  b
 -----------------------------------   ∧E1
            b

この∧I, ∧E1, ∧E1 に相当するλ項を新しく導入したい

p1 : a, p2 : b があった時に、

      p1 × p2 :  a  ∧  b

となって欲しい。そして、p : a ∧ b があった時に、

     π1 p : a
     π2 p : b

となって欲しい。× と π1 と π2 が新しく導入する項になる。この項に対応する操作を定義する。

     p1 : a       p2 : b
 -----------------------------------   ∧I
       p1 × p2 : a  ∧  b
         p : a  ∧  b
 -----------------------------------   ∧E1
          π1 p : a
         p : a  ∧  b
 -----------------------------------   ∧E2
          π2 p : b

これらは Haskell では以下のような構文を使う

    data Product a b = P { x :: a , y :: b }
    let p = P 'a' 1
    x p
    y p

それぞれの型を確認してみよう。

直積を使った証明

Sum 排他的和

∧ はできたが、∨ はどうしよう? ∧の上下をひっくり返すと良さそうに思える。

            a
 -----------------------------------   ∨E1
         a  ∨  b
            b
 -----------------------------------   ∨E2
         a  ∨  b

こっちは良さそう。

         a  ∨  b
 -----------------------------------   
       a          b

これはよろしくない。下は一つでないと。

         a  ∨  b
 -----------------------------------   
             :
             :
 -----------------------------------   
           c

となるのが望ましい。

         a  ∨  b     a -> c    b -> c
 -------------------------------------- ∨I 
           c

というのが正しそう。この∨は、命題論理の∨と少し違う。

これに対応する項は、

            x : a
 -----------------------------------   ∨E1
         L x : a  ∨  b
            y : b
 -----------------------------------   ∨E1
         R y : a  ∨  b
         s : a  ∨  b     i1 : a -> c    i2 : b -> c
 -------------------------------------------------------------- ∨I 
         ?