論理関係

logical relationsとかfundamental theoremとかいう（S君曰く「いかがわしい」）名前についてTypesメーリングリストで質問したら、いろいろな人からいろいろな答えが。半分ぐらい個人メールだが。その「人」の研究のレベルと「答え」の内容のレベルがちゃんと正比例しているのがおもしろい。とか日本語なのをいいことに失礼な発言をしてみる。

ちなみに前者の正解は

http://www.seas.upenn.edu/~sweirich/types/archive/1989/msg00047.html

らしい。同様の返事がPlotkinから僕にも来たので、「eliminationができるから」とか「Curry-Howard同型による」とかはデマです（←暴言）。