Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Higher-order unification


view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 04:18 UTC