依存積型

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

表記1

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

表記2

$ \Pi_{(x:A)} B(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)

$ \frac{\Gamma, x:A \vdash b(x) : B(x)}{\Gamma \vdash \lambda x.b(x) : \Pi_{(x:A)} B(x)}\Pi\text{-intro}.

除去規則(elimination rule)

$ \frac{\Gamma \vdash f : \Pi_{(x:A)} B(x) }{\Gamma, x:A\vdash f(x) : B(x)}\Pi\text{-elim}.

計算規則(computation rule)

$ \frac{\Gamma, x:A \vdash b(x) : B(x) }{\Gamma, x:A \vdash (\lambda y.b(y))(x)\ \dot{=}\ b(x) : B(x)}\Pi\text{-comp}.

$ \frac{\Gamma \vdash f : \Pi_{(x:A)} B(x)}{\Gamma \vdash \lambda x.f(x) \dot{=} f : \Pi_{(x:A)} B(x)}\Pi\text{-uniq}

確認用

Q. 依存積型

関連

(集合) 積(product)

(型理論)

(圏論)

参考

メモ

調査用

Wikipedia.icon

Wikipedia.icon