Types and Programming Languages

Audrey Tangさんに刺激されてAmazonで買ってしまいました。
Types and Programming Languagesを勉強することで、これまでとは違った物の考え方ができるようになればなぁと思っています。

実際に読み始めると、自分の数学の理解力が壁になりそうな感じがしました。本書では、公理、定義、定理を1つずつ積み上げて数学的に説明がされているので、そのやり方になじまないときつそうです。久しぶりに数学的な本を読んだので頭がパンクしそうです。

ついていけるか心配だけど、Audrey Tangさんが本書を勉強しながらPugsの開発をされたことを考えると、「自分も今、同じ本を読んでいるんだなぁ」とワクワクします。

なんだかんだ言いながら、今はChapter 5の"The Untyped Lambda-Calculus"を読んでいます。"Lambda-Calculus"って何か響きがカッコいいです。ちなみに、Lambda-Calculusという言葉は聞いたことがありましたが、勉強したのは今回が初めてです。

この章の最初の方に「論理和と論理否定の関数を定義しろ」という演習問題があるのですが、論理和の方は解けませんでした...一番簡単な問題なのに...でも論理否定は解けました。真(tru)と偽(fls)を表現する関数が定義されているもとで、論理否定(not)は以下のように定義されます。

not = λb. b fls tru;
tru = λt. λf. t;
fls = λt. λf. f;

一応検算してみると...

   not tru
=  (λb. b fls tru) tru
→ tru fls tru
=  (λt. λf. t) fls tru
→ (λf. fls) tru
→ fls

   not fls
=  (λb. b fls tru) fls
→ fls fls tru
=  (λt. λf. f) fls tru
→ (λf. tru) fls
→ tru

Lambda-Calculusはじっくりやってみると面白いかもしれません。

Types and Programming Languages (The MIT Press)