余帰納法
#Fleeting_Notes
余帰納法(coinduction)
きちんと理解するには集合の言葉を使わないと全然わからない
帰納法による帰納的定義と、余帰納法による余帰納的定義で説明
帰納法による帰納的定義の方は、ベースを定義して、無限の方向に広がっていくような定義
余帰納法による余帰納的定義は、無限長のデータをどうにか定義する
帰納法による定義の方では最小不動点が関係して、余帰納法による定義では最大不動点というものが関係する?
数式で書いた場合の余帰納的定義の例
任意の集合$ A と無限のストリーム$ ⟨A^∞, γ : A^∞ → (A × A^∞)⟩
$ A^∞ は無限ストリームで、直観的に言うと無限リスト
確認用
Q. 余帰納法
関連
余帰納的型
双模倣
参考
矢田部 俊介. 循環性を受け入れる ――構成主義における可述性の位置づけの変更とその影響――. 2013. https://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/173335/1/phs_7_1.pdf
P9 の余帰納的定義
『型システム入門 -プログラミング言語と型の理論-』 P
メモ
帰納法と余帰納法の何がどう双対なのか(初等的に) - sumiiのブログ
Coqの余帰納法についてまとめました #Coq - Qiita
『A Tutorial on (Co)algebras and (Co)induction』
Data Types as Quotients of Polynomial Functors. https://drops.dagstuhl.de/storage/00lipics/lipics-vol141-itp2019/LIPIcs.ITP.2019.6/LIPIcs.ITP.2019.6.pdf
Coinduction - Wikipedia
調査用
Google.icon 余帰納法(日)
Google.icon Coinduction(英)
Wikipedia.icon
余帰納法 - Wikipedia(日)
余帰納法(検索) - Wikipedia(日)
Wikipedia.icon
Coinduction - Wikipedia(英)
Coinduction(検索) - Wikipedia(英)