[opentheory-users] Troubleshooting an article reader

[Joe Leslie-Hurd]

Hi Mario,

> 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 agree with your assessment that dummy free variables are a scourge,
and therefore in version 6 of the article standard I propose changing
the behaviour of defineTypeOp to take the names of the "a" and "r"
variables as additional arguments:

http://www.gilith.com/research/opentheory/article.html#defineTypeOpCommand

The nice thing is that literally any variable name will work, because
the two resulting theorems of defineTypeOp each have precisely one
free variable, so there's nothing to clash with. It's easy to recover
the legacy version 5 behaviour by simply passing in the names "a" and
"r".

Does that satisfy your concerns? I believe that's the only instance in
the spec of dummy free variables, but please let me know if that's not
the case.

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

You are correct, see the example package

http://www.gilith.com/research/opentheory/example-1.0.html

for a description of the external type operators, constants (and
axioms) that are treated as primitive by the OpenTheory logical
kernel.

I assume you have already cloned my HOL Light fork with the OpenTheory
proof logging, which is available from

http://src.gilith.com/hol-light.html

If you look at the top of opentheory/stdlib/stdlib.int, you can see
the mapping that's used to translate the HOL Light names for the
primitive symbols to the OpenTheory names.

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

Excellent news: please do let me know if you find any bugs in the tool.

Cheers,

Joe