Games and Weak-Head Reduction for Classical PCF

We present a game model for classical PCF, a nite version of PCF extended by a catch/throw mechanism. This model is build from E-dialogues, a kind of two-players game de ned by Lorenzen. In the E-dialogues for classical PCF, the strategies of the rst player are isomorphic to the Bohm trees of the language. We de ne 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 rein 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 di erent from Ong's model of Parigot's lambda-mu-calculus. His model works by addin...

• Type: Conference
• Year: 1997
• Where: TLCA
• Authors: Hugo Herbelin
• Keywords: Classical Pcf, Model, Theoretical Computer Science, TLCA 1997, Weak-head Reduction