[opentheory-users] Troubleshooting an article reader

[Mario Carneiro]

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