[opentheory-users] Troubleshooting an article reader

[Ramana Kumar]

On Mon, Oct 13, 2014 at 7:11 AM, Mario Carneiro <di.gama at gmail.com> wrote:

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

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.

An unambiguous operational specification of alpha-equivalence can be found
in the Model/syntax.ml in the HOL Light distribution (see the definition of
ACONV). Alternatively, see my extended port of that formalisation:
https://github.com/CakeML/cakeml/blob/master/hol-light/standard/syntax/holSyntaxScript.sml#L78
https://github.com/CakeML/cakeml/blob/master/hol-light/syntax-lib/holSyntaxLibScript.sml#L41

Terms that differ at free variables cannot be alpha-equivalent.

My current implementation says no, and so the following terms:
>
> [] |- ((\b. b x217) = ((one_REP (one_ABS x217)) = x217))
> [] |- (((\x219. x219 r) = ((one_REP (one_ABS r)) = r)) = ...)
>
> 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.)
>

That sounds correct.


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


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

These type operators and constant are primitive in the HOL inference system.


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

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.


>
> 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/fe8a9163/attachment.html>