[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Arity of NEW operator in `tlapm`



Hi Stephan,

I am sorry, the exact _expression_ that raises the error I described has the other
form of function definition:

```
LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET f[x \in S \X S] == e(x[1], x[2])
         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})
```

but as I was describing it, I both was convinced that I used the form `f == ...`
(because I use it at most places), and did not consider the possibility that
different (syntactically similar) function definitions would yield a different result from SANY.

To be more precise this time, when the module:

```
------------------------------- MODULE test --------------------------------
EXTENDS FiniteSets


LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET f == [x \in S \X S |-> e(x[1], x[2])]
         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})


LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET f[x \in S \X S] == e(x[1], x[2])
         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})

================================================================================
```

is given to SANY with:

```

$ java -cp /some/path/tlatools/tla/ -DTLA-Library=/some/path/v2-tlapm/library tla2sany.SANY test.tla
```

then the output is:

```
****** SANY2 Version 2.1 created 24 February 2014

Parsing file test.tla
Parsing file /some/path/v2-tlapm/library/FiniteSets.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Naturals.tla
Parsing file /some/path/tlatools/tla/tla2sany/StandardModules/Sequences.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module test
Semantic errors:

*** Errors: 1

line 14, col 40 to line 14, col 45 of module test

Function 'f' is defined with 1 parameters, but is applied to 2 arguments.
```

So SANY indicates that the function application in the second lemma is
in error, even though `tlapm` proves that the functions in the two lemmata
are equal (as described on p.304):

```
LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET
            f1 == [x \in S \X S |-> e(x[1], x[2])]
            f2[x \in S \X S] == e(x[1], x[2])
         IN  f1 = f2
    OBVIOUS
```


Other comments:

1. Yesterday I switched to using the syntax `f[<< a, b >>]`, so that the proofs will be both
checked by `tlapm`, and compliant to SANY (because proving something "modulo errors from
the syntax checker" is not a convincing claim, and because if others attempt to confirm the
results using the toolbox, instead of `tlapm` directly, they will be required to first
correct errors reported by SANY).

This change reminded me that another reason for preferring the syntax  `f[a, b]` was
difficulties in automated proof. It was possible to prove the same claims, but some
refinement of the proofs or hiding of definitions was needed, for some steps
(few compared to the total number of steps).

It may be worth noting that the failures were not by the backends (I think in all cases),
but Isabelle was rejecting some of the proofs found by Zenon
(with a "Failed to finish proof" in the Isabelle log and looking in the `*.thy`
file it seems that these were proofs generated by Zenon).

There are more details, and some suggestions about the command line interface of `tlapm`,
from that process that seem worth reporting, but the issue in this thread is different,
so another thread or a GitHub issue is probably more appropriate for reporting more details.


2. Yet another way to use the combination of function definition and application that
would raise a SANY error, but avoid the error is by passing the defined function as
argument to an operator that is defined using the syntax `f[a, b]`.


Best regards,
ioannis



On Thu, May 11, 2017 at 5:08 AM, Stephan Merz <stepha...@xxxxxxxxx> wrote:
Hi Ioannis,

The above comment relates to another error that SANY raises, which I have been considering
opening an issue about. The error has the form:

   "Function 'f' is defined with 1 parameters, but is applied to 2 arguments."

when SANY sees `f[a, b]` after a definition of the form `f == [t \in S \X S |-> e(t[1], t[2]) ]`.
I understand the motivation for raising an error in this case, to avoid what will usually indicate
a reasoning error, but based on my understanding of TLA+ this seems valid TLA+ (p.303 in the TLA+ book
and the untyped nature of TLA+). The function application can always be rewritten equivalently
without syntactic sugar as `f[ << a, b >> ]`, thus avoiding the SANY error. So raising this error
does not restrict what one can express.

I am unable to reproduce this issue. For example, SANY accepts

LEMMA
  ASSUME NEW S, NEW e(_,_), IsFiniteSet(S)
  PROVE  LET f == [x \in S \X S |-> e(x[1], x[2])]
         IN  \A x \in S : IsFiniteSet({f[x,y] : y \in S})

Could you please expand?

Thanks,
Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.