ラムダ計算の話

ラムダ計算の話 宇佐見公輔 第3回 関西日曜数学 友の会

自己紹介 • 宇佐見公輔（@usamik26） • 大学時代は数学専攻（代数、応用数理） • 現在はプログラマ（フェンリル株式会社、iOS アプリ開発）

ラムダ計算（λ-calculus）とは • 計算機科学で出てくる体系のひとつ • プログラミング言語の型システムとの関連 • 関数型プログラミングを支える理論

ラムダ記法 • 数学で使われる関数の表記法 • ラムダ記法による関数の表記法

ラムダ記号の意味合い • ラムダ記法における は、 や のような意味合いの記号 • そう思って並べてみるとなんとなく似ている気がする

ラムダ記法：関数の適用 • ラムダ記法で関数に値を代入する • 記法の比較：関数 に値を代入する

ラムダ記法：多変数関数 • 多変数関数のラムダ記法 • これは1変数関数の組み合わせと同一視できる（カリー化）

ラムダ記法：高階関数 • に関数 を2回適用する関数の例 • カリー化して書けば

ラムダ式（λ-term）の導入 • ラムダ記法そのものを、より抽象的に取り扱う • そのために、記号列としてのラムダ式を導入する

ラムダ式の定義 • 可算無限濃度の集合 が与えられているとする • 以下で再帰的に定義される記号列の集合 の要素をラムダ式 と呼ぶ（なお、括弧は一定のルールで取り外すことができる） • (1) • (2) • (3) のとき のとき のとき

ラムダ式とラムダ記法 • は変数の集合を意味する • (1) は、変数はラムダ式であることを意味する • (2) は、関数のラムダ記法に対応する • (3) は、関数適用のラムダ記法に対応する

ラムダ計算 • こうして定義されたラムダ式の性質を見ることで、ラムダ記法 で記述された関数のなす世界を研究するのが、ラムダ計算の理 論である • 特に、個々の関数（ とか と か）の性質によらず、関数の世界に内在する性質を考察する

ラムダ式についての補足 • 記号列として定義されたラムダ式が、常にラムダ記法に対応し て意味を持つとは限らない（ラムダ記法としてありえない式が できてしまう） • しかし、まずはそれを許容して議論する方が見通しが良くなる • その後、型（関数の定義域や値域に相当する概念）を導入する ことで、ラムダ記法との対応の議論ができる

ベータ変換 • 以下で再帰的に定義されるラムダ式の変換をベータ変換と呼ぶ • (1) • (2) • ここで 式 ならば は、ラムダ式 および の中の変数 に置き換えたラムダ式のことである（代入） をラムダ

代入についての補足 • ラムダ式 の中の変数 があるとき • 代入 について、 という部分式 を束縛変数、そうでないとき自由変数と呼ぶ を考えるとき、 の自由変数は の束縛 変数ではないものとする • また の束縛変数は 以外の変数に置き換えて考える（一 般に、ラムダ式の束縛変数をその式に現れない別の変数に置き 換えた式を、元の式と同一視する）

ベータ変換の例 各ラムダ式の自由変数は他の式の束縛変数ではないものとする

Church-Rosser の定理 • ベータ変換のしかたは一通りではない • Church-Rosser の定理：ひとつのラムダ式からベータ変換で 得られたふたつのラムダ式は、何度かベータ変換を行うこと で、同じラムダ式にできる

正規形 • Church-Rosser の定理により、ラムダ式 のステップで止まる（式中に から始めて有限 がなくなる）ベータ変換列があ るとき、最終結果は一致する • この最終結果を の正規形と呼ぶ • 与えられた関数（ラムダ記法）を機械的に処理して正規形を得 るのが、関数型プログラミング言語における計算である（計算 機科学の用語では評価と呼ぶ）

さらなる話題・・・ • ここまでのラムダ計算は、型なしラムダ計算と呼ばれる • 型を導入した、型つきラムダ計算という体系がある • 型つきラムダ計算は、ラムダ記法との対応ができる • 型つきラムダ計算は、型を対象、ラムダ式を射として、圏をな す • これにより、圏論の議論が応用できる