Czy ktoś wie, skąd pochodzą nazwy System „F” i System „T”? Nie pytam, kto wprowadził te nazwy (Girard System F i Gödel System T), ale co oznaczają „F” i „T”.
Czy ktoś wie, skąd pochodzą nazwy System „F” i System „T”? Nie pytam, kto wprowadził te nazwy (Girard System F i Gödel System T), ale co oznaczają „F” i „T”.
Odpowiedzi:
Wysłałem to do TYPES, ale prawdopodobnie warto również skopiować tutaj:
W „Systemie typów zmiennych piętnaście lat później” Girard zauważa, że nie ma konkretnego powodu dla nazwy F:
Jednak w [3] wykazano, że oczywiste zasady konwersji dla tego systemu, zwanego przez przypadek F, były zbieżne.
Może być inne wytłumaczenie w jego pracy magisterskiej, ale jej nie przeczytałem, ponieważ niestety nie mówię płynnie po francusku.
Ponieważ jednak mam słabą znajomość języka niemieckiego, rzuciłem okiem na artykuł Gödela „Über eine noch nicht benüzte Erweiterung des finiten Standpunktes”, w którym wprowadzono System T (i jego interpretację Dialectia). Nazywa ten system w nawiasach:
Das heisst die Axiome dieses Systems (es werde T genannt) sind formal fast dieselben wie die der primitiv rekursiven Zahlentheorie [...] [1]
Jednak poprzednie półtorej strony poświęciliśmy na rozmowę o strukturze typu systemu T, więc rozsądne jest odgadnięcie, że T oznacza „typy”. Ale w druku nie podano wyraźnego powodu.
[1] „Oznacza to, że aksjomaty tego układu (nazwane T) są prawie takie same jak w pierwotnej teorii liczb rekurencyjnych [...]”