<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Oct 13, 2014 at 12:51 AM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
This looks pretty bad, because it seems like the variable x has got<br>
captured. But if you give the opentheory tool the global option<br>
--show-var-types it will annotate every term variable with its type,<br>
and now the before stack is<br>
<br>
    [|- (!(x : B). (P : B -> bool) (x : B) ==> (Q : bool)) ==><br>
        (?) (P : B -> bool) ==> (Q : bool),<br>
     [[],<br>
      [[(P : B -> bool), \(y : B). (p : A -> B -> bool) (x : A) (y : B)],<br>
       [(Q : bool),<br>
        ?(y : B) (x : A). (p : A -> B -> bool) (x : A) (y : B)]]], ...<br>
<br>
and the after stack is<br>
<br>
    [|- (!(x : B).<br>
           (let (y : B) <- (x : B) in<br>
            (p : A -> B -> bool) (x : A) (y : B)) ==><br>
           ?(y : B) (x : A). (p : A -> B -> bool) (x : A) (y : B)) ==><br>
        (?(y : B). (p : A -> B -> bool) (x : A) (y : B)) ==><br>
        ?(y : B) (x : A). (p : A -> B -> bool) (x : A) (y : B), ...<br>
<br>
which makes it clear that there are two variables with name "x" but<br>
having different types, which according to the rules of higher order<br>
logic makes them distinct. The article standard contains the words<br>
<br>
"Variables are identified by name and type."<br>
<br>
but should probably make this point far more explicit.<br>
<br>
Anyway, your reader's strategy of renaming the bound variable to a new<br>
name is safe (if not necessary in this case) and so it doesn't solve<br>
your problem.<br></blockquote><div><br></div><div>Actually, you put your finger right on the issue. I tried changing equality for Vars so that it checks both name and type, instead of just name, and now it rips through the whole file without error. I think the error lies not in this part, since the dummy rename isn't important, but rather later when the inner x in \x. ((\y. (x p y) x) is identified as bound instead of free, which then causes problems in the alpha-equivalence.<br></div><div> <br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
As to your last question, the only article readers I know of have been<br>
implemented in Standard ML, Ocaml and Haskell, so there is no<br>
imperative reference available. Perhaps you are writing one!<br></blockquote><div><br></div><div>I intend to write a translator from OpenTheory to Metamath [<a href="http://us.metamath.org/index.html">http://us.metamath.org/index.html</a>]. Although the main theorem collection is based on and FOL+ZFC foundation, the basic language supports arbitrary syntax, and I've drafted an axiom set that appears to be sufficient to model HOL (based on HOL Light's axioms).  However, Metamath does not support proper substitution but rather a form of direct substitution coupled with distinct variable conditions on the substitutions (meaning that even bound occurrences are not allowed). This makes the implementation much simpler, and it's surprisingly effective at being able to model all the details of proper substitution by recursing through equality theorems. Anyway, there are various nontrivial details to be dealt with, but I'll definitely keep you informed if I am successful.<br><br></div><div>Mario<br></div></div></div></div>