markdown

関数型プログラミングと型理論ポータル

lecture/information/programming-languages/foundation/関数型プログラミングと型理論ポータル-講義.n.md

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

date2026-04-01description関数型プログラミングと型理論の講義全体の入口。λ計算・型付きλ計算・Curry–Howard対応・依存型理論へ向かう学習地図である。type講義statusactive

portalinformationprogramming-languageslecture

導入どうにゅう

この束たばは、λ計算らむだけいさんから型付かたつきλ計算らむだけいさん・多相たそう型かた・Curry–Howard対応たいおう・依存型理論いぞんかたりろんへと至いたる学習路がくしゅうじを整理せいりする。関数型かんすうがたプログラミングの動機どうきから出発しゅっぱつし、計算けいさんとは何なにか・型かたとは何なにかを形式的けいしきてきに問とい直なおす内容ないようである。

このポータルは 情報工学ポータル から参照さんしょうされている。前提ぜんていとして利用りようできる既存きそんの講義こうぎは下したの「前提ぜんていコンテンツ」に示しめした。

全体像ぜんたいぞう

この束たばは次つぎの 5 層そうで構成こうせいされる。

層そう	ディレクトリ	内容ないよう
§A 基礎きそ	`foundation/`	FP の動機どうき・束縛そくばく・置換ちかん・評価戦略ひょうかせんりゃく
§B 純粋計算体系じゅんすいけいさんたいけい	`lambda-calculus/`	λ計算らむだけいさん・β簡約かんやく・コンビネータ・Church encoding
§C 型付かたつきλ計算らむだけいさん	`type-theory/`	STLC・積型せきがた・多相たそう・HM型推論かたすいろん
§D 論理ろんりとの対応たいおう	`curry-howard/`	Curry–Howard対応たいおう・依存型いぞんかた
§E 拡張かくちょう	`extensions/`	型かたクラス・線形型せんけいかた・モナド・圏論けんろん

§A: 基礎きそ・橋渡はしわたし（`foundation/`）

data/lecture/information/programming-languages/foundation/関数型プログラミングの入口-講義.n.md data/lecture/information/programming-languages/foundation/束縛と自由変数の基本-講義.n.md data/lecture/information/programming-languages/foundation/置換とα同値の基本-講義.n.md

§B: 純粋計算体系じゅんすいけいさんたいけい（`lambda-calculus/`）

data/lecture/information/programming-languages/lambda-calculus/ラムダ計算の基本-講義.n.md data/lecture/information/programming-languages/lambda-calculus/β簡約とη変換の基本-講義.n.md data/lecture/information/programming-languages/lambda-calculus/コンビネータ計算の基本-講義.n.md data/lecture/information/programming-languages/lambda-calculus/Church encodingの基本-講義.n.md data/lecture/information/programming-languages/lambda-calculus/不動点と再帰の基本-講義.n.md data/lecture/information/programming-languages/lambda-calculus/操作的意味論の基本-講義.n.md

§C: 型付かたつきλ計算らむだけいさんと多相たそう（`type-theory/`）

data/lecture/information/programming-languages/type-theory/型とは何か-講義.n.md data/lecture/information/programming-languages/type-theory/単純型付きラムダ計算の基本-講義.n.md data/lecture/information/programming-languages/type-theory/型安全性の基本-講義.n.md data/lecture/information/programming-languages/type-theory/let多相の基本-講義.n.md data/lecture/information/programming-languages/type-theory/HindleyMilner型推論の基本-講義.n.md

§D: 論理ろんりとの対応たいおう・依存型いぞんかた（`curry-howard/`）

data/lecture/information/programming-languages/curry-howard/Curry-Howard対応の基本-講義.n.md data/lecture/information/programming-languages/curry-howard/依存型理論の入口-講義.n.md

前提ぜんていコンテンツ

data/lecture/information/discrete-math/離散数学の入口-講義.n.md data/lecture/information/discrete-math/論理と真理値表の基本-講義.n.md data/lecture/information/discrete-math/集合と写像の基本-講義.n.md data/lecture/information/programming/プログラミング基礎の入口-講義.n.md data/lecture/information/algorithm/foundation/再帰の基本-講義.n.md

一言ひとことでいうと

関数かんすうを第一級だいいちきゅうの市民しみんとして扱あつかう計算けいさんの形式化けいしきかがλ計算らむだけいさんであり、その項こうに型かたを付つけることで「何なにが正ただしい計算けいさんか」を数学的すうがくてきに議論ぎろんできるようになる。