<div dir="ltr"><br><div class="gmail_extra"><div class="gmail_quote"><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"><span></span><span><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></span><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><span><div></div></span></div></div></div></blockquote><div><br></div><div>I mean that any formula with a free dummy variable is effectively unusable, because you need to know the name of the variable in order to substitute it away. (Presumably, you already know the type, since it's easy to predict the forms of theorems that are generated.) For example, suppose you know that the formula<br><br></div><div>[] |- x1 = x1<br><br></div><div>was derived and is on the stack, but x1 is a dummy variable created on a whim by the virtual machine, so you don't at that point in the file know the particular string "x1". You can't bind it, because going from that to [] |- \x1. x1 = \x1. x1 requires absThm with x1 as parameter. You can't substitute it to a known variable a, because going from that to [] |- a = a requires subst with [[],[[x1,a]]] as parameter. And you can't export a theorem and specify the form [] |- a = a, because that's not alpha-equivalent. The only conclusion I can draw is that dummy variables should never be generated in a formula where they would appear free, since there are no means to eliminate them. I'm surprised, then, that a and r aren't quantified in the outputs to defineTypeOp, because if they were you could use dummy variables rather than hardcoding the strings "a" and "r" into the implementation.<br><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 class="gmail_extra"><div class="gmail_quote"><span></span><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></div></blockquote><div><br></div><div>Ah, just read the theory file spec; I see what you mean about "interpretations". It still seems like an article file that doesn't use the "standard" names for the primitives wouldn't compile, though. To take a simple example, suppose I construct the term (f:(A->B) x:A) in a "non-standard" article file. The final appTerm command has to check that f has the exact type TypeOp(->)[A, B] (or something like it), where the "->" is hardcoded into the reader, i.e. it is the "standard" name ([],"->"). However, the term f:(A->B) was built manually earlier in the article, via a sequence of commands like <br><br>varTerm(var(f,opType(typeOp(name(["HOLLight"],"fun")),[A,B])))<br></div><div><br>where the name(["HOLLight"],"fun") is *not* hardcoded and instead is in the article file. This will cause an error in appTerm unless the article file used "->" for its function application operator. In other words a HOL light article should not be able to compile on its own, unless the reader also had name(["HOLLight"],"fun") hardcoded - I would expect a mapping like this to be done during the conversion process, before it makes it into the .art file, if indeed the name "->" is required by spec.<br><br></div><div>FYI I fixed my Poly/ML problem, and now opentheory works like a charm :)<br></div><div><br>Mario<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 class="gmail_extra"><div class="gmail_quote"><div></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><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></div></div><span>_______________________________________________<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></span></blockquote></div><br></div></div>
</blockquote></div><br></div></div>