Games and Weak-Head Reduction for Classical PCF - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 1997

Games and Weak-Head Reduction for Classical PCF

Résumé

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.
Fichier principal
Vignette du fichier
tlca-Her97-classical-games.pdf (242.19 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00381542 , version 1 (05-05-2009)

Identifiants

Citer

Hugo Herbelin. Games and Weak-Head Reduction for Classical PCF. Typed Lambda Calculi and Applications 1997, Apr 1997, Nancy, France. pp.214--230, ⟨10.1007/3-540-62688-3⟩. ⟨inria-00381542⟩
85 Consultations
195 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More