最近、関数型プログラミングについて認知度が高まってきているように思う。私自身もそうであるが、関数型プログラミングにたいしてある程度のイメージを持っていたが、調べてみると意外とずれていて、勘違いすることが多かった。そのズレを直し、正しく関数型の発展の筋を理解する必要性を感じてきた。そこで、自分が勉強してきたり、これから読んでみたいと思う名著を紹介したい。

以前にも推薦図書のブログを書いたが、そちらは理論というよりも実践・応用編でコンピュータ技術者向けである。

ラムダ計算

関数型の基本はラムダ計算である。

Lambda-Calculus and Combinators: An Introduction
J. Roger Hindley, Jonathan P. Seldin
ラムダ計算とコンビネータ理論の初心者向け教科書。私もこれで勉強を始めている。

The Lambda Calculus: Its Syntax and Semantics
H. P. Barendregt
中級向けのラムダ計算の名著。

A Tutorial Introduction to the Lambda Calculus
Raul Rojas
ラムダ計算を簡単に学ぶためのチュートリアル。

再帰理論

再帰理論は、不動点理論や計算可能性の研究と関係がある。
Introduction To Metamathematics
Stephen Cole Kleene

コンビネータ理論

ラムダ計算は計算の基礎理論であり、変数も関数も区別なく、計算という概念に取り込んでいる。コンビネータの始まりは、以下に道具（公理）を少なくして、記述をするかという問題意識に乗っ取っており、どうやって関数の入力変数（argument）を減らして、関数を抽象化するこということを目指している。

Combinatory Logic, Volume I
Haskell B. Curry & Robert Feys (1958)
コンビネータ理論を詳細に知りたい人のための古典的名著。プログラミン言語の名前にもなったHaskell B. Curryの著作。

On the Building Blocks of Mathematical Logic
Moses Schönfinkel (1924)
コンビネータ理論の起源となった歴史的論文。

To Mock a Mockingbird
Raymond Smullyan (1985)
コンビネータを童話風に描いた初心者向け書籍。コンビネータ理論版不思議の国のアリスといったところ。

型の理論と証明支援

コンビネータ理論を突き詰めていくと、式の型から数学的証明が導き出せるという理論に行き着く。これがCurry-Howard対応である。私はまだ取り組んでいないので、読みたいものを示す。

前掲の「Combinatory Logic, Volume I」もcurry-Howard対応の歴史的名著となっている。

Proof and Types
Jean-Yves Girard (1989)
ラムダ計算と自然演繹の関係を明示的に示した古典的教科書
PDF

関数型プログラミング

Can Programming Be Liberated from the von Neumann Style

John Backus (1977)
プログラミングには関数型プログラミング的な言語が必要でないかと問題意識を提示した歴史的論文。