# [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.