[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.