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

*From*: Ron Pressler <ron.pr...@xxxxxxxxx>*Date*: Thu, 4 Jan 2018 11:38:32 -0800 (PST)*References*: <2de00f5b-0cc4-4528-bc27-e24a1a244ce5@googlegroups.com>

You write:

Crucially,

a state is a set of variables whose values can change over time.

but what is meant as state here is not exactly what is meant as mutable state in programming. Here's an example of a (pure) Haskell function:

gcd :: Int -> Int -> Intgcd x y = if x == y then xelse if x > y then gcd (x - y) yelse gcd x (y - x)

there is no mutation going on, yet the variables x and y are variables whose values change over time (at each iterative step). It's true that there may not be any mutation of memory addresses (actually, there likely is, because the function is tail-recursive), there is still state. The corresponding TLA+ specification also says nothing about mutation of memory cells. In fact, TLA+ has no notion of memory at all, unless you choose to model it. Variables whose values can change just means that a set of names refers to different values -- this happens in pure functional languages all the time.

**Follow-Ups**:

**References**:

- Prev by Date:
**Re: [tlaplus] How can this lemma (involving []) be applied?** - Next by Date:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Previous by thread:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Next by thread:
**Re: Is TLA+ still useful if your implementation language is a purely functional one, like Haskell?** - Index(es):