Generalizations of Rice's theorem, applicable to executable and non-executable formalisms

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review


We formulate and prove two Rice-like theorems that characterize limitations on nameability of properties within a given naming scheme for partial functions. Such a naming scheme can, but need not be, an executable formalism. A programming language is an example of an executable naming scheme, where the program text names the partial function it implements. Halting is an example of a property that is not nameable in that naming scheme. The proofs reveal requirements on the naming scheme to make the characterization work. Universal programming languages satisfy these requirements, but also other formalisms can satisfy them. We present some non-universal programming languages and a non-executable specification language satisfying these requirements. Our theorems have Turing's well-known Halting Theorem and Rice's Theorem as special cases, by applying them to a universal programming language or Turing Machines as naming scheme. Thus, our proofs separate the nature of the naming scheme (which can, but need not, coincide with computability) from the diagonal argument. This sheds further light on how far reaching and simple the `diagonal' argument is in itself.
Originele taal-2Engels
RedacteurenA. Voronkov
StatusGepubliceerd - 2012
Evenementconference; Turing-100. The Alan Turing Centenary -
Duur: 1 jan. 2012 → …

Publicatie series

NaamEPiC Series
ISSN van geprinte versie2040-557X


Congresconference; Turing-100. The Alan Turing Centenary
Periode1/01/12 → …
AnderTuring-100. The Alan Turing Centenary


Duik in de onderzoeksthema's van 'Generalizations of Rice's theorem, applicable to executable and non-executable formalisms'. Samen vormen ze een unieke vingerafdruk.

Citeer dit