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 build 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 Bhö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.

This research was partly supported by ESPRIT Basic Research Action “Types for Proofs and Programs” and by Programme de Recherche Coordonnées “Mécanisation du raisonnement”.