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

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

ラムダ計算

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

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

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

Lecture Notes on the Lambda Calculus] (PDF版)
Peter Selinger (2013)
講義ノート、ラムダ計算について流れ良く書かれている。

Introduction to Lambda Calculus (PDF版)
Henk Barendregt & Erik Barendsen (2000)
ラムダ計算のチュートリアル

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

The Calculi of Lambda-Conversion
Alonzo Church (1941)
ラムダ計算の創始者チャーチの本。少し読みにくいが哲人が書いたものとして是非読んでみたい。

再帰理論

再帰理論は、不動点理論や計算可能性の研究と関係がある。
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)
コンビネータ理論の起源となった歴史的論文。

Foundations of Combinatory Logic
Haskell B. Curry
Curryの博士論文。コンビネータ理論の生まれた経緯を知るに読んでおきたい。

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

型の理論、Curry-Howard同型対応、証明支援

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

Lectures on the Curry‑Howard Isomorphism [PDF] (お薦め）(https://www.cs.cmu.edu/~rwh/courses/clogic/www/handouts/curry-howard.pdf)
Morten H. Sørensen & Paweł Urzychyn (2006)
Curry-Howard同型対応を学ぶ定番の教科書。

カリー・ハワード同型対応　工学部専門科目「計算と論理」配布資料 PDF
五十嵐淳 (2026)
Curry-Howard同型対応を手っ取り早く知りたい方はこれがいい。

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

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

圏論

圏論は計算の理論には必要な数学的領域だ。
ベーシック圏論
Tom Leinster (2014)
圏論の教科書で、私は読書会の対象書籍になっていたので、これで圏論を勉強しました。ただし、具体的な例が少なくて、証明などは自分で考える必要があります。

Topoi: The Categorial Analysis of Logic (お薦め）
Goldblatt (2006)
とても分かりやすく関手、自然変換など、具体例も豊富でむしろこちらの方が初心者向け。私はこの本をガイドブックとして活用しています。

関数型プログラミング

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

An Introduction to Functional Programming through Lambda Calculus　PDF
Greg Michaelson (1988)
書名の通りズバリ、関数型プログラミングとラムダ計算のための書籍。1.3節のOrigin of functional languagesに関数型プログラミングの歴史的流れが記してあるので、是非読むべき。

Lambda-Caluculus, Combinators, and Functional Programming
Györgi Revesz (1988)
コンパクトに纏まっている入門書。