依存直積型
依存直積型
第二成分の型が第一成分の値に依存するような直積型
表記
Leanでは以下のように表記する
(a : α) × β a Σ a : α, β a /mrsekut-book-4007305803/252ではラムダ式の記法で書かれていた
\Sigma_n:\mathrm{Nat}.A^n
Leanでの
(n : Nat) × A^n と同じ具体例
具体的に書き出してみるとわかりやすい
普通の集合Aがある
A=\{x,y,z\}
また、Aに依存するような集合B(a)を以下のように定める
B(x)=\{1,2\}
B(y)=\{\mathrm{True},\mathrm{False}\}
B(z)=\{\heartsuit,\clubsuit\,\spadesuit\}
このとき、依存直積(a:A)\times B(a)は以下のようになる
\{(x,1),(x,2),(y,\mathrm{True}),(y,\mathrm{False}),(z,\heartsuit),(z,\clubsuit),(z,\spadesuit)\}
従って、\Sigmaを使って、
\sum_{a\in A} B(a)と表記する
これは、なぜ「依存直積型」なのに「Σ」を使うのかという疑問に答えている
Leanの表記の
(a : A) × B a や Σ a : A, B a の意味もわかる本当は↑Leanでも表現できるような具体例を書きたかったが、色々知識不足過ぎて無理なので諦めた
直積型の一般化である
上記の例だと
(a : A) × B a とした時、 B a は a に依存した直積になっているが、 (a : A) × C のような直積は、通常の直積
A × C と同じであるLeanでの依存直積型の表記 ref
以下2つは同じ意味
leandef f (α : Type u) (β : α → Type v) (a : α) (b : β a) : (a : α) × β a :=
⟨a, b⟩
def g (α : Type u) (β : α → Type v) (a : α) (b : β a) : Σ a : α, β a :=
Sigma.mk a bちなみに前者の記号
⟨ は、 \< とか \langle で出せる