[opentheory-users] Troubleshooting an article reader

[Joe Leslie-Hurd]

Hi Mario,

I've implemented the "debug" pragma of the article version 6 draft standard

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

in the opentheory tool, which allowed me to insert

"debug"
pragma

at the lines indicated by your output and compare the two implementations.

Let's begin with the subst command on line 16959. Before it executes
the opentheory stack looks like this:

   [|- (!x. P x ==> Q) ==> (?) P ==> Q,
     [[], [[P, \y. p x y], [Q, ?y x. p x y]]],
     |- !y. (let y <- y in p x y) ==> ?y x. p x y, ...

and afterwards it looks like

   [|- (!x. (let y <- x in p x y) ==> ?y x. p x y) ==> (?y. p x y) ==>
        ?y x. p x y, ...

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. In case it helps, here the typed result of the
deductAntisym on line 17007 according to the opentheory tool:

     {!(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)}

I'm afraid I can't help you any further without more information: I
hope you're able to compile the opentheory tool soon so you can use
these new debug pragmas to help identify where your reader is
diverging.

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!

Cheers,

Joe



On Sun, Oct 12, 2014 at 3:36 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> I'm working on an article reader for Java, and the current error I'm seeing
> doesn't make sense compared to the spec. That is, my test file,
> bool-int.art, shouldn't be valid, although I assume it is. The relevant
> lines from the output are:
>
> 877::assume                     [p] |- p
> 1447:843,1444:eqMp              [(p ==> q)] |- (p = (p /\ q))
> 1450:877,1447:eqMp              [p, (p ==> q)] |- (p /\ q)
> 1624:1621:subst                 [(p /\ q)] |- q
> 1627:1450,1624:deductAntisym    [p, (p ==> q)] |- ((p /\ q) = q)
> 1630:1450,1627:eqMp             [p, (p ==> q)] |- q
> 9849:698:subst                  [] |- ((((! \x. ((P x) ==> Q)) /\ ((? P) ==>
> Q)) = (! \x. ((P x) ==> Q))) = ((! \x. ((P x) ==> Q)) ==> ((? P) ==> Q)))
> 10205:10187,10204:deductAntisym [] |- (((! \x. ((P x) ==> Q)) /\ ((? P) ==>
> Q)) = (! \x. ((P x) ==> Q)))
> 10206:10205,9849:eqMp           [] |- ((! \x. ((P x) ==> Q)) ==> ((? P) ==>
> Q))
> 16595:10206:subst               [] |- ((! \x. ((P x) ==> Q)) ==> ((? P) ==>
> Q))
> 16959:16595:subst               [] |- ((! \x50. ((\y. (x p y) x50) ==> (?
> \y. (? \x. (x p y))))) ==> ((? \y. (x p y)) ==> (? \y. (? \x. (x p y)))))
> 17006:1630:subst                [(! \x. ((\y. (x p y) x) ==> (? \y. (? \x.
> (x p y))))), ((! \x. ((\y. (x p y) x) ==> (? \y. (? \x. (x p y))))) ==> ((?
> \y. (x p y)) ==> (? \y. (? \x. (x p y)))))] |- ((? \y. (x p y)) ==> (? \y.
> (? \x. (x p y))))
> 17007:16959,17006:deductAntisym [(! \x. ((\y. (x p y) x) ==> (? \y. (? \x.
> (x p y))))), ((! \x. ((\y. (x p y) x) ==> (? \y. (? \x. (x p y))))) ==> ((?
> \y. (x p y)) ==> (? \y. (? \x. (x p y)))))] |- (((! \x50. ((\y. (x p y) x50)
> ==> (? \y. (? \x. (x p y))))) ==> ((? \y. (x p y)) ==> (? \y. (? \x. (x p
> y))))) = ((? \y. (x p y)) ==> (? \y. (? \x. (x p y)))))
>
> (The output format shows all theorem-creating steps, labeled by the line in
> the file they first appeared, and the theorems they depend on.) I've trimmed
> the output just to show the direct ancestors of step 17007, which I think is
> incorrect, because the second hypothesis should have been eliminated but
> wasn't because the terms
>
> \x50. ((\y. (x p y) x50) ==> (? \y. (? \x. (x p y))))
> \x. ((\y. (x p y) x) ==> (? \y. (? \x. (x p y))))
>
> are not alpha-equivalent. The other candidate for the error is step 16959,
> where we do the substitution P -> \y. (x p y) and Q -> (? \y. (? \x. (x p
> y))) into \x. ((P x) ==> Q), but since x is bound in the original term and
> free in P, in accordance with the spec I swap out x -> x50 before doing the
> substitution. Is this wrong?
>
> If there are any readers written in an imperative language, that would also
> make a good reference. Unfortunately the functional PL examples are
> different enough in structure that I have difficulty mentally mapping the
> algorithm from one language to another.
>
> Mario
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>