[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

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

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

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141013/485f33b1/attachment-0001.html>