[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