[plt-scheme] Check for function equality?
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