Email Gateway (Aug 18 2022 at 18:33): Email Gateway (Aug 18 2022 at 18:33):From: Steve Wong <s.wong.731@gmail.com>
Hi,
I'm experimenting with matching a pattern containing schematic type
variables and it'd be great if someone could clarify the following:
1) match "?x (?y::?'a)" against "(p::(nat=>nat) => nat) q"
ML {*
val trm = @{term "(p::(nat\<Rightarrow>nat) \<Rightarrow> nat) q "};
val pat = @{cpat "?x (?y::?'a)"} |> term_of;
val mtchs = Unify.matchers @{theory} [(pat,trm)] |> Seq.list_of;
*}
Unsurprisingly, I get a substitution with ?y::nat=>nat := q.
2) match "?x (?y::?'a) against "(p::nat=>nat) q"
Here, I don't get a substitution where ?y is instantiated to the function
p::nat=>nat. Why can't ?'a be instantiated to nat=>nat like in 1)? I get
that substitution when ?y::?'a=>?'b though.
Any help will be appreciated.
Steve
Email Gateway (Aug 18 2022 at 18:33):From: Lawrence Paulson <lp15@cam.ac.uk>
There may be a mistake in your question, since I would expect y to be instantiated to q, not p. However, as a general rule, a type variable cannot be instantiated to a function type during higher-order unification. The reason for this restriction is that otherwise the search space would be unmanageable. I believe it is relaxed when the unification is essentially first-order.
Larry Paulson
Email Gateway (Aug 18 2022 at 18:35):From: Makarius <makarius@sketis.net>
May this old thread on isabelle-dev helps:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg01173.html
Makarius
Last updated: Nov 21 2024 at 12:39 UTC