Function domains in TLAPS

[Ron Pressler]

Hi.

I've noticed that TLAPS does not automatically deduce anything about a function's domain from facts about its mapping. E.g., the lemma in the following snippet fails:

    CONSTANT f

    AXIOM A == f[3] = 8

    LEMMA 3 \in DOMAIN f BY A

This means that axioms must be specified/theorems proven separately for functions' mappings and their domains, which is extra work. Is this an artifact of the logic (if 3 is outside f's domain, f[3] may be anything, and if I know it's 8, that doesn't mean that 3 is in the domain) or just a limitation of TLAPS?

Ron

[Stephan Merz]

Just knowing that g[3] = 8 doesn't allow you to infer that g is a function or to conclude anything about DOMAIN g, so TLAPS does the right thing. (For example, 42[3] denotes some unspecified value in TLA+, would you want to conclude that 42 is a function?) You want to state "type predicates" for the functions that appear in your specification – typically as ASSUME clauses for constant parameters, and as invariants for variables.

Best regards,

Stephan

On 14 Jun 2016, at 16:09, Ron Pressler <r...@paralleluniverse.co> wrote:

Hi.

I've noticed that TLAPS does not automatically deduce anything about a function's domain from facts about its mapping. E.g., the lemma in the following snippet fails:

    CONSTANT f

    AXIOM A == g[3] = 8

    LEMMA 3 \in DOMAIN g BY A

This means that axioms must be specified/theorems proven separately for functions' mappings and their domains, which is extra work. Is this an artifact of the logic (if 3 is outside f's domain, f[3] may be anything, and if I know it's 8, that doesn't mean that 3 is in the domain) or just a limitation of TLAPS?

Ron

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Ron Pressler]

On Tuesday, June 14, 2016 at 5:18:04 PM UTC+3, Stephan Merz wrote:

Just knowing that g[3] = 8 doesn't allow you to infer that g is a function or to conclude anything about DOMAIN g, so TLAPS does the right thing. (For example, 42[3] denotes some unspecified value in TLA+, would you want to conclude that 42 is a function?) You want to state "type predicates" for the functions that appear in your specification – typically as ASSUME clauses for constant parameters, and as invariants for variables.

But this doesn't help, either:

    CONSTANT f

    ASSUME A1 == f = [x \in DOMAIN f |-> f[x]]

    ASSUME A2 == f[3] = 8

    LEMMA  3 \in DOMAIN f BY A1, A2

So now we know it's a function, but still don't infer anything about the domain from the mapping.

[Stephan Merz]

Correct, this is still too unspecific because f[3] denotes some value even if 3 is not an element of the domain of f. I was thinking of assumptions of the kind

f \in [ 0 .. 10 -> Nat ]

that help you reduce DOMAIN f to a specific set.

Stephan

[Ron Pressler]

On Tuesday, June 14, 2016 at 5:29:29 PM UTC+3, Stephan Merz wrote:

Correct, this is still too unspecific because f[3] denotes some value even if 3 is not an element of the domain of f. I was thinking of assumptions of the kind

f \in [ 0 .. 10 -> Nat ]

that help you reduce DOMAIN f to a specific set.

Oh, OK. Thanks. Unfortunately, I can't specify the function's domain because the function (and its domain) is computed by a recursive operator (and as TLAPS doesn't support recursive operators, I also specified the function with axioms), but had trouble proving things unless I stated separate axioms and theorems about the function's domain, in addition to the mapping.

[Leslie Lamport]

You seem to think that for any function f, you should be able to deduce

   (f[3] = 8) => (3 \in DOMAIN f)

That formula is equivalent to

    (3 \notin DOMAIN f)  =>  (f[3] # 8)

From what general properties of functions would you expect to be able
to deduce this?

Leslie

[Ron Pressler]

On Tuesday, June 14, 2016 at 5:35:30 PM UTC+3, Leslie Lamport wrote:

From what general properties of functions would you expect to be able
to deduce this?

Of course! Makes perfect sense. Thanks! 

[Ron Pressler]

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)...