<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Mon, Oct 13, 2014 at 7:11 AM, Mario Carneiro <span dir="ltr"><<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.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"><div dir="ltr"><div><div>One thing that is not well explained in the spec is the definition of alpha-equivalent, even though it is used several times. (I'd also like the note "Bound variables will be renamed if necessary to prevent distinct variables becoming identical after the instantiation" in subst to be explained a little more explicitly. Which variables are to be considered distinct?) Can free variables be renamed in an alpha-equivalence? <br></div></div></div></blockquote><div><br></div><div>Terms are alpha-equivalent if they are equal up to a consistent renaming of bound variables. If variable binding is understood, alpha-equivalence is trivial. (Indeed in nameless term representations, like de Bruijn's, alpha-equivalence is the same as equality.) However, variable binding always feels just slightly more complicated than one would like.<br><br></div><div>An unambiguous operational specification of alpha-equivalence can be found in the Model/<a href="http://syntax.ml" target="_blank">syntax.ml</a> in the HOL Light distribution (see the definition of ACONV). Alternatively, see my extended port of that formalisation:<br><a href="https://github.com/CakeML/cakeml/blob/master/hol-light/standard/syntax/holSyntaxScript.sml#L78" target="_blank">https://github.com/CakeML/cakeml/blob/master/hol-light/standard/syntax/holSyntaxScript.sml#L78</a><br></div><div><a href="https://github.com/CakeML/cakeml/blob/master/hol-light/syntax-lib/holSyntaxLibScript.sml#L41" target="_blank">https://github.com/CakeML/cakeml/blob/master/hol-light/syntax-lib/holSyntaxLibScript.sml#L41</a><br><br></div><div>Terms that differ at free variables cannot be alpha-equivalent.<br></div></div><div class="gmail_quote"><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"><div dir="ltr"><div><div>My current implementation says no, and so the following terms:<br><br>[] |- ((\b. b x217) = ((one_REP (one_ABS x217)) = x217))<br>[] |- (((\x219. x219 r) = ((one_REP (one_ABS r)) = r)) = ...)<br><br></div>should not be considered alpha-equivalent in this application of eqMp because the variable substitution x217 -> r necessary involves a free variable (there are no issues with b -> x219). (FYI this is an error I just got in base.art line 64411, but don't feel obligated to track that down.) </div></div></blockquote><div><br></div><div>That sounds correct.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>If I were manually coding this article file, I'm not sure how I would resolve the issue, since I don't know the name of the dummy x217 so that I could subst it for r, and I can't apply absThm either since it also needs the name of the dummy. Note that this dummy x217 was created by defineTypeOp since there are two names there, r and a, which are not in the stack input. Is that supposed to be a literal "r"? (In metamath, all dummy variable names are specified by the stack machine when they are created, so this issue of "unknown dummies" doesn't occur.)<br></div></div></blockquote><div><br></div><div>I'm not sure I understand what you mean here. Is the problem that you can't see the type of x217?<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div><br></div>One last question: There are a few constants that appear to be hardcoded into the implementation, in particular "bool", "->" and "=", which are used by commands assume, appThm, refl, respectively (and also "a", "r" in case I guessed correctly in the previous paragraph). </div></blockquote><div><br></div><div>These type operators and constant are primitive in the HOL inference system.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">This causes conflicts if the constant names for these objects are different in the article file, for example in article files from HOL light where they have names like "HOLLight.=" and "HOLLight.fun". How do you handle these differences in your implementation? The spec doesn't seem to define these constants unambiguously, but I don't see how you could write an implementation that is not sensitive to local differences with these constants.<br></div></blockquote><div><br></div><div>I think Joe uses the notion of a theory interpretation to map constants in the HOLLight namespace to the correct OpenTheory namespace. He can probably explain in more detail.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"></div><div><div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 13, 2014 at 1:40 AM, Mario Carneiro <span dir="ltr"><<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.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"><div dir="ltr"><div class="gmail_extra"><div class="gmail_quote"><div><div>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></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><span><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></span><div>I intend to write a translator from OpenTheory to Metamath [<a href="http://us.metamath.org/index.html" target="_blank">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.<span><font color="#888888"><br><br></font></span></div><span><font color="#888888"><div>Mario<br></div></font></span></div></div></div> </blockquote></div><br></div> </div></div><br>_______________________________________________<br> opentheory-users mailing list<br> <a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br> <br></blockquote></div><br></div></div>