Showing the function=? is impossible

Question

Here's a lab from a first-year computer science course, taught in Scheme: https://www.student.cs.uwaterloo.ca/~cs135/assns/a07/a07.pdf

At the end of the lab, it basically presents the halting problem, and shows that it is impossible to solve by introducing the function diagonal, which is defined as:

(define (diagonal x)
  (cond
     [(halting? x x) (eternity 1)]
     [else true]))

Where eternity is a non-terminating program defined as (define (eternity x) (eternity x)). What happens when you feed diagonal its own definition as input ... ?

This is all fairly standard stuff. Then, the lab says:

For a real challenge, definitively answer the question posed at the end of Exercise 20.1.3 of the text, with the interpretation that function=? consumes two lists representing the code for the two functions. This is the situation Church considered in his proof.

So the gist of it is that function=? takes two inputs. Each is a list, which represents the definition of a function, i.e. it is a list of the form (define (id args ...) body ...). We can assume that both functions are syntactically valid and will terminate for all inputs (without runtime errors). function=? returns true if and only if the two functions will always return the same result when given the same inputs. For example,

(function=? '(define (foo x) (* 2 x)) 
            '(define (bar x) (+ x x))) ; should return #t

(function=? '(define (foo x) (+ x 1)) 
            '(define (bar x) (+ x 2))) ; should return #f

Now, function=? is obviously impossible to write - the challenge is to prove it is impossible. I thought about this for a while, and the best solution I could come up with is the following:

(define (disprove-function=? x)
  ((lambda (snip)
     (let ((self (list 'define '(disprove-function=? x)
                       (list snip (list 'quote snip)))))
       (if (function=? self '(define (id x) x))
           (list x)
           x)))
   '(lambda (snip) 
      (let ((self (list 'define '(disprove-function=? x)
                        (list snip (list 'quote snip)))))
        (if (function=? self '(define (id x) x))
            (list x)
            x)))))

Basically, disprove-function=? uses standard quining techniques to generate its own source code (the variable self), and then asks function=? if it is equivalent to the identity function. If function=? says #f, then disprove-function=? will always behave like the identity function. Contradiction! If function=? says #t, then disprove-function=? will always behave differently from identity; in particular, it will behave like the list function. Contradiction! Thus, function=? can't exist. QED.

My question is: is there a more elegant way to approach this problem? My solution seems ... long and ugly. Not nearly as nice as the diagonal function for proving that the halting problem is unsolvable.

NB: Please give me answers and not hints! Even though this is a homework question, it is not my homework question: I don't go to this university! Further, as you can see from the lab, this question is under the Enhancements category and isn't worth marks, so even if you don't believe me, there is still no problem with just giving me an answer. Finally, I already have a solution, which I am pretty sure is right; I was just wondering if there was a better solution.

Answer 1

Using the halting problem seems like the good solution. Suppose you have a function red that takes the code of a function (or λ-term) (or a untyped function), reduces one step (or β-redex) in it and returns the code of the resulting function. Suppose also that you have a function normal that says if the term is in normal form.

In Turing machines language, red would be the computation of one step and normal would return true when we are in a final state.

Let's simulate the computation of $n$ steps, returning $43$ instead of $1$ if we reach the end of the computation:

(define (run t n)
  (if (= n 0) 1
    (if (normal t) 43
      (run (red t) (n-1)))))

Then we can decide if the execution of a term will terminate or not:

(define (one x) 1)
(define (terminate t) (not (function=? (run t) one)))

From that we can use the usual diagonal argument:

(define (loop x) (loop x))
(define (f x) (if (terminate (code-of-application x (quote x))) (loop 0) 1)
(f code-of-f)

If f terminates on code-of-f then (terminate (code-of-application code-of-f (quote code-of-f)) will return true and then f will loop on code-of-f. So it should loop. Then (terminate ...) should return false and f will terminate on code-of-f, contradiction.

Technicalities: one need to define a base language which is expressive enough to be able to write everything is written above. You then need red and normal which can be tougher than one can imagine. You need also the standard quine techniques: quote which, given the code of a term, returns a term representing the code of the term, code-of-application a b is easy and self-explanatory, and of course you need to write everything above internally to write code-of-f.

The lambda-calculus is surprisingly simple and expressive to both write all this down and to prove its correctness, which is why Church used it to solve Hilbert's tenth problem, but one can do it in a lot of languages, possibly in a simpler way, using language-specific quine tricks.