Program ＞ Haskell ＞ Haskell入門 ＞ 第1章 はじめてのHaskell

Haskell入門 関数型プログラミング言語の基礎と実践 本間 雅洋 技術評論社 2017-09-27 ￥3608

【Column】 ラムダ計算 †

関数型プログラミング言語は、「ラムダ計算」という計算モデルが礎にあります。

（参考）日経ソフトウエア 2008年3月号 55ページ

ラムダ計算 †

（参考）ラムダ計算 - Wikipedia https://w.wiki/3aqc

ラムダ計算（ラムダけいさん、英語: lambda calculus）は、計算模型のひとつで、計算の実行を関数への引数の評価（英語: evaluation）と適用（英語: application）としてモデル化・抽象化した計算体系である。
ラムダ算法とも言う。
関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。
アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。
1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を（否定的に）解いた。
ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。
計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。

ラムダ計算は1つの変換規則（変数置換）と1つの関数定義規則のみを持つ、最小の（ユニバーサルな）プログラミング言語であるということもできる。
ここでいう「ユニバーサルな」とは、全ての計算可能な関数が表現でき正しく評価されるという意味である。
これは、ラムダ計算がチューリングマシンと等価な数理モデルであることを意味している。
チューリングマシンがハードウェア的なモデル化であるのに対し、ラムダ計算はよりソフトウェア的なアプローチをとっている。

型付きラムダ計算 †

Haskellは、型付きラムダ計算に分類されます。

（参考） 型付きラムダ計算 - Wikipedia https://w.wiki/4iDA

型付きラムダ計算（英: typed lambda calculus）とは、無名の関数の抽象表現にラムダ ({\displaystyle \lambda }\lambda ) というシンボルを用いる型付き形式手法である。
型付きラムダ計算は基礎的なプログラミング言語でもあり、MLやHaskellなどの型付き関数型言語の基盤であり、さらには型付き命令型プログラミング言語の間接的な基盤とも言える。
また、カリー・ハワード同型対応によって数理論理学と証明論とも密接に関連しており、圏論のクラスの内部言語と見なすこともできる。
例えば単純な型付きラムダ計算はデカルト閉圏 (CCC) の言語である。

ある観点から見れば、型付きラムダ計算は型を持たないラムダ計算を改良したものと言えるが、別の観点からは、より根本的な理論と見ることもでき、型を持たないラムダ計算の方が型が1つしかない特殊ケースと見ることができる。

「型」に関する参考ページ †

• 型の理論入門 （ 論理学入門 III ） | MaruLabo
  https://www.marulabo.net/docs/type-theory-talkie/

• 型の理論 入門 - YouTube
  https://www.youtube.com/playlist?list=PLQIrJ0f9gMcNMNV-GKmpmvvy9d_KEAZj2

YouTube †

• 「型の理論」入門（３）「型付きラムダ計算」 - YouTube
  https://www.youtube.com/watch?v=p9dv0RH4s60