ラムダ計算 - mrsekut-p

ラムダ計算

Alonzo ChurchとStephen Cole Kleeneが1930年代に発明した計算モデル

すべての計算が関数定義と関数適用の基本的な演算に帰着される

変数や値も全てラムダ抽象で表す

例えばtrueも自然数も関数

ref Church encoding

四則演算子などもない、必要であれば無から関数で構成する

二変数関数は一変数関数を返す関数として定義

ラムダ計算の実行順序は、継続によって決まる

ラムダ計算の表示的意味論

ラムダ計算の表記

ラムダ計算での実装

イメージ的には以下のような階層関係mrsekut.icon

ラムダ計算

型無しラムダ計算

型付きラムダ計算

単純型付きラムダ計算

それ以外の型付きラムダ計算

こういうふうにも見れる

ラムダ計算

型付きラムダ計算

型無しラムダ計算

単純型付きラムダ計算

それ以外の型付きラムダ計算

「型なしラムダ計算」を「1つの型しか持たない型付きラムダ計算」、と見ている

ラムダ計算の実行の抽象化

関連

ラムダ式同士の等価性

Church encoding

Church-Rosserの定理

Lambda Explorer

https://lambdaexplorer.com/

ラムダ計算の処理系

勉強のための資料集

「ラムダ計算」を独学で学習するための，講義ノートやPDFのリンク集　（復習用の問題付き） - 主に言語とシステム開発に関して

https://nowokay.hatenablog.com/entry/20110926/1317015450#fn-34da927f

参考

『(理論)12 計算モデルの基礎理論』

今読んだ中では一番くわしい

『C言語による計算の理論』 11章

計算可能性の話に重点を置いて、関連してラムダ計算の紹介がある

実践より

『アンダースタンディングコンピューテーション』

横内『プログラム意味論』

『論理と計算のしくみ』

『計算モデルとプログラミング』

Schemeでごにょる

http://www.cs.tsukuba.ac.jp/~kam/lecture/complogic2014/main.pdf

https://tarao.hatenablog.com/entry/20100208/1265605429