Intensional Kleene and Rice theorems for abstract program semantics

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 work investigated intensional generalisations of such results that take into account the way in which function...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2022-11, Vol.289, p.104953, Article 104953
Main Authors: Baldan, Paolo, Ranzato, Francesco, Zhang, Linpeng
Format: Article
Language:English
Subjects:
Affine program invariants
Computability theory
Kleene's second recursion theorem
Program analysis
Recursive function
Rice's theorem
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 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 over-approximation necessarily includes an infinite set of false positives which covers all the values of the semantic abstract domain.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2022.104953