Am 30/05/2013 15:11, schrieb Lawrence Paulson: > I know that there have been a lot of other papers on higher-order unification > expressed as an inference system. Maybe Dale Miller knows more about this > work.
I do follow that literature and haven't seen anything relevant on pattern unification. Having had another look at my paper on the algorithm in the clear light of day I realize why: there is no conceptual issue after all. The algorithm does not need the types, it works for untyped terms. Hence the extension to Isabelle's typed terms merely involves unifying types as you go along. I had another look at the code an it seems to do enough type unification, assuming the two start terms have the same type. Hence I must concur with you: although worthwhile, such a verification would not be "significant in a wider context", as you put it. Tobias > Larry > > On 30 May 2013, at 13:04, Tobias Nipkow <[email protected]> wrote: > >> >> Am 30/05/2013 13:49, schrieb Tobias Nipkow: >>> Am 30/05/2013 13:41, schrieb Lawrence Paulson: >>>> The only question is whether Isabelle is important enough for such work to >>>> be seen as significant in a wider context. >>> >>> Makarius is right, the interaction of schematic type variables and HOU has >>> never >>> been nailed down properly and would be of interest to a larger community. >> >> Correction: my CTRS 90 paper contains a pen-and-paper formalisation of the >> full >> HOU algorithm expressed as transformation rules, but without proofs. It is >> the >> pattern unification algorithm where the polymorphic case seems not to have >> been >> examined in any detail (except probably in my head at the time). >> >> Tobias >> >>> Tobias >>> _______________________________________________ >>> isabelle-dev mailing list >>> [email protected] >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >>> >> _______________________________________________ >> isabelle-dev mailing list >> [email protected] >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
