Games and Weak-Head Reduction for Classical PCF

Abstract : We present a game model for classical PCF, a finite version of PCF extended by a catch/throw mechanism. This model is built from E-dialogues, a kind of two-players game defined by Lorenzen. In the E-dialogues for classical PCF, the strategies of the first player are isomorphic to the Böhm trees of the language. We define an interaction in E-dialogues and show that it models the weak-head reduction in classical PCF. The interaction is a variant of Coquand's debate and the weak-head reduction is a variant of the reduction in Krivine's Abstract Machine. We then extend E-dialogues to a kind of games similar to Hyland-Ong's games. Interaction in these games also models weak-head reduction. In the intuitionistic case (i.e. without the catch/throw mechanism), the extended E-dialogues are Hyland-Ong's games where the innocence condition on strategies is now a rule. Our model for classical PCF is different from Ong's model of Parigot's lambda-mu-calculus. His model works by adding new moves to the intuitionistic case while ours works by relaxing the game rules.
Type de document :
Communication dans un congrès
Philippe de Groote and J. Roger Hindley. Typed Lambda Calculi and Applications 1997, Apr 1997, Nancy, France. Springer, 1210, pp.214--230, 1997, Lecture Notes in Computer Science. 〈10.1007/3-540-62688-3〉
Liste complète des métadonnées

Littérature citée [13 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00381542
Contributeur : Hugo Herbelin <>
Soumis le : mardi 5 mai 2009 - 17:11:53
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : jeudi 10 juin 2010 - 22:47:06

Fichiers

tlca-Her97-classical-games.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Hugo Herbelin. Games and Weak-Head Reduction for Classical PCF. Philippe de Groote and J. Roger Hindley. Typed Lambda Calculi and Applications 1997, Apr 1997, Nancy, France. Springer, 1210, pp.214--230, 1997, Lecture Notes in Computer Science. 〈10.1007/3-540-62688-3〉. 〈inria-00381542〉

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

105