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

共 21 条

[11] CURIEN PL, 2006, NOTES GAME SEMANTICS
[12] Dybjer P, 1996, LECT NOTES COMPUT SC, V1158, P120
[13] Formal neighbourhoods, combinatory Bohm trees, and untyped normalization by evaluation
Dybjer, Peter
Kuperberg, Denis
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2012, 163 (02) : 122 - 131
[14] Denotational aspects of untyped normalization by evaluation
Filinski, A
Rohde, HK
[J]. RAIRO-THEORETICAL INFORMATICS AND APPLICATIONS, 2005, 39 (03): : 423 - 453
[15] Categorical combinatorics for innocent strategies
Harmer, Russ
Hyland, Martin
Mellies, Paul-Andre
[J]. 22ND ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2007, : 379 - +
[16] Hyland JME, 2000, INFORM COMPUT, V163, P285, DOI [10.1006/inco.2000.2917, 10.1006/inco2000.2917]
[17] Lindstrom, 2012, EPISTEMOLOGY VERSUS, P215, DOI 10.1007/978-94-007-4435-611
[18] Games and full abstraction for FPC
McCusker, G
[J]. INFORMATION AND COMPUTATION, 2000, 160 (1-2) : 1 - 61
[19] A COINDUCTION PRINCIPLE FOR RECURSIVELY DEFINED DOMAINS
PITTS, AM
[J]. THEORETICAL COMPUTER SCIENCE, 1994, 124 (02) : 195 - 219
[20] Plotkin G. D., 1977, Theoretical Computer Science, V5, P223, DOI 10.1016/0304-3975(77)90044-5

← 1 2 3 →