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-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev