시스템 “F”와 시스템 “T”의 이름이 어디에서 유래했는지 아는 사람이 있습니까? 누가 그 이름 (Girard System F, Gödel System T)을 소개했는지는 묻지 않고 “F”와 “T”의 의미는 무엇입니까?
답변
나는 이것을 TYPES에 게시했지만 여기에서도 복사 할 가치가 있습니다.
-
“15 년 후 변수 유형의 시스템 F”에서 Girard는 이름 F에 특별한 이유가 없다고 말합니다.
그러나 [3]에서 우연히 F라고 불리는이 시스템에 대한 명백한 변환 규칙이 수렴하고 있음을 보여 주었다.
그의 논문에는 또 다른 설명이있을 수 있지만 불행히도 나는 프랑스어에 유창하지 않기 때문에 그것을 읽지 못했습니다.
-
그러나 나는 독일어로 반 문학을 했으므로 Gödel의 논문 “Uber eine noch nicht benüzte Erweiterung des finiten Standpunktes”를 보았습니다. 여기서 System T (그리고 Dialectia 해석)가 소개되었습니다. 그는이 시스템의 이름을 괄호로 묶습니다.
Das heisst die Axiome dies Systems (es werde T genannt) 정식 빠른 디젤 엔진 다이 다이어 프라이머 티어 rekursiven Zahlentheorie […] [1]
그러나 이전 페이지와 절반은 시스템 T의 유형 구조에 대해 이야기하는 데 소비되었으므로 T가 “유형”을 의미한다고 추측하는 것이 합리적입니다. 그러나 인쇄에 명시적인 이유는 없습니다.
[1] “이것은이 시스템의 공리 (T라고 함)가 원시 재귀 수 이론의 공리와 거의 동일하다는 것을 의미합니다 …]