Quantification over sequences

[Zixian Cai]

Hi,

I’m just wondering whether it is possible to have quantification over non-numerals.
For example, I would like to say, \E lst \in Seq(1..n): … or \E lst \in Seq(Nat): …

When I check it using TLC, it says “TLC encountered a non-enumerable quantifier bound”.

Sincerely,
Zixian

[Stephan Merz]

TLA+ allows you to write bounded quantification over arbitrary sets and your examples are perfectly legal TLA+, but as the error message indicates, TLC is restricted to quantification over finite sets. You may override operator definitions (in the Toolbox tab Advanced Options -> Definition Override) and write something like

Seq(S) <- UNION { [1 .. k -> S] : k \in 0 .. 3 }

to restrict to sequences of length at most 3. In the case where S itself is infinite (such as Nat in your second example), you'll want to override its definition in a similar way.

Of course, you have to think about what this change of semantics means for your specification.

Regards,
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+u...@googlegroups.com.
> To post to this group, send email to tla...@googlegroups.com.
> Visit this group at https://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.

[Zixian Cai]

I guess the error message could be phrased better, because given a finite set S, Seq(S) is enumerable.

Sincerely,
Zixian

[Stephan Merz]

The meaning of "enumerable" as used by TLC is explained in section 14.2.2 of Specifying Systems (p. 232). It is different from countable (sometimes called denumerable) sets in mathematics or recursively enumerable sets in computability.

Stephan

[Zixian Cai]

Hi Stephan,

Thanks for the explanation. it makes sense now.

Sincerely,
Zixian