A Concrete Representation of Observational Equivalence for PCF
Martin Churchill, James Laird, Guy McCusker
TL;DR
This paper introduces a concrete representation of observational equivalence in PCF using game semantics, simplifying the identification of indistinguishable strategies and terms.
Contribution
It provides a new representation of innocent strategies that directly equates observationally equivalent PCF terms, avoiding complex quantifications.
Findings
Representation of innocent strategies that captures observational equivalence
Simplifies the process of identifying equivalent PCF terms
Bridges game semantics with concrete term equivalence
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Parallel Computing and Optimization Techniques · Formal Methods in Verification