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

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

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

  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?