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

Re: [tlaplus] TLA+ logic

On Friday, December 4, 2015 at 6:20:50 PM UTC+2, fl wrote:
Looking at the concept of operators just reminds me that "operators" and functions are
two different things. Look at the syntax. In fact you can quantify over a variable that denotes
a function. It's over an operator that you can't quantify.

Oh, I know that. My original question was whether there's a difference (other than in syntax or implementation), and the answer is that there is -- the size of the domain. Now my question is whether the requirement to limit the domain ever makes a difference in practice so that it actually reduces expressivity.