ジラールのパラドックス

ジラールのパラドックス(Girard's paradox)

集合論の文脈でのパラドックスであるラッセルのパラドックスがあって、型理論の中でも同じようなジラールのパラドックスというものがある

簡略化したものがHurkensのパラドックスらしい

$ \mathrm{Type} : \mathrm{Type} のように、型$ \mathrm{Type} が型$ \mathrm{Type} に含まれてしまって矛盾を起こす

こういうものは非可述的とか自己言及的と言われる

読む文献

Doug HoweのThe Computational Behaviour of Girard's Paradox. LICS 1987: 205-214 (pdf)

Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986) (pdf)

非可述的な型で起こる矛盾を解決したものは、型が階層を持っていて、自分自身を含まない可述的な構成になっている

型宇宙と呼ばれているっぽい

確認用

Q. ジラールのパラドックス