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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Sun, 11 Nov 2018 18:31:12 -0800 (PST)*References*: <a9da40e6-492d-4ca7-89a5-1ca10bc44796@googlegroups.com>

This discussion of intension and extension may be fine, but I'm

concerned that an engineer reading it might get the idea that

TLA+ has subtle problems and is difficult to understand. So, I

will explain the issue being discussed in simple terms that an

of a definition. Some logicians formalize the definition A == 2 by

saying that it adds the axiom A = 2. I found it simpler to make

definition a syntactic concept in TLA+, so a defined operator is

essentially a macro. This implies that the definition A == 2 means

that one can replace A by 2 or vice versa in any _expression_ without

changing the meaning of that _expression_. Thus,

changing the meaning of the _expression_.

Similarly,

(2) If A(x) == 2*x and B(x) == 2*x, then for any _expression_ exp,

A(exp) can be replaced by B(exp) (and vice versa) in any

_expression_ without changing the meaning of that _expression_.

Note that in (2), I did not write A = B because that's not a legal

TLA+ _expression_. To keep TLA+ as simple as possible, equality of

operators is not expressible in it.

Also, A(x) == 2*x and A(y) == 2*y define the same operator A,

so (2) is true if the definition of A is replaced by A(y) = 2*y.

Note: A TLA+ recursive definition is shorthand for its actual

definition. For example, the recursive function definition

f[n \in Nat] == IF n = 0 THEN 1 ELSE n * f[n-1]

is shorthand for the actual definition

f == CHOOSE f : f = [n \in Nat |-> IF n = 0 THEN 1 ELSE n * f[n-1]]

The actual definition of a recursively defined operator is quite

complicated, but it defines the operator to have the expected meaning

on values of its arguments for which the recursion terminates.

-------

Let me give the name "definitional equivalence" to the general

property of definitions illustrated by (1) and (2). Definitional

equivalence is similar to the property of equality called

"substitutivity". Substitutivity asserts that exp1 = exp2 implies

that replacing exp1 by exp2 (or vice versa) in any _expression_ leaves

the value of the _expression_ unchanged. Definitional equivalence holds

for all definitions and expressions of TLA+. However, substitutivity

holds only for ordinary mathematics, which is formalized by the subset

of TLA+ obtained by eliminating the action operators and temporal

operators in Tables 3 and 4 (page 269) of "Specifying Systems". The

full TLA+ language expresses a temporal logic, and substitutivity does

not hold in temporal logic. This complicates writing proofs of

liveness properties, but it is of no concern to users of TLA+ who

don't write proofs.

Leslie

concerned that an engineer reading it might get the idea that

TLA+ has subtle problems and is difficult to understand. So, I

will explain the issue being discussed in simple terms that an

engineer will understand.

TLA+ is a precise, formal mathematical language. As far as I can

tell, mathematicians have no standard way of formalizing the conceptTLA+ is a precise, formal mathematical language. As far as I can

of a definition. Some logicians formalize the definition A == 2 by

saying that it adds the axiom A = 2. I found it simpler to make

definition a syntactic concept in TLA+, so a defined operator is

essentially a macro. This implies that the definition A == 2 means

that one can replace A by 2 or vice versa in any _expression_ without

changing the meaning of that _expression_. Thus,

(1) if A == 2 and B == 2, then A = B is true and any A appearing

in an _expression_ can be changed to B (and vice-versa) without changing the meaning of the _expression_.

Similarly,

(2) If A(x) == 2*x and B(x) == 2*x, then for any _expression_ exp,

A(exp) can be replaced by B(exp) (and vice versa) in any

_expression_ without changing the meaning of that _expression_.

Note that in (2), I did not write A = B because that's not a legal

TLA+ _expression_. To keep TLA+ as simple as possible, equality of

operators is not expressible in it.

Also, A(x) == 2*x and A(y) == 2*y define the same operator A,

so (2) is true if the definition of A is replaced by A(y) = 2*y.

Note: A TLA+ recursive definition is shorthand for its actual

definition. For example, the recursive function definition

f[n \in Nat] == IF n = 0 THEN 1 ELSE n * f[n-1]

is shorthand for the actual definition

f == CHOOSE f : f = [n \in Nat |-> IF n = 0 THEN 1 ELSE n * f[n-1]]

The actual definition of a recursively defined operator is quite

complicated, but it defines the operator to have the expected meaning

on values of its arguments for which the recursion terminates.

-------

Let me give the name "definitional equivalence" to the general

property of definitions illustrated by (1) and (2). Definitional

equivalence is similar to the property of equality called

"substitutivity". Substitutivity asserts that exp1 = exp2 implies

that replacing exp1 by exp2 (or vice versa) in any _expression_ leaves

the value of the _expression_ unchanged. Definitional equivalence holds

for all definitions and expressions of TLA+. However, substitutivity

holds only for ordinary mathematics, which is formalized by the subset

of TLA+ obtained by eliminating the action operators and temporal

operators in Tables 3 and 4 (page 269) of "Specifying Systems". The

full TLA+ language expresses a temporal logic, and substitutivity does

not hold in temporal logic. This complicates writing proofs of

liveness properties, but it is of no concern to users of TLA+ who

don't write proofs.

Leslie

**References**:**How to determine an Action execution.***From:*apostolis . xe . . .

- Prev by Date:
**Re: [tlaplus] How to determine an Action execution.** - Next by Date:
**Re: [tlaplus] Ability to use Vim keystrokes with TLA+ Toolbox?** - Previous by thread:
**Re: [tlaplus] How to determine an Action execution.** - Next by thread:
**building tlaplus from source fails** - Index(es):