Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Schematic type variable


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

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

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC