依存積型 - pogi-log

依存積型

依存積型(dependnt product type)、パイ型(Π型)、依存関数型(dependent function type)

依存関数型(dependent function type)や、パイ型(Π-types)などいろいろ呼び方がある

表記1

$ \prod_{x:A}B(x)

表記2

$ \Pi_{(x:A)} B(x)

ラムダ計算で表すと、λx.f(x)という文のようなもの

入力x : Aを受け取ってf(x) : B(x)という出力をする

形成規則(formation rule)

$ \frac{\Gamma, 𝑥:𝐴 \vdash 𝐵(x) \ \mathrm{type}}{Γ \vdash \Pi_{x:A} B(x)\ \mathrm{type}}\Pi.

導入規則(introduction rule)

除去規則(elimination rule)

計算規則(computation rule)

確認用

Q. 依存積型