# [isabelle] Infinite variable chasing

*To*: isabelle-users at cl.cam.ac.uk
*Subject*: [isabelle] Infinite variable chasing
*From*: Michael Chan <mchan at inf.ed.ac.uk>
*Date*: Thu, 14 Oct 2010 17:11:16 +0200
*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.9) Gecko/20100423 Thunderbird/3.0.4

Hello all,

`I'm having a problem with looking up the instantiation to a variable in
``a matcher with Envir.lookup. The particular matcher is:
`
ML{* fun rtac' rl i j st = (snd o Seq.chop j) (rtac rl i st) *}
schematic_lemma
fixes g :: "nat => nat"
shows "((?f :: (?'a => ?'b) => ?'c) ?s = ?v) = (g a = x) & Q ?f ?s ?v"
apply rule
apply(tactic {* rtac' refl 1 1712 *})
goal (1 subgoal):
1. Q (%a::?'a => nat. a (?f9 a)) (%b::?'a. g a) x
variables:
a, x :: nat
g :: nat => nat
?f9 :: (?'a => nat) => ?'a
Q ::
((?'a => nat) => nat) => (?'a => nat) => nat => bool
type variables:
?'a :: type

`If I lookup the instantiation to the variable ?s in this particular
``matcher, which here has the type ?'a => nat, I run into an infinite
``recursion. The infinite recursion seems to be caused by an infinite
``chasing of type variable assignment at Type.devar:
`

`(*chase variable assignments; if devar returns a type var then it must
``be unassigned*)
`fun devar tye (T as TVar v) =
(case lookup tye v of
SOME U => devar tye U
| NONE => T)
| devar _ T = T;
Put simply, there's no variable assignment for it to be chased.

`In the implementation, Envir.lookup indirectly invokes Type.equal_type,
``which checks over each type variable -- in this case, that's ?'a and
``?'b. ?'b is fine, and only ?'a is problematic. Now let's look at the tye:
`
val tye =
Branch2
(Branch2
(Empty, (("'a", 0), (["HOL.type"], "?'a")),
Empty),
(("'b", 0), (["HOL.type"], "RealDef.real")),
Branch2
(Empty,
(("'a", 1), (["HOL.type"], "RealDef.real")),
Empty))
: Type.tyenv

`If we call devar tye on (?'a, 0), we'll run into an infinite recursion
``because lookup tye (TVar ("'a", 0), ["HOL.type"])) also gives (TVar
``("'a", 0), ["HOL.type"])).
`
Why isn't the variable chasing procedure given a maximum depth?
Any help will be appreciated.
Michael
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*