[plt-scheme] Check for function equality?

From: Stephen Bloch (sbloch at adelphi.edu)
Date: Mon Feb 23 13:29:06 EST 2009

On Feb 21, 2009, at 11:00 AM, David Yrueta wrote:

> I believe I may have brushed up against the "halting problem" in  
> university philosophy courses.  In this context, concepts  
> originating in mathematics or logic weren't explained or even  
> discussed with any seriousness, but instead were typically used as  
> arrows in the quivers of warring epistemologists launching  
> broadsides in the mind vs. matter war, much in the same manner and  
> spirit that philosophers in the 60's marshaled the Heisenberg  
> Principle against human determinism and in favor of "free  
> will" (cue eye rolling). The result was precisely as intended,  
> confirming the prejudice in liberal arts students like myself  
> against anything with a mathematical flavor, and discouraging any  
> real thought on the subject of these problems.

There was a trio of philosophically earthshaking results, all within  
about ten years of one another: Heisenberg's uncertainty principle,  
Goedel's incompleteness theorems, and Turing's proof of the  
undecidability of the Halting Problem.  All three are quoted by lay  
philosophers much more often than they're understood :-)

> By the way, has anyone out there used / heard of "Tarski's World."   
> It a logic study program.  I was thinking of taking it up with a  
> friend.

Yes, I've taught an undergraduate logic course a number of times  
using Tarski's World and the textbook _Language Proof and Logic_ (and  
its predecessors).  The book has a certain philosophical resemblance  
to HtDP, as follows:

In HtDP, we introduce a data type, then some patterns for how to test  
and code for that data type.  These patterns may be based on the type 
(s) of the function's input(s) (usually) or on the type of its output  
(occasionally).  Then introduce another data type (or another kind of  
data type) and repeat.  We do this in turn for images, strings,  
numbers, posns, structs in general, polymorphic data types, lists,  
and self-referential data types in general.

In _LP&L_, we introduce a logical connective, then patterns for how  
to use that connective in (formal and informal) proofs.  These  
patterns may be based on whether the connective appears in the  
hypotheses (input) of the proof, or in the desired conclusion  
(output) of the proof.  Then introduce another connective and  
repeat.  We do this in turn for AND/OR, NOT, IF-THEN, IFF, single  
quantifiers, and multiple quantifiers.

Stephen Bloch
sbloch at adelphi.edu

Posted on the users mailing list.