2015年4月25日土曜日

TaPL chapter 5: lambda と評価戦略

TaPL 5 章は lambda calculus の復習。今日は "Recursion" の前までしか読めなかった。

評価戦略のまとめ。

  • full beta-reduction: 簡約できるところは全部簡約する。どこを簡約するかは自由
  • normal order startegy: 最も左の、最も外側の redex から順に簡約する
  • call by name: normal order に似てるけど、lambda abstraction の中(関数の中)は簡約しない。
  • call by need: call by name の変形版。一度簡約した redex を記憶しておき、同じ redex を複数回簡約しない。Haskell のやつ。
  • call by value: 引数から先に簡約する。lambda abstraction の中はしない。多くの言語(C, Java など)で採用されてる。この本では call by value を使う。

それから、基本的な関数(例えば整数の equality check とか)を lambda calculus でどう書くかという話。例えば、リスト [x, y, z] を
  \c. \n. c x (c y (c z n))
と表すとすると、nil, cons などは以下のようになる。(exercise 5.2.8)

---
nil => \c. \n. n

---
cons = \h. \t. \c. \n. c h (t c n)

---
isnil = \t. t (\x. \y. fls) tru

isnil (\c. \n. c z n) = (\c. \n. c z n) (\x. \y. fls) tru
                      = (\x. \y. fls) z tru
                      = fls


---
head = \t. t (\x. \y. x) fls

head nil = (\t. t (\x. \y. x) fls) (\c. \n. n)
         = (\c. \n. n) (\x. \y. x) fls
         = fls

head (\c \n. c z n) = (\t. t (\x. \y. x) fls) (\c \n. c z n)
                    = (\c \n. c z n) (\x. \y. x) fls
                    = (\x. \y. x) z fls
                    = z


---
nils = pair nil nil
ss = \t. \p. pair (snd p) (cons t (snd p))
tail = \t. fst (t ss nils)

tail [x, y] = tail (\c. \n. c x (c y n))
            = (\t. fst (t ss nils)) (\c. \n. c x (c y n))
            = fst ((\c. \n. c x (c y n)) ss nils)
            = fst (ss x (ss y nils))
            = fst (ss x (pair (snd nils) (cons y (snd nils))))
            = fst (ss x (pair nil [y]))
            = fst (pair [y] (cons x [y]))
            = [y]

tail [] = tail (\c. \n. n)
        = fst ((\c. \n. n) ss nils)
        = nil

こういうのはパズルなので考えればできると思うが、そもそも true を \t. \f. t と、1 を \s. \z. s z と表せばうまくいく、という考えにどうやってたどり着いたのか謎だ。


・・・で、そもそもなんでここで lambda の復習してるんだっけ。この後で使うんだろう、多分。

0 件のコメント:

コメントを投稿