Rice's Theorem under Self-Modification: Elevation Operators and a Normal Form

Abstract

We ask whether it can be certified algorithmically that a self-modifying program keeps a behavioural property, a safety property in the motivating case, after its next rewrite (preservation) and along its whole evolution (persistence). When the rewrite depends only on behaviour, preservation is a behavioural property and Rice's theorem applies. When the rewrite reads the code, preservation is no longer behavioural; yet, under a uniform disruption condition, the s-m-n reduction that proves Rice's theorem works inside a single class of behaviourally identical programs, and preservation inherits the degree of the halting problem. One step never exceeds the degree of the property, while persistence can climb one level of the arithmetical hierarchy. We then isolate the mechanism shared by rewriting, supervision and system comparison, the elevation operator, and prove a normal form: the preserving set is determined by a single finite trigger and a polarity, and the Rice-Shapiro theorem restricts the polarity to the arithmetical class of the property. Runtime monitors, consistency supervision, conformance to a reference and observational equivalence are instances, and no sound theory covers the preserving systems.

v3: journal version. Shortened; neutral terminology; new Proposition 7.12 showing that the class of elevation operators is complete for anchored normal forms; comparison with enforcement by program rewriting (Hamlen, Morrisett and Schneider) added; illustrations moved to an appendix. 35 pages. Companion paper: arXiv:2606.28639 (applied consequences)