|
I don't think we need to use a recursive operator here. We can
instead write
PermSeqs(seq, n) ==
LET
indice_maps ==
{im \in [1..n -> DOMAIN seq]:
\A i, j \in 1..n:
i /= j => im[i] /= im[j]}
IN
{[x \in 1..n |-> seq[im[x]]]:
im \in indice_maps}
Which gives the same results.
On 3/6/19 2:06 AM, Stephan Merz wrote:
I believe that the post [1] on StackOverflow, with a link to a
worked-out example on GitHub, should help you get started.
If I understand correctly, the TLA+ specification of
your operator would be
Range(s) == { s[i] : i
\in DOMAIN s }
RECURSIVE PermSeqs(_,_)
\* set of sequences of
length k that are permutations of elements of sequence s
PermSeqs(s,k) ==
IF k=0 THEN { << >> }
ELSE { t \in [1..k -> Range(s)] : \E i \in 1 .. Len(s) :
/\ Head(t) = s[i]
/\ Tail(t) \in PermSeqs(SubSeq(s,1,i-1) \o
SubSeq(s,i+1,Len(s)), k-1) }
For example,
PermSeqs(<<1,2,2,3,4>>,
2) =
{ <<1,
2>>, <<1, 3>>, <<1, 4>>,
<<2,
1>>, <<2, 2>>, <<2,
3>>, <<2, 4>>,
<<3, 1>>, <<3, 2>>, <<3,
4>>,
<<4, 1>>, <<4, 2>>, <<4,
3>> }
PermSeqs(<<1,2>>,
3) = {}
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@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
|