2010/02/27 by Martin Churchill, Churchill, Martin, James Laird +3
Computer Science · #F.3.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO
paper · pdf · doi:10.48550/arxiv.1003.0107
A result on observational equivalence for PCF and innocent strategies, as presented at the Games for Logic and Programming Languages (GaLoP) workshop in York, March 2009
The full abstraction result for PCF using game semantics requires one to identify all innocent strategies that are innocently indistinguishable. This involves a quantification over all innocent tests, cf. quantification over all innocent contexts. Here we present a representation of innocent strategies that equates innocently indistinguishable ones, yielding a representation of PCF terms that equates precisely those terms that are observational equivalent.