Re: [tlaplus] Function domains in TLAPS

[Stephan Merz <stepha...@xxxxxxxxx>]

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...@xxxxxxxxxxxxxxxxxxx> 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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.