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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Tue, 14 Jun 2016 07:25:56 -0700 (PDT)*References*: <c9f9a016-fcd1-4d87-abc0-1b594b6455f0@googlegroups.com> <FEFF636D-58CE-42CF-AC5D-A01D63E11D45@gmail.com>

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.

**Follow-Ups**:**Re: [tlaplus] Function domains in TLAPS***From:*Leslie Lamport

**Re: [tlaplus] Function domains in TLAPS***From:*Stephan Merz

**References**:**Function domains in TLAPS***From:*Ron Pressler

**Re: [tlaplus] Function domains in TLAPS***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Function domains in TLAPS** - Next by Date:
**Re: [tlaplus] Function domains in TLAPS** - Previous by thread:
**Re: [tlaplus] Function domains in TLAPS** - Next by thread:
**Re: [tlaplus] Function domains in TLAPS** - Index(es):