Nombres del sistema F y del sistema T

9

¿Alguien sabe de dónde vienen los nombres Sistema "F" y Sistema "T"? No estoy preguntando quién introdujo esos nombres (Girard System F y Gödel System T), sino qué significan la "F" y la "T".

Alejandro DC
fuente

Respuestas:

8

Publiqué esto en TYPES, pero probablemente también valga la pena copiarlo aquí:

  1. En "El sistema F de tipos variables, quince años después", Girard señala que no había una razón particular para el nombre F:

    Sin embargo, en [3] se demostró que las reglas obvias de conversión para este sistema, llamado F por casualidad, estaban convergiendo.

    Puede haber otra explicación en su tesis, pero no la he leído ya que desafortunadamente no hablo francés con fluidez.

  2. Sin embargo, dado que estoy semi-alfabetizado en alemán, eché un vistazo al artículo de Gödel "Über eine noch nicht benüzte Erweiterung des finiten Standpunktes", donde se introdujo el Sistema T (y la interpretación de Dialectia). Él nombra este sistema entre paréntesis a un lado:

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

    Sin embargo, la página y media anterior se dedicaron a hablar sobre la estructura de tipos del sistema T, por lo que es razonable suponer que T significa "tipos". Pero, no se da ninguna razón explícita en forma impresa.

    [1] "Esto significa que los axiomas de este sistema (denominado T) son casi los mismos que los de la teoría primitiva recursiva de números [...]"

Neel Krishnaswami
fuente
2
Acabo de comprobar la tesis de Girard : habla sobre "sistema de sistema" (sistema funcional), pero nunca menciona "Sistema F". Entonces, lo que probablemente sucedió es que ha acortado el nombre más tarde.
Alejandro DC
3
@AlejandroDC Aunque esa hipótesis suena plausible, para su información, ese enlace no es la tesis completa, solo partes y piezas transcritas por Kevin Watkins . (No he visto una copia del original.)
Noam Zeilberger