Martin-Lofの 理論とそのパラドックス

Martin-Lofの1971年の論文では、循環性がその中核を占めています。彼は、この条件があるので、彼の理論は圏論と非常に相性が良い（ご存知のように、圏論では、圏全体は圏をなし、その意味で強い循環性を持ちます）と主張しています。しかし、翌年に、Girardがこの中核部分の（もしくは現代の書き方では Type: type）からパラドックス（ブラリ-フォルティのパラドックスの一般化）が導けることを証明し、彼の夢は消えました。現在では、循環的部分を削除した、厳格な可述性に基づく依存型理論（おそらく整合的だろうと思われるもの）が、Martin-Lofの体系ということになっています。
さて、Girardのパラドックスですが、文献は

• Girardの論文は仏文？だったはずなので、Thierry Coquandの An Analysis of Girard's Paradox (LICS 1986)をどうぞ。
• その計算的な振る舞いについては、Doug Howe のThe Computational Behaviour of Girard's Paradox をどうぞ。この矛盾はループする計算に対応するとか。

そして、Girardのパラドックスを簡略化したのが Hurkensのパラドックス です。

• 文献はA simplification of Girard's paradox(Antonius J. C. Hurkens)（LNCS902）です（C先生曰く "Very good paper!!"だそうです）。
• Hurkensのパラドックスは、すでに証明支援系でもコードされています。
  • Coqはこちら。
  • Agdaはこちら。

さて、本日C先生から教えていただいたのが、Type:Type を貫きながら、それに領域理論のモデルを与えた強者の話。Microsoft Cambridge Lab. のLuca Cardelli*1なんですが、問題の論文は ここにある以下の二本だそうです。

• A polymorphic lambda-calculus with Type:Type
• Phase distinctions in Type Theory

*1:id:havanaclub さんが「神」とブクマコメントしていて納得しました。