Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00381542
Contributor : Hugo Herbelin <>
Submitted on : Tuesday, May 5, 2009 - 5:11:53 PM
Last modification on : Wednesday, December 9, 2020 - 3:10:47 PM
Long-term archiving on: : Thursday, June 10, 2010 - 10:47:06 PM

Files

tlca-Her97-classical-games.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

298

Files downloads

730