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

Re: Recursive definitions of higher-order operators

Thank you Leslie and Ron!

This is interesting.  It is probably a bug in TLC because if I swap the order of the operators, like below,

RECURSIVE FlatMap(_,_)

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

I'll get an error:

Definition of FlatMap has different arity than its RECURSIVE declaration.

This is a similar error I was struggling with this morning when playing with SortSet.  But making LTE the first parameter seems to work:

TestSet(n) == [key:1..n, val:{"x", "y"}]

RECURSIVE SortSet(_,_)

SortSet(LTE(_,_),S) ==

    IF S = {} THEN <<>>

    ELSE LET s == CHOOSE t \in S : \A u \in S : LTE(t, u)

         IN  <<s>> \o SortSet(LTE, S \ {s})

LL == SortSet(LAMBDA x,y : x.key <= y.key, TestSet(4))