skip to main content
research-article

Full abstraction for nominal Scott domains

Published: 23 January 2013 Publication History

Abstract

We develop a domain theory within nominal sets and present programming language constructs and results that can be gained from this approach. The development is based on the concept of orbit-finite subset, that is, a subset of a nominal sets that is both finitely supported and contained in finitely many orbits. This concept appears prominently in the recent research programme of Bojanczyk et al. on automata over infinite languages, and our results establish a connection between their work and a characterisation of topological compactness discovered, in a quite different setting, by Winskel and Turner as part of a nominal domain theory for concurrency. We use this connection to derive a notion of Scott domain within nominal sets. The functionals for existential quantification over names and `definite description' over names turn out to be compact in the sense appropriate for nominal Scott domains. Adding them, together with parallel-or, to a programming language for recursively defined higher-order functions with name abstraction and locally scoped names, we prove a full abstraction result for nominal Scott domains analogous to Plotkin's classic result about PCF and conventional Scott domains: two program phrases have the same observable operational behaviour in all contexts if and only if they denote equal elements of the nominal Scott domain model. This is the first full abstraction result we know of for higher-order functions with local names that uses a domain theory based on ordinary extensional functions, rather than using the more intensional approach of game semantics.

Supplementary Material

JPG File (r1d1_talk3.jpg)
MP4 File (r1d1_talk3.mp4)

References

[1]
URL http://www.citeulike.org/group/11951/.
[2]
S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51: 1--77, 1991.
[3]
S. Abramsky, D. R. Ghica, A. S. Murawski, C.-H. L. Ong, and I. D. B. Stark. Nominal games and full abstraction for the nu-calculus. In Proc. LICS 2004, pages 150--159. IEEE Computer Society Press, 2004.
[4]
S. Abramsky, R. Jagadeesan, and P. Malacaria. Full abstraction for PCF. Information and Computation, 163 (2): 409--470, 2000.
[5]
S. Abramsky and A. Jung. Domain theory. In Handbook of Logic in Computer Science, Volume 3. Semantic Structures, chapter 1. Oxford University Press, 1994.
[6]
M. Bojanczyk, L. Braud, B. Klin, and S. Lasota. Towards nominal computation. In Proc. POPL 2012, pages 401--412. ACM Press, 2012.
[7]
M. Bojanczyk, B. Klin, and S. Lasota. Automata with group actions. In Proc. LICS 2011, pages 355--364. IEEE Computer Society Press, 2011.
[8]
M. Bojanczyk and S. Lasota. A machine-independent characterization of timed languages. In Proc. ICALP 2012, Part II, volume 7392 of LNCS, pages 92--103. Springer-Verlag, 2012.
[9]
V. Ciancia and U. Montanari. Symmetries, local names and dynamic (de)-allocation of names. Information and Computation, 208 (12): 1349--1367, 2010.
[10]
P.-L. Curien. Definability and full abstraction. In Computation, Meaning and Logic, Articles dedicated to Gordon Plotkin, volume 172 of ENTCS, pages 301--310. Elsevier, 2007.
[11]
M. J. Gabbay. A study of substitution, using nominal techniques and Fraenkel-Mostowski sets. Theoretical Computer Science, 410 (12--13): 1159--1189, 2009.
[12]
M. J. Gabbay. Foundations of nominal techniques: Logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic, 17 (2): 161--229, 2011.
[13]
M. J. Gabbay and V. Ciancia. Freshness and name-restriction in sets of traces with names. In Proc. FOSSACS 2011, volume 6604 of LNCS, pages 365--380. Springer-Verlag, 2011.
[14]
M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13: 341--363, 2002.
[15]
F. Gadducci, M. Miculan, and U. Montanari. About permutation algebras, (pre)sheaves and named sets. Higher-Order Symb. Computation, 19: 283--304, 2006.
[16]
J. M. E. Hyland and C.-H. L. Ong. On full abstraction for PCF: I, II and III. Information and Computation, 163 (2): 285--408, 2000.
[17]
P. T. Johnstone. Sketches of an Elephant, A Topos Theory Compendium, Volumes 1 and 2. Number 43--44 in Oxford Logic Guides. Oxford University Press, 2002.
[18]
J. Laird. A game semantics of names and pointers. Annals of Pure and Applied Logic, 151 (2): 151--169, 2008.
[19]
S. Lösch and A. M. Pitts. Relating Two Semantics of Locally Scoped Names. In Proc. CSL 2011, volume 12 of Leibniz International Proceedings in Informatics (LIPIcs), pages 396--411, 2011.
[20]
G. Markowsky. Chain-complete p.o. sets and directed sets with applications. Algebra Universalis, 6: 53--68, 1976.
[21]
E. Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90--113, Department of Computer Science, University of Edinburgh, 1989.
[22]
U. Montanari and M. Pistore. π-Calculus, structured coalgebras and minimal HD-automata. Proc. MFCS 2000, volume 1893 of phLNCS, pages 569--578. Springer-Verlag, 2000.
[23]
A. S. Murawski and N. Tzevelekos. Algorithmic games for full ground references. In Proc. ICALP 2012, Part II, volume 7392 of LNCS, pages 312--324. Springer-Verlag, 2012.
[24]
M. Odersky. A functional theory of local names. In Proc. POPL 1994, pages 48--59. ACM Press, 1994.
[25]
A. M. Pitts. Nominal logic, a first order theory of names and binding. Information and Computation, 186: 165--193, 2003.
[26]
A. M. Pitts. Alpha-structural recursion and induction. Journal of the ACM, 53: 459--506, 2006.
[27]
A. M. Pitts. Structural recursion with locally scoped names. Journal of Functional Programming, 21 (3): 235--286, 2011.
[28]
A. M. Pitts and M. J. Gabbay. A metalanguage for programming with bound names modulo renaming. MPC 2000, volume 1837 of LNCS, pages 230--255. Springer-Verlag, 2000.
[29]
A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What's new? MFCS 1993, volume 711 of LNCS, pages 122--141. Springer-Verlag, 1993.
[30]
G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5: 223--255, 1977.
[31]
F. Pottier. Static name control for FreshML. LICS 2007, pages 356--365. IEEE Computer Society Press, 2007.
[32]
D. S. Scott. Domains for denotational semantics. ICALP 1982, volume 140 of phLNCS, pages 577--613. Springer-Verlag, 1982.
[33]
M. R. Shinwell. The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, University of Cambridge, 2005.
[34]
M. R. Shinwell and A. M. Pitts. On a monadic semantics for freshness. Theoretical Computer Science, 342: 28--55, 2005.
[35]
M. R. Shinwell, A. M. Pitts, and M. J. Gabbay. FreshML: Programming with binders made simple. ICFP 2003, pages 263--274. ACM Press, 2003.
[36]
I. D. B. Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, Dec. 1994.
[37]
S. Staton. Name-Passing Process Calculi: Operational Models and Structural Operational Semantics. PhD thesis, University of Cambridge, 2007.
[38]
T. Streicher. Domain-Theoretic Foundations of Functional Programming. World Scientific, Singapore, 2006.
[39]
D. C. Turner. Nominal Domain Theory for Concurrency. PhD thesis, University of Cambridge, 2009.
[40]
D. C. Turner and G. Winskel. Nominal domain theory for concurrency. CSL 2009, volume 5771 of LNCS, pages 546--560. Springer-Verlag, 2009.
[41]
N. Tzevelekos. Nominal Game Semantics. PhD thesis, University of Oxford, 2008.
[42]
N. Tzevelekos. Fresh-register automata. POPL 2011, pages 295--306. ACM Press, 2011.
[43]
N. Tzevelekos. Program equivalence in a simple language with state. Computer Languages, Systems and Structures, 38 (2): 181--198, 2012.

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. denotational semantics
  2. domain theory
  3. full abstraction
  4. nominal sets
  5. symmetry

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)2
  • Downloads (Last 6 weeks)0
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media