Email Gateway (Aug 19 2022 at 08:29): Email Gateway (Aug 19 2022 at 08:29):From: John Munroe <munddr@gmail.com>
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
Email Gateway (Aug 19 2022 at 08:29):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: Nov 21 2024 at 12:39 UTC