[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

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