Re: [isabelle] Higher-order unification



Isabelle's higher-order unification algorithm is intentionally incomplete for
terms with schematic type variables because otherwise it would require another
dimension of search/backtracking/divergence. The effect is exactly what you
observed: instantiations with function types are not always found. But there is
no simple description of when the incompleteness manifests itself: the algorithm
does what it does. You second example works because you are just unifying a
variable with a term - it is hard to get that one wrong.

Tobias

Am 03/08/2012 06:24, schrieb John Munroe:
> Hi,
> 
> I have some questions about the higher-order unification algorithm.
> For the following:
> 
> axiomatization foo :: "real => real => real"
> ML {*
> val ptrm = @{cpat "(?f :: ?'a => ?'b) ?s"} |> term_of;
> val trm = @{term "foo a"};
> val mtchs = Unify.matchers @{theory} [(ptrm,trm)] |> Seq.list_of;
> *}
> 
> I don't get a match. But if the type of the pattern was ?'a => ?'b =>
> ?'c, I get a match. It looks like ?'b isn't transformed to become a
> function type here. However, if I match using:
> 
> axiomatization foo :: "real => real => real"
> ML {*
> val ptrm = @{cpat "(?f :: ?'a)"} |> term_of;
> val trm = @{term "foo"};
> val mtchs = Unify.matchers @{theory} [(ptrm,trm)] |> Seq.list_of;
> pretty_insts @{context} (map (fn x => (x,0)) mtchs)
> *}
> 
> I get a match. Now, it seems that ?'a would need to be unified to a
> function type in order for it to come up with a match. So when do
> schematic type variables unify to function types and when do they not?
> 
> Thanks
> 
> John
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.