Document Open Access Logo

A Rice’s Theorem for Abstract Semantics

Authors Paolo Baldan , Francesco Ranzato , Linpeng Zhang

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.117.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Paolo Baldan
  • Dipartimento di Matematica, University of Padova, Italy
Francesco Ranzato
  • Dipartimento di Matematica, University of Padova, Italy
Linpeng Zhang
  • Department of Computer Science, University College London, UK

Funding

  • Baldan, Paolo: Partially funded by University of Padova, under the SID2018 project "Analysis of STatic Analyses (ASTA)"; Italian Ministry of University and Research, under the PRIN2017 project no. 201784YSZ5 "AnalysiS of PRogram Analyses (ASPRA)".
  • Ranzato, Francesco: Partially funded by University of Padova, under the SID2018 project "Analysis of STatic Analyses (ASTA)"; Italian Ministry of University and Research, under the PRIN2017 project no. 201784YSZ5 "AnalysiS of PRogram Analyses (ASPRA)"; Facebook Research, under a "Probability and Programming Research Award".

Acknowledgements

We are grateful to Roberto Giacobazzi for thorough discussions and comments.

Cite AsGet BibTex

Paolo Baldan, Francesco Ranzato, and Linpeng Zhang. A Rice’s Theorem for Abstract Semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 117:1-117:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ICALP.2021.117

Abstract

Classical results in computability theory, notably Rice’s theorem, focus on the extensional content of programs, namely, on the partial recursive functions that programs compute. Later and more recent work investigated intensional generalisations of such results that take into account the way in which functions are computed, thus affected by the specific programs computing them. In this paper, we single out a novel class of program semantics based on abstract domains of program properties that are able to capture nonextensional aspects of program computations, such as their asymptotic complexity or logical invariants, and allow us to generalise some foundational computability results such as Rice’s Theorem and Kleene’s Second Recursion Theorem to these semantics. In particular, it turns out that for this class of abstract program semantics, any nontrivial abstract property is undecidable and every decidable overapproximation necessarily includes an infinite set of false positives which covers all values of the semantic abstract domain.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computability
  • Theory of computation → Recursive functions
  • Theory of computation → Abstraction
Keywords
  • Computability Theory
  • Recursive Function
  • Rice’s Theorem
  • Kleene’s Second Recursion Theorem
  • Program Analysis
  • Affine Program Invariants

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Andrea Asperti. The intensional content of Rice’s theorem. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, page 113–119, New York, NY, USA, 2008. ACM. URL: https://doi.org/10.1145/1328438.1328455.
  2. Manuel Blum. A machine-independent theory of the complexity of recursive functions. J. ACM, 14(2):322–336, April 1967. URL: https://doi.org/10.1145/321386.321395.
  3. Manuel Blum. On effective procedures for speeding up algorithms. J. ACM, 18(2):290–305, April 1971. URL: https://doi.org/10.1145/321637.321648.
  4. Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic. Abstract extensionality: on the properties of incomplete abstract interpretations. Proceedings of the ACM on Programming Languages (POPL 2020), 4:1-28, December 2020. URL: https://doi.org/10.1145/3371096.
  5. Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157-1210, 2010. URL: https://doi.org/10.3233/JCS-2009-0393.
  6. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM Symp. on Principles of Programming Languages (POPL 1977). ACM, 1977. URL: https://doi.org/10.1145/512950.512973.
  7. Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato. Program analysis is harder than verification: A computability perspective. In Proc. Int. Conf. on Computer Aided Verification (CAV 2018), pages 75-95. Springer, 2018. Google Scholar
  8. Nigel Cutland. Computability: An Introduction to Recursive Function Theory. Cambridge University Press, 1980. URL: https://doi.org/10.1017/CBO9781139171496.
  9. Matthew S. Hecht. Flow Analysis of Computer Programs. Elsevier, 1977. Google Scholar
  10. Mathieu Hoyrup. The decidable properties of subrecursive functions. In Proc. Int. Coll. on Automata, Languages and Programming (ICALP 2016), volume 55 of LIPIcs, pages 108:1-108:13, 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.108.
  11. Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. Polynomial invariants for affine programs. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2018), page 530–539, New York, NY, USA, 2018. ACM. URL: https://doi.org/10.1145/3209108.3209142.
  12. John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Informatica, 7:305-317, 1977. URL: https://doi.org/10.1007/BF00290339.
  13. Michael Karr. Affine relationships among variables of a program. Acta Inf., 6:133-151, 1976. URL: https://doi.org/10.1007/BF00268497.
  14. Dexter Kozen. Indexings of subrecursive classes. Theor. Comput. Sci., 11:277-301, 1980. URL: https://doi.org/10.1016/0304-3975(80)90017-1.
  15. Gerhard Lischke. Über die erfüllung gewisser erhaltungssätze durch kompliziertheitsmasse. Mathematical Logic Quarterly, 21(1):159-166, 1975. URL: https://onlinelibrary.wiley.com/doi/abs/10.1002/malq.19750210121.
  16. Gerhard Lischke. Natürliche kompliziertheitsmasze und erhaltungssätze I. Mathematical Logic Quarterly, 22(1):413-418, 1976. URL: https://doi.org/10.1002/malq.19760220150.
  17. Gerhard Lischke. Natürliche kompliziertheitsmasze und erhaltungssätze II. Mathematical Logic Quarterly, 23(13‐15):193-200, 1977. URL: https://doi.org/10.1002/malq.19770231302.
  18. Antoine Miné. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends in Programming Languages, 4(3-4):120-372, 2017. URL: https://doi.org/10.1561/2500000034.
  19. Jean-Yves Moyen and Jakob Grue Simonsen. More intensional versions of Rice’s theorem. In Proc. Computability in Europe (CIE 2019), Computing with Foresight and Industry, pages 217-229. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-22996-2_19.
  20. Markus Müller-Olm and Helmut Seidl. A note on Karr’s algorithm. In Proc. Int. Coll. on Automata, Languages and Programming (ICALP 2004), pages 1016-1028. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27836-8_85.
  21. Markus Müller-Olm and Helmut Seidl. Precise interprocedural analysis through linear algebra. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2004), page 330–341, New York, NY, USA, 2004. ACM. URL: https://doi.org/10.1145/964001.964029.
  22. Piergiorgio Odifreddi. Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers. Sole Distributors for the Usa and Canada, Elsevier Science Pub. Co., 1989. Google Scholar
  23. Francesco Ranzato. Decidability and synthesis of abstract inductive invariants. In Proc. 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of LIPIcs, pages 30:1-30:21, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.30.
  24. John H. Reif and Harry R. Lewis. Symbolic evaluation and the global value graph. In Proc. 4th ACM Symp. on Principles of Programming Languages (POPL 1977), pages 104-118. ACM, 1977. URL: https://doi.org/10.1145/512950.512961.
  25. H.G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74:358–366, 1953. URL: https://doi.org/10.2307/1990888.
  26. Xavier Rival and Kwangkeun Yi. Introduction to Static Analysis – An Abstract Interpretation Perspective. MIT Press, 2020. Google Scholar
  27. Hartley Rogers. Gödel numberings of partial recursive functions. Journal of Symbolic Logic, 23(3):331–341, 1958. URL: https://doi.org/10.2307/2964292.
  28. Hartley Rogers. Theory of Recursive Functions and Effective Computability. Higher Mathematics Series. McGraw-Hill, 1967. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact