--Lambda Calculusの簡約

ここでは、Haskell の式をそのまま使う。record と data は使わない

---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で置き換える)

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

--問題

以下の式を計算せよ

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

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

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

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