[plt-scheme] Check for function equality?

One can explain this without resort to Turing machines or other automata!

Here's how you might do it.

Imagine you had a function called "halts":

  ;; halts? : program input -> boolean
  ;; returns true when the program halts on the given input
  ;; returns false when the program would fail to halt on the given input
  ;; always returns something.

Now consider this function:

  (define (als-program x)
    (cond
      [(halts? x x) (als-program x)]
      [else 3]))

and ask what is

  (als-program als-program).

I'll let dave try to think this thru (it works best when you do it
yourself). Break it up into two cases based on what the conditional
does.

Once you've figured that out, let me know and then I'll answer you
question. (Yes, I know it is rude to answer a question with a
question, but hey, I'm rude.)

Robby

On Thu, Feb 19, 2009 at 5:26 PM, Marco Morazan <morazanm at gmail.com> wrote:
> On Thu, Feb 19, 2009 at 4:43 PM, dave yrueta <dyrueta at gmail.com> wrote:
>> Hi All --
>>
>> Is there a Scheme function similar to "check-expect" that tests for
>> equality between functions?
>>
>
> Some of my students (first year) asked the same question. As you may
> imagine by the answers you received so far, it is a tough question to
> answer. If you are a student that has not taken a course in automata
> theory, I happily suggest you do before trying to tackle your
> question. :-) If you are familiar with Turing Machines, then you know
> that the Halting Problem is unsolvable and you should be able to
> answer your question by reducing the Halting Problem to your problem.
> Assume you have a Turing Machine that can answer your question
> reliably. Show that if such a Turing Machine exists then you can solve
> the Halting Problem. Since we know that the Halting Problem is
> unsolvable, then that hypothetical Turing Machine that solves your
> problem can not exist. Q.E.D. ;-)
>
> The catch, of course, is the assumption that Turing Machines can be
> programmed to solve any solvable problem. Search for Church's Thesis
> for more details on that assumption.
>
> Others have suggested using theorem provers. This is also something
> that can lead you down an enlightening path. :-)
>
> --
>
> Cheers,
>
> Marco
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>