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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sat, 4 Nov 2017 22:55:06 -0700 (PDT)*References*: <7928ce64-f9ac-4cb3-91bb-925a58a7cb8d@googlegroups.com>

The answer to your two questions is that they are "silly expressions". See Section 6.2 (page 67) of *Specifying Systems.*

Leslie

On Saturday, November 4, 2017 at 10:50:38 PM UTC-7, Greg Wiley wrote:

In the TLA book on page 57, the definition for RdMiss(p) contains the formula:

buf[p].op = "Rd"

However, buf is function with domain Proc and range that includes

requests, values, and NoValue. So, buf[p] might not be a function with a

domain containing "op". It might not be a function at all.

I guess I have two questions:

What does f["op"] mean when "op" is not in the domain of the function, f?

What does f["op"] mean when f is not a function?

I'm looking specifically for what those things mean in TLA+ but a mathematical

context is more than welcome.

TIA, -=greg

**Follow-Ups**:**Re: What does f[x] mean when f is not a function?***From:*Greg Wiley

**References**:**What does f[x] mean when f is not a function?***From:*azte . . .

- Prev by Date:
**What does f[x] mean when f is not a function?** - Next by Date:
**Re: What does f[x] mean when f is not a function?** - Previous by thread:
**What does f[x] mean when f is not a function?** - Next by thread:
**Re: What does f[x] mean when f is not a function?** - Index(es):