Second-Order Type Isomorphisms Through Game Semantics
| Autor: | Joachim De Lataillade |
|---|---|
| Přispěvatelé: | Preuves, Programmes et Systèmes (PPS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7) |
| Jazyk: | angličtina |
| Rok vydání: | 2007 |
| Předmět: |
Second-order λμ-calculus
FOS: Computer and information sciences Computer Science - Logic in Computer Science Pure mathematics Logic Game semantics Second-order λµ-calculus 0102 computer and information sciences Type (model theory) Characterization (mathematics) 01 natural sciences Computer Science::Logic in Computer Science Game Semantics Control Categories Types Isomorphisms 0101 mathematics Control (linguistics) Hyperdoctrines ACM: F.3.2 Mathematics System F 010102 general mathematics Classical logic [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Extension (predicate logic) 16. Peace & justice Logic in Computer Science (cs.LO) Algebra 010201 computation theory & mathematics F.3.2 Order type |
| Popis: | The characterization of second-order type isomorphisms is a purely syntactical problem that we propose to study under the enlightenment of game semantics. We study this question in the case of second-order λ$\mu$-calculus, which can be seen as an extension of system F to classical logic, and for which we define a categorical framework: control hyperdoctrines. Our game model of λ$\mu$-calculus is based on polymorphic arenas (closely related to Hughes' hyperforests) which evolve during the play (following the ideas of Murawski-Ong). We show that type isomorphisms coincide with the "equality" on arenas associated with types. Finally we deduce the equational characterization of type isomorphisms from this equality. We also recover from the same model Roberto Di Cosmo's characterization of type isomorphisms for system F. This approach leads to a geometrical comprehension on the question of second order type isomorphisms, which can be easily extended to some other polymorphic calculi including additional programming features. Comment: accepted by Annals of Pure and Applied Logic, Special Issue on Game Semantics |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|