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:
(deﬁne (diagonal x) (cond [(halting? x x) (eternity 1)] [else true]))
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, deﬁnitively 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
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)))))
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.