The intensional content of Rice's theorem

The proofs of major results of Computability Theory like Rice, Rice-Shapiro or Kleene's fixed point theorem hide more information of what is usually expressed in their respective statements. We make this information explicit, allowing to state stronger, complexity theoretic-versions of all these theorems. In particular, we replace the notion of extensional set of indices of programs, by a set of indices of programs having not only the same extensional behavior but also similar complexity (Complexity Clique). We prove, under very weak complexity assumptions, that any recursive Complexity Clique is trivial, and any r.e. Complexity Clique is an extensional set (and thus satisfies Rice-Shapiro conditions). This allows, for instance, to use Rice's argument to prove that the property of having polynomial complexity is not decidable, and to use Rice-Shapiro to conclude that it is not even semi-decidable. We conclude the paper with a discussion of "complexity-theoretic" ve...

• Type: Conference
• Year: 2008
• Where: POPL
• Authors: Andrea Asperti
• Keywords: Complexity Clique, Point Theorem, POPL 2008, Programming Languages, Satisfies Rice-shapiro Conditions