依存和型
#Fleeting_Notes
依存和型(dependent sum type)、シグマ型(Σ-type)、依存対型、依存ペア型(dependent pair type)
シグマ型(Σ-types)や依存ペア型などいろいろ呼び方がある
具体的な値を思い浮かべやすいという点で依存対型、依存ペア型が呼び方としておすすめ
具体的な値
[(Nat, 1), (String, "hello"), (Bool, true)]
表記1
$ \sum_{x:A}B(x)
$ B(x) : 依存型
表記2
$ \Sigma_{(x:A)} B(x)
確認用
Q. 依存和型
参考
『言語の数理とLLMの知能 -言葉を計算で繋ぐメカニズム-』
メモ
多相関数と依存型をちゃんと理解しよう - 檜山正幸のキマイラ飼育記 (はてなBlog)
/mrsekut-p/依存和型
Σ: 依存ペア型 - Lean by Example
関連
(論理) 存在量化
(集合) 直和(disjoint sum)
(ホモトピー) 全空間
依存積型
調査用
Google.icon 依存和型(日)
Google.icon Dependent sum type(英)
Wikipedia.icon
依存和型 - Wikipedia(日)
依存和型(検索) - Wikipedia(日)
Wikipedia.icon
Dependent sum type - Wikipedia(英)
Dependent sum type(検索) - Wikipedia(英)