Editing Rice's theorem (section)

===Proof sketch===
Suppose, for concreteness, that we have an algorithm for examining a program ''p'' and determining infallibly whether ''p'' is an implementation of the squaring function, which takes an integer ''d'' and returns ''d''<sup>2</sup>.  The proof works just as well if we have an algorithm for deciding any other non-trivial property of program behavior (i.e. a semantic and non-trivial property), and is given in general below.

The claim is that we can convert our algorithm for identifying squaring programs into one that identifies functions that halt.  We will describe an algorithm that takes inputs ''a'' and ''i'' and determines whether program ''a'' halts when given input ''i''.

The algorithm for deciding this is conceptually simple: it constructs (the description of) a new program ''t'' taking an argument ''n'', which (1) first executes program ''a'' on input ''i'' (both ''a'' and ''i'' being hard-coded into the definition of ''t''), and (2) then returns the square of ''n''. If ''a''(''i'') runs forever, then ''t'' never gets to step (2), regardless of ''n''. Then clearly,  ''t'' is a function for computing squares if and only if step (1) terminates.  Since we have assumed that we can infallibly identify programs for computing squares, we can determine whether ''t'', which depends on ''a'' and ''i'', is such a program; thus we have obtained a program that decides whether program ''a'' halts on input ''i''.  Note that our halting-decision algorithm never executes ''t'', but only passes its description to the squaring-identification program, which by assumption always terminates; since the construction of the description of ''t'' can also be done in a way that always terminates, the halting-decision cannot fail to halt either.

  halts (a,i) {
    define t(n) {
      a(i)
      '''return''' n×n
    }
    '''return''' is_a_squaring_function(t)
  }

This method does not depend specifically on being able to recognize functions that compute squares; as long as ''some'' program can do what we are trying to recognize, we can add a call to ''a'' to obtain our ''t''. We could have had a method for recognizing programs for computing square roots, or programs for computing the monthly payroll, or programs that halt when given the input <code>"Abraxas"</code>; in each case, we would be able to solve the halting problem similarly.