Game Semantics and Normalization by Evaluation

被引：2

作者：

Clairambault, Pierre ^{[1
]}

Dybjer, Peter ^{[2
]}

机构：

[1] Univ Lyon, CNRS, ENS Lyon, Inria,UCBL, Lyon, France

[2] Chalmers Tekniska Hogskola, Gothenburg, Sweden

来源：

FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2015) | 2015年 / 9034卷

关键词：

FULL ABSTRACTION; UNTYPED NORMALIZATION;

D O I：

10.1007/978-3-662-46678-0_4

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We show that Hyland and Ong's game semantics for PCF can be presented using normalization by evaluation (nbe). We use the bijective correspondence between innocent well-bracketed strategies and PCF B "ohm trees, and show how operations on PCF Bohm trees, such as composition, can be computed lazily and simply by nbe. The usual equations characteristic of games follow from the nbe construction without reference to low-level game-theoretic machinery. As an illustration, we give a Haskell program computing the application of innocent strategies.

引用

页码：56 / 70

页数：15