Re: [tlaplus] Recursive definitions of higher-order operators

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

On Monday, December 7, 2015 at 7:00:51 PM UTC+2, Stephan Merz wrote:

Ah, but you can define it using a recursive function:

Range(s) == {s[i] : i \in DOMAIN s}

FlatMap(F(_), seq) ==

  LET FM[s \in Seq(Range(seq))] == 

        IF s = << >> THEN << >> ELSE F(Head(s)) \o FM[Tail(s)] 

  IN  FM[seq]

The following also works:

    FlatMap(F(_), seq) ==

        LET RECURSIVE Helper(_)

            Helper(s) == IF Len(s) = 0 THEN <<>> ELSE F(Head(s)) \o Helper(Tail(s)) 

        IN Helper(seq) 

If it's OK according to spec (and doesn't just happen to work, as was the case with my original version), then this seems like the simplest (legal) approach.

Ron