Intensional Kleene and Rice Theorems for Abstract Program Semantics

TL;DR

This paper introduces a new class of program semantics based on abstract domains that capture nonextensional aspects like complexity and invariants, generalizing Rice's and Kleene's theorems to these semantics.

Contribution

It defines a novel class of abstract program semantics and extends foundational computability results to include nonextensional properties of programs.

Findings

Nontrivial properties in this semantics are undecidable.

Decidable over-approximations include infinite false positives.

Generalization of Rice's and Kleene's theorems to abstract semantics.

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 over-approximation necessarily includes an infinite set of false positives which covers all the values of the semantic abstract domain.