関数型プログラミングの推薦図書：理論編

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

以前にも[関数型プログラミングの推薦図書のブログ](https://qiita.com/Trubetzkoy/items/14926a7ccb4d2a0e9107)を書いたが、そちらは理論というよりも実践・応用編でコンピュータ技術者向けである。

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

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

[The Lambda Calculus: Its Syntax and Semantics](https://amzn.to/3Z4gn2R)
H. P. Barendregt
中級向けのラムダ計算の名著。

[Introduction to Lambda Calculus](http://cl-informatik.uibk.ac.at/events/isr-2024/B/material/lambda-sel.pdf)
Henk Barendregt & Erik Barendsen (2000)
ラムダ計算のチュートリアル

[A Tutorial Introduction to the Lambda Calculus (PDF)](https://personal.utdallas.edu/~gupta/courses/apl/lambda.pdf)
Raul Rojas (2015)
ラムダ計算を簡単に学ぶためのチュートリアル。

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

### 再帰理論
再帰理論は、不動点理論や計算可能性の研究と関係がある。
[Introduction to Metamathematics](https://amzn.to/4377o2g)
Stephen Cole Kleene

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

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

[On the Building Blocks of Mathematical Logic](https://content.wolfram.com/sites/43/2020/12/Schonfinkel-OnTheBuildingBlocksOfMathematicalLogic.pdf)
Moses Schönfinkel (1924)
コンビネータ理論の起源となった歴史的論文。

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

https://amzn.to/4ebKqMl


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

前掲の「[Combinatory Logic, Volume I](https://amzn.to/3YuZr5rf)」もcurry-Howard対応の歴史的名著となっている。

[Proof and Types](https://amzn.to/4iLSMv3)  [(PDF)](https://www.paultaylor.eu/stable/prot.pdf)
Jean-Yves Girard (1989) 
ラムダ計算と自然演繹の関係を明示的に示した古典的教科書


### 関数型プログラミング

[Can Programming Be Liberated from the von Neumann Style (PDF)](http://www.arcaneoverflow.co.uk/archive/John_Backus-Can_Programming_Be_Liberated_From_the_Von_Neumann_Style--A_Functional_Style_And_Its_Algebra_Of_Programs.pdf)
John Backus (1977)
プログラミングには関数型プログラミング的な言語が必要でないかと問題意識を提示した歴史的論文。

[An Introduction to Functional Programming through Lambda Calculus](https://amzn.to/43CFDir)　[PDF](https://www.macs.hw.ac.uk/~greg/books/gjm.lambook88.pdf)
Greg Michaelson (1988)
書名の通りズバリ、関数型プログラミングとラムダ計算のための書籍。1.3節のOrigin of functional languagesに関数型プログラミングの歴史的流れが記してあるので、是非読むべき。

[Lambda-Caluculus, Combinators, and Functional Programming](https://www.amazon.co.jp/Lambda-calculus-Combinators-Functional-Programming-Theoretical/dp/0521114292/ref=tmm_pap_swatch_0?_encoding=UTF8&dib_tag=se&dib=eyJ2IjoiMSJ9.7w09bzfKL1VrAepBOCSpg6_8omm7DBgsnNjfy8F5GDnAPzxTnhiPKobOGQvdEvWrGFTkf1bR0f1nonZVKeWVD2mPmGUF-83tlPmGB9OrlshnL1mcK-eZNPy3pxXekEMpXldEeCXU8MmVgdeNRpCW7g.JGlVCBGIROROMZLjvi5YprXy6EJ47CS4rUzALT6v8hw&qid=1750138423&sr=8-1)
Györgi Revesz (1988)
コンパクトに纏まっている入門書。