# Re: [tlaplus] Element-wise sum of a set of finite sequences

Hi Stephan,

Thanks a lot for your input. It's close to what I had in mind but for the case of
SumSet({<<1,2,3>>, <<1,2,3>>, <<1,2,3>>}) = <<1,2,3>>, actually the good result should be : <<3,6,9>>

Basically I would like the regular vector addition :)

- Francesco

On Thursday, 3 March 2016 12:06:12 UTC+1, Stephan Merz wrote:
Hi Francesco,

as far as I can tell, your function is not well specified for an empty set of sequences, so I'll assume that the function need produce the correct result only when the input set is non-empty. I'll also assume that all sequences have the same length. Then you can write something like the following

(* Auxiliary function to sum the i-th components of all sequences in S *)
sumi(i,S) ==
LET s[T \in SUBSET S] ==
IF T = {} THEN 0
ELSE LET x == CHOOSE x \in T : TRUE
IN  x[i] + s[T \ {x}]
IN  s[S]

SumSet(S) ==
LET l == Len(CHOOSE x \in S : TRUE)
IN  [i \in 1 .. l |-> sumi(i,S)]

(Of course, you can put the definition of sumi inside the LET in the definition of SumSet if you don't want that operator to be visible on the top level.)

I used TLC to check that

SumSet({<<1,2,3>>, <<3,4,6>>) = <<4,6,9>>  and

SumSet({<<1,2,3>>, <<1,2,3>>, <<1,2,3>>}) = <<1,2,3>>

Best,
Stephan

On 03 Mar 2016, at 11:44, bongiovanni francesco <bong...@xxxxxxxxx> wrote:

Hello,

I was wondering how one would specify in an elegant way the sum of finite sequences of integer in a set S.

Example:

Let S = { << 1,2,3 >>, << 3,4,6 >> }

The result of the function would be : << 1+3, 2+4, 3+6>> that the finite sequence <<4,6,9>>

The function has to work for an arbitrary number of finite sequences, provided they have the same length obviously.

Could someone guide towards this spec please ?