2020-05-27から1日間の記事一覧

人生の諸問題に抽象的な理論で取り組む日記

TAPL §20 Recursive Types

再帰型が登場すると strong normalization が破綻する、normalization の中身読んでないので空気を読むと、型がついてても発散する項がありえるって話に驚き。あと D = μX.X→X(= D→D)と言う型で型無しラムダ計算を埋め込めてしまう……。無限はヤバイ。 Iso-…