Re: [tlaplus] Checking if a set is a singleton

[Igor Konnov <igor.konnov@xxxxxxxxx>]

Hi,

Apalache has a number of expression simplifications that rewrite
constraints over cardinalities into simpler forms, when possible. You
can see the exact list in [1]. For example:

- Cardinality(a..b) is equivalent to IF a =< b THEN (b - a) + 1 ELSE 0
- Cardinality(SUBSET S) is equivalent to 2^Cardinality(S)
- Cardinality(Set) = 0 iff Set = {} (the one you have also mentioned)
- There is a special encoding for constraints like Cardinality(S) >= k.

In general, however, Apalache has a heavy encoding of Cardinality in
SMT. It essentially reduces over a set, but producing symbolic
constraints instead of concrete values:

```
MyCardinality(S) ==
    LET \* @type: (Int, a) => Int;
        Add(n, elem) == n + 1
    IN
    ApaFoldSet(Add, 0, S)
```

You can find the complete example in [2] and the definition of
ApaFoldSet via RECURSIVE operators in [3] (this definition is similar
to FoldSet from the community modules [4]).

[1] https://github.com/apalache-mc/apalache/blob/884dcbcfbbbed577492dc65f623b30f8e509f4e3/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala#L140
[2] https://github.com/apalache-mc/apalache/blob/8af6eae3011f2c0544a517267901327c38c43c94/src/tla/Apalache.tla#L134
[3] https://github.com/apalache-mc/apalache/blob/main/test/tla/TestCardinalityAsFold.tla
[4] https://github.com/tlaplus/CommunityModules/blob/master/modules/FiniteSetsExt.tla#L12

Best regards,
Igor

On Wed, Jan 21, 2026 at 11:36 PM Mathew Kuthur James
<mathewkj2048@xxxxxxxxx> wrote:
>
> Hi,
>
> In TLA+, given a set S, I understand that it's better to write S = {} than writing Cardinality(S) = 0. Is there a similar method to check if S is a singleton set, that beats using Cardinality(S) = 1? I am considering using singleton(S) == (\A x \in S : \A y \in S : x = y) /\ (S \= {})
>
> In general, is the Cardinality function costly in terms of model-checking performance, such that there are performance gains by using set comprehension for checking if a set is a singleton or empty (readability concerns aside)? What sort of test would I need to run to observe the performance gap, if one exists?
>
> --
> 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@xxxxxxxxxxxxxxxx.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/9a03af10-86d8-44bf-8c39-677d9b02e5d5n%40googlegroups.com.

-- 
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@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/CACooHMAb-8jw6L7Rf2uiFijfHv7ineZfEtaHy-A2-%2BBbcvWwCg%40mail.gmail.com.