[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

> 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.)
>>
>
> I'm not sure I understand what you mean here. Is the problem that you
> can't see the type of x217?
>

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

[] |- x1 = x1

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.

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

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

varTerm(var(f,opType(typeOp(name(["HOLLight"],"fun")),[A,B])))

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.

FYI I fixed my Poly/ML problem, and now opentheory works like a charm :)

Mario


>
>
>>
>> On Mon, Oct 13, 2014 at 1:40 AM, Mario Carneiro <di.gama at gmail.com>
>> wrote:
>>
>>> On Mon, Oct 13, 2014 at 12:51 AM, Joe Leslie-Hurd <joe at gilith.com>
>>> wrote:
>>>
>>>> This looks pretty bad, because it seems like the variable x has got
>>>> captured. But if you give the opentheory tool the global option
>>>> --show-var-types it will annotate every term variable with its type,
>>>> and now the before stack is
>>>>
>>>>     [|- (!(x : B). (P : B -> bool) (x : B) ==> (Q : bool)) ==>
>>>>         (?) (P : B -> bool) ==> (Q : bool),
>>>>      [[],
>>>>       [[(P : B -> bool), \(y : B). (p : A -> B -> bool) (x : A) (y :
>>>> B)],
>>>>        [(Q : bool),
>>>>         ?(y : B) (x : A). (p : A -> B -> bool) (x : A) (y : B)]]], ...
>>>>
>>>> and the after stack is
>>>>
>>>>     [|- (!(x : B).
>>>>            (let (y : B) <- (x : B) in
>>>>             (p : A -> B -> bool) (x : A) (y : B)) ==>
>>>>            ?(y : B) (x : A). (p : A -> B -> bool) (x : A) (y : B)) ==>
>>>>         (?(y : B). (p : A -> B -> bool) (x : A) (y : B)) ==>
>>>>         ?(y : B) (x : A). (p : A -> B -> bool) (x : A) (y : B), ...
>>>>
>>>> which makes it clear that there are two variables with name "x" but
>>>> having different types, which according to the rules of higher order
>>>> logic makes them distinct. The article standard contains the words
>>>>
>>>> "Variables are identified by name and type."
>>>>
>>>> but should probably make this point far more explicit.
>>>>
>>>> Anyway, your reader's strategy of renaming the bound variable to a new
>>>> name is safe (if not necessary in this case) and so it doesn't solve
>>>> your problem.
>>>>
>>>
>>> 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.
>>>
>>>
>>>> As to your last question, the only article readers I know of have been
>>>> implemented in Standard ML, Ocaml and Haskell, so there is no
>>>> imperative reference available. Perhaps you are writing one!
>>>>
>>>
>>> I intend to write a translator from OpenTheory to Metamath [
>>> http://us.metamath.org/index.html]. 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.
>>>
>>> Mario
>>>
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141013/f7ed393c/attachment.html>