関数型かんすうがたプログラミングと型理論かたりろんポータル

date2026-07-14document_iddoc_84693fdcb572eef2b425f8904ac5159fdescription関数型プログラミングから無型λ計算、型理論、Curry–Howard対応へ進む学習順と、各段階で導入する概念を示す講義ポータルである。prerequisitesdata/lecture/information/programming/introduction-to-programming.lecture.n.mdtype講義statusactive

portalinformationprogramming-languageslecture

1導入どうにゅう

このポータルでは、関数型かんすうがたプログラミングから無型むがたλ計算けいさん、型付かたつきλ計算けいさん、Curry–Howard対応たいおうへ進すすむ学習順がくしゅうじゅんを説明せつめいする。計算規則けいさんきそくと型規則かたきそくを段階的だんかいてきに導入どうにゅうし、異ことなる体系たいけいの主張しゅちょうを混同こんどうしないことが目的もくてきである。

2学習順がくしゅうじゅん

関数型かんすうがたプログラミングの動機どうきとして、参照透過性さんしょうとうかせいと第一級関数だいいちきゅうかんすうを理解りかいする。
変数へんすうの束縛そくばくと自由変数じゆうへんすうを定義ていぎする。
捕縛回避置換ほばくかいひちかんとα同値どうちを定義ていぎする。
無型むがたλ計算けいさんのβ簡約かんやく、正規形せいきけい、評価戦略ひょうかせんりゃくを学習がくしゅうする。
その後ごにのみ型判断かたはんだんを導入どうにゅうし、型付かたつきλ計算けいさんを学習がくしゅうする。

現時点げんじてんで本系列ほんけいれつに実装じっそうされているのは第だい4段階だんかいまでである。第だい5段階だんかいは今後こんごの講義こうぎで扱あつかう予定よていである。

data/lecture/information/programming-languages/foundation/introduction-to-functional-programming.lecture.n.md data/lecture/information/programming-languages/foundation/variable-binding-and-free-variables-basics.lecture.n.md data/lecture/information/programming-languages/foundation/substitution-and-alpha-equivalence-basics.lecture.n.md data/lecture/information/programming-languages/lambda-calculus/lambda-calculus-basics.lecture.n.md

3体系たいけいの境界きょうかい

無型むがたλ計算けいさんの項こうには型注釈かたちゅうしゃくがなく、 $Ω$ のように停止ていししない項こうも記述きじゅつできる。単純型付たんじゅんかたつきλ計算けいさんでは型判断かたはんだんを追加ついかし、型付かたつけ可能かのうな項こうを制限せいげんする。したがって、無型むがたの項こうに型安全性かたあんぜんせいを仮定かていしたり、単純型付たんじゅんかたつきの停止性ていしせいを無型むがたの全項ぜんこうへ適用てきようしたりしてはならない。

4論理ろんりへの接続せつぞく

型付かたつきλ計算けいさんを導入どうにゅうした後あと、型かたを命題めいだい、項こうを証明しょうめいとして解釈かいしゃくするCurry–Howard対応たいおうへ進すすむ。論理結合子ろんりけつごうしと集合しゅうごう・写像しゃぞうは、その数学的すうがくてき前提ぜんていである。

data/lecture/information/discrete-math/logic-and-truth-tables-basics.lecture.n.md data/lecture/information/discrete-math/sets-and-maps-basics.lecture.n.md

5まとめ

本系列ほんけいれつでは、束縛そくばくと置換ちかんを確立かくりつしてから無型むがたλ計算けいさんを導入どうにゅうし、その後ごに型かたと論理ろんりの関係かんけいを扱あつかう。

Functional Programming and Type Theory Portal

1Introduction

This portal presents a learning sequence from functional programming through the untyped lambda calculus and typed lambda calculi to the Curry–Howard correspondence. It introduces computational rules and typing rules in separate stages so that claims about distinct calculi are not conflated.

2Learning sequence

Understand referential transparency and first-class functions as motivations for functional programming.
Define variable binding and free variables.
Define capture-avoiding substitution and alpha-equivalence.
Study beta-reduction, normal forms, and evaluation strategies in the untyped lambda calculus.
Only then introduce typing judgments and study typed lambda calculi.

At present, this sequence implements only stages 1 through 4. Stage 5 is planned for future lectures.

3Boundaries between calculi

Terms of the untyped lambda calculus have no type annotations, and the calculus can express nonterminating terms such as $Ω$ . The simply typed lambda calculus adds typing judgments and restricts attention to typable terms. Consequently, one must neither assume type safety for untyped terms nor extend termination results for the simply typed calculus to all untyped terms.

4Connection to logic

After typed lambda calculi have been introduced, the sequence proceeds to the Curry–Howard correspondence, which interprets types as propositions and terms as proofs. Logical connectives, sets, and maps provide the mathematical prerequisites for that interpretation.

data/lecture/information/discrete-math/logic-and-truth-tables-basics.lecture.n.md data/lecture/information/discrete-math/sets-and-maps-basics.lecture.n.md

5Summary

This sequence establishes binding and substitution before introducing the untyped lambda calculus, and it addresses the relationship between types and logic only afterward.