Re: Recursive definitions of higher-order operators

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

On Thursday, January 7, 2016 at 6:08:26 PM UTC+2, bongiovanni francesco wrote:

Hi everyone,

I was wondering, how a Reduce (or Fold) operator would look like in TLA+ ? 

For a sequence:

    Reduce(Op(_, _), x, seq) ==

        LET RECURSIVE Helper(_, _)

        Helper(i, y) ==

            IF i > Len(seq) THEN y

                                     ELSE Helper(i + 1, Op(y, seq[i]))

        IN Helper(1, x) 

For a set (unordered reduction):

    ReduceSet(Op(_, _), x, s) ==

        LET RECURSIVE Helper(_, _)

        Helper(x1, s1) ==

            IF s1 = {} THEN x1

                            ELSE LET y == CHOOSE y \in s1 : TRUE

                                      IN Helper(Op(x1, y), s1 \ {y})

        IN Helper(x, s)

Alternatively, you could define:

    Ordering(s) ==

        CHOOSE seq \in [1..Cardinality(s) -> s] : \A i, j \in DOMAIN seq : i /= j => seq[i] /= seq[j] 

and then:

    ReduceSet(Op(_, _), x, s) == Reduce(Op, x, Ordering(s))