[isabelle] Higher-order unification



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.