システムFとシステムTの名前

誰もシステム “F”とシステム “T”の名前はどこから来るのか知っていますか?私はその名前を誰が紹介したのか(Girard
System F、GödelSystem T)は問いませんが、 “F”と “T”は何を意味していますか?

ベストアンサー

私はこれをTYPESに投稿しましたが、ここでもコピーする価値があります:

  1. In “The system F of variable types, fifteen years later”, Girard
    remarks that there was no particular reason for the name F:

    However, in [3] it was shown that the obvious rules of
    conversion for this system, called F by chance, were
    converging.

    There may be another explanation in his thesis, but I haven’t
    read it since unfortunately I am not fluent in French.

  2. However, since I am semi-literate in German, I did take a look
    at Gödel’s paper “Über eine noch nicht benüzte Erweiterung des
    finiten Standpunktes”, where System T (and the Dialectia
    interpretation for it) was introduced. He names this system in a
    parenthetical aside:

    Das heisst die Axiome dieses Systems (es werde T genannt) sind
    formal fast dieselben wie die der primitiv rekursiven Zahlentheorie
    […][1]

    However, the previous page and a half were spent talking about
    the type structure of system T, so it is reasonable to guess that T
    stands for “types”. But, no explicit reason is given in print.

    [1] “This means the axioms of this system (dubbed T) are nearly
    the same as those of primitive recursive number theory […]”

返信を残す

メールアドレスが公開されることはありません。 * が付いている欄は必須項目です