Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2015: Programming Languages and Systems pp 313–331Cite as

Decision Algorithms for Checking Definability of Order-2 Finitary PCF

  • Conference paper
  • First Online:

  • 675 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9458))

Abstract

We consider a definability problem for finitary PCF, which asks whether, given a function (as an element of a cpo), there exists a term of finitary PCF whose interpretation is the function. The definability problem for finitary PCF is known to be decidable for types of order at most 2. However, its complexity and practical algorithms have not been well studied. In this paper, we give two algorithms for checking definability: one based on Sieber’s sequentiality relation, which runs in quadruply exponential time for the size of the type of the given function, and the other based on a saturation method, which runs in triply exponential time for the size. With the recent advance of higher-order model checking, our result may be useful for implementing a tool for deciding observational equivalence between finitary PCF terms of types of order at most 3.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    We thank an anonymous reviewer for providing us the information of Stoughton’s work.

  2. 2.

    A function f between pointed cpos is continuous if f is monotonic and preserves the least upper bound of any directed subset. Note that, if f is a function between finite cpos, f is continuous if and only if f is monotonic.

  3. 3.

    A cartesian product of two cpos \(D_1=(S_1,\le _1)\) and \(D_2=(S_2,\le _2)\) is a cpo \((S_1\times S_2,\le _{D_1 \times D_2})\) where \((d_1,d_2)\le _{D_1 \times D_2}(d_1^{\prime },d_2^{\prime }) \mathop {\Longleftrightarrow }\limits ^{\mathrm {def}}d_1 \le _1 d_1^{\prime }\wedge d_2 \le _2 d_2^{\prime }\).

References

  1. Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  2. Abramsky, S., McCusker, G.: Call-by-value games. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 1–17. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. Amadio, R.M., Curien, P.L.: Domains and Lambda-Calculi. Cambridge University Press, Cambridge (1998)

    Book  MATH  Google Scholar 

  4. Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013. LIPIcs, vol. 23, pp. 129–148 (2013)

    Google Scholar 

  5. Hopkins, D., Murawski, A.S., Ong, C.-H.L.: Hector: an equivalence checker for a higher-order fragment of ML. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 774–780. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Hopkins, D., Murawski, A.S., Ong, C.-H.L.: A fragment of ML decidable by visibly pushdown automata. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 149–161. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Hopkins, D., Ong, C.-H.L.: Homer: a higher-order observational equivalence model checkER. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 654–660. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Hyland, J.M.E., Ong, C.-H.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  9. Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3), 1–62 (2013)

    Article  MathSciNet  Google Scholar 

  10. Loader, R.: The undecidability of lambda-definability. In: The Church Festschrift. CSLI/University of Chicago Press (1994)

    Google Scholar 

  11. Loader, R.: Finitary PCF is not decidable. Theor. Comput. Sci. 266(1), 341–364 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  12. Milner, R.: Fully abstract models of typed \(\lambda \)-calculi. Theor. Comput. Sci. 4(1), 1–22 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  13. Murawski, A.S.: On program equivalence in languages with ground-type references. In: Proceedings of LICS 2003, pp. 108–108. IEEE (2003)

    Google Scholar 

  14. Murawski, A.S.: Functions with local state: regularity and undecidability. Theor. Comput. Sci. 338(1–3), 315–349 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  15. Murawski, A.S., Walukiewicz, I.: Third-order Idealized Algol with iteration is decidable. Theor. Comput. Sci. 390(2–3), 214–229 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  16. Ong, C.-H.L.: Observational equivalence of 3rd-order Idealized Algol is decidable. In: Proceedings of LICS 2002, pp. 245–256. IEEE (2002)

    Google Scholar 

  17. Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81–90. IEEE (2006)

    Google Scholar 

  18. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  19. Plotkin, G.D.: Lambda-definability and logical relations. Technical report, SAI-RM-4, School of Artificial Intelligence, University of Edinburgh (1973)

    Google Scholar 

  20. Plotkin, G.D.: Lambda-definability in the full type hierarchy. To HB Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 363–373 (1980)

    Google Scholar 

  21. Ramsay, S.J., Neatherway, R., Ong, C.-H.L.: An abstraction refinement approach to higher-order model checking. In: Proceedings of POPL 2014, pp. 61–72. ACM (2014)

    Google Scholar 

  22. Reynolds, J.C.: The essence of Algol. In: O’Hearn, P.W., Tennent, R.D. (eds.) ALGOL-like Languages. Progress in Theoretical Computer Science, pp. 67–88. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  23. Sieber, K.: Reasoning about sequential functions via logical relations. In: Applications of Categories in Computer Science. London Mathematical Society Lecture Note Series, vol. 177, pp. 258–269. Cambridge University Press (1992)

    Google Scholar 

  24. Stoughton, A.: Mechanizing logical relations. In: Main, M.G., Melton, A.C., Mislove, M.W., Schmidt, D., Brookes, S.D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 359–377. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  25. Winskel, G.: Formal Semantics of Programming Languages. The MIT Press, Cambridge (1993)

    MATH  Google Scholar 

Download references

Acknowledgments

We thank anonymous reviewers for useful comments. This work was partially supported by JSPS Kakenhi 15H05706, and 23220001.

Author information

Authors and Affiliations

  1. The University of Tokyo, Tokyo, Japan

    Sadaaki Kawata, Kazuyuki Asada & Naoki Kobayashi

Authors
  1. Sadaaki Kawata
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kazuyuki Asada
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Naoki Kobayashi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sadaaki Kawata .

Editor information

Editors and Affiliations

  1. Univ. of Science and Technology of China, Hefei, Anhui, China

    Xinyu Feng

  2. Pohang Univ. of Science and Technology, Nam-Gu, Pohang, Korea (Republic of)

    Sungwoo Park

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Kawata, S., Asada, K., Kobayashi, N. (2015). Decision Algorithms for Checking Definability of Order-2 Finitary PCF. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-26529-2_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-26528-5

  • Online ISBN: 978-3-319-26529-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation