[plt-scheme] The perfect teaching language--Is this too much to ask for?
On Jun 15, 2009, at 2:29 PM, Bill Wood wrote:
> On Mon, 2009-06-15 at 13:10 -0400, Stephen Bloch wrote:
> . . .
>> I'll have to think about this: "type" as a type still seems so
>> elegant, so expressively efficient :-) My naive first impulse is to
>> suggest a consistent but incomplete static type-checker that never
>> misclassifies something's type, correctly classifies the types of
>> MOST expressions in practice, and when it can't, knows when to give
>> up so it at least terminates. Has somebody already proven that
>> that's unattainable too?
>
> Just a shot in the dark here: This seems to be similar to the
> question
> of the existence of decision procedures for classical predicate
> calculi.
> IIRC Goedel showed that first-order PC had no decision procedure but
> Herbrand showed there was a semi-decision procedure -- one that always
> halted on theorems but that might spin attempting to find a
> counter-example to a non-theorem (the non-theorem may have no finite
> counter-examples but have an infinite one). As I understand it
> second-order PC, however, does not have even a semi-decision
> procedure,
> for if it did it could be used to build a decision procedure for FOPC.
>
> If something analogous holds for intuitionistic PC (the logic involved
> in the Curry-Howard Correspondence) then might it defeat your
> incomplete
> type-checker?
Let's think of this for a moment as not a general proof system but
just a "type-of" function. I'm putting priority on termination and
correctness at the expense of specificity: the function will always
return in finite time, and will always return a supertype of the
correct type, but not necessarily the narrowest type that could
possibly be inferred. This is certainly possible, if nothing else by
setting an alarm clock and returning type "any" if the alarm goes off
before the algorithm manages to prove some more specific type. The
question is whether you could get it to give useful answers "most" of
the time "in practice" within a reasonable time bound.
Back in the proof world, I'm not asking for a complete decision
procedure (recursive), nor even a semi-decision procedure (r.e.), but
rather a terminating algorithm that, on any given theorem, produces a
proof of either this theorem or something weaker (in the sense of
being implied by the given theorem). Theoretically, this is trivial:
the algorithm always produces a proof of "1=1". In practice, you
would want it to prove either the theorem itself or something "not
much weaker" "most" of the time. And logic has nothing to tell us
about such fuzzy criteria :-)
Stephen Bloch
sbloch at adelphi.edu