Re: [tlaplus] Function domains in TLAPS

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

BTW, just to provide some context:

Inspired by the discussion of FL's algebraic stack, I defined an iterated function application operator like so:

    RECURSIVE Yn(_, _, _)

    Yn(X, f, n) == \* apply f, n times; X is the identity domain, i.e. X = DOMAIN Yn(X, f, 0)

        LET Yn1 == Yn(X, f, n-1)

            D   == {x \in DOMAIN Yn1 : Yn1[x] \in DOMAIN f} IN

        IF n = 0 THEN [x \in X |-> x]

                 ELSE [x \in D |-> f[Yn1[x]]]

Then (mostly as an exercise to learn TLAPS) I wanted to see how many axioms specifying Yn are required to be able to deduce various theorems about it; e.g.:

    THEOREM \A f, X : \A m, n \in Nat : n >= m => DOMAIN Yn(X, f, n) \subseteq DOMAIN Yn(X, f, m)

    THEOREM \A f, X : \A n \in Nat : \A x \in DOMAIN Yn(X, f, n+1) : 

                                        f[Yn(X, f, n)[x]] = Yn(X, f, n)[f[x]]

It turns out you need quite a few (at least I couldn't do it with less than five or so)...