Valentin Blot, 09/06/2017 11:00
AN INTERPRETATION OF SYSTEM F THROUGH BAR RECURSION Valentin Blot, Queen Mary University of London Salle B107, bâtiment B, Université de Villetaneuse 09/06/2017 11:00 - 12:30 Résumé : There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the programs obtained from these two interpretations have a fundamentally different computational behavior and their relationship is not well understood. We make a step towards a comparison by defining the first translation of system F into a simply-typed total language with a variant of bar recursion. This translation relies on a realizability interpretation of second-order arithmetic. Due to Gödel's incompleteness theorem there is no proof of termination of system F within second-order arithmetic. However, for each individual term of system F there is a proof in second-order arithmetic that it terminates, with its realizability interpretation providing a bound on the number of reduction steps to reach a normal form. Using this bound, we compute the normal form through primitive recursion. Moreover, since the normalization proof of system F proceeds by induction on typing derivations, the translation is compositional. The flexibility of our method opens the possibility of getting a more direct translation that will provide an alternative approach to the study of polymorphism, namely through bar recursion.
Salut, Valentin n'étant pas encore arrivé (un peu juste en temps depuis GdN), on commencera plutôt à 11h30. Flavien Le 2017-06-06 12:14, breuvart a écrit :
AN INTERPRETATION OF SYSTEM F THROUGH BAR RECURSION
Valentin Blot, Queen Mary University of London
Salle B107, bâtiment B, Université de Villetaneuse
09/06/2017 11:00 - 12:30
Résumé : There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the programs obtained from these two interpretations have a fundamentally different computational behavior and their relationship is not well understood. We make a step towards a comparison by defining the first translation of system F into a simply-typed total language with a variant of bar recursion. This translation relies on a realizability interpretation of second-order arithmetic. Due to Gödel's incompleteness theorem there is no proof of termination of system F within second-order arithmetic. However, for each individual term of system F there is a proof in second-order arithmetic that it terminates, with its realizability interpretation providing a bound on the number of reduction steps to reach a normal form. Using this bound, we compute the normal form through primitive recursion. Moreover, since the normalization proof of system F proceeds by induction on typing derivations, the translation is compositional. The flexibility of our method opens the possibility of getting a more direct translation that will provide an alternative approach to the study of polymorphism, namely through bar recursion.
_______________________________________________ Gdtlogprog mailing list Gdtlogprog@lipn.univ-paris13.fr https://www-lipn.univ-paris13.fr/mailman/listinfo/gdtlogprog
participants (1)
-
breuvart