[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

Am 28/05/2013 23:53, schrieb Makarius:
> On Tue, 28 May 2013, Tobias Nipkow wrote:
> 
>> Am 28/05/2013 13:34, schrieb Lawrence Paulson:
>>> Historical note: when the original high-order unification code was written,
>>> there was no user-level polymorphism. If my memory is correct, the TVar
>>> constructor did not even exist. Polymorphism was only used for type inference
>>> in terms.
>>
>> correct. i added that part of the code in about 1990. of course i never proved
>> anything about it.
> 
> The complexity of the implementation is one thing, but how about the algorithmic
> ideas?
> 
> Is "Huet + schematic polymorphism" and "Miller + schematic polymorphism"
> sufficiently well-understood to make a nice formalization from that? Lets say
> with the de-Bruijn toolbox that Stefan had in his entry to POPLmark (which has
> the advantage that it is close to what is actually done in Isabelle/ML, unlike
> Nominal datatypes).

definitely a nice project, but not easy. full hou does not terminate to start
with, and termination of pattern unification is tricky. hence a relational
rather than a functional formalisation suggests itself. i agree, de bruijn.

tobias

> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev