3 ms·

Thanks. It will take me some time to digest this.

by tome 9y ago

pron 9y ago
My 40 minute talk is a good intro to the theory, and the posts cover everything in great detail. Also, I've given it some more thought, and I think that my original (slightly corrected) answer is actually the better way (even when dealing with computation), and I'll explain why below: CONSTANTS T, R (* the "type" of elements in the in/out list *) VARIABLES in, out, f Map ≜ ∧ in ∈ Seq(T) ∧ f ∈ [T → R] ∧ □[∧ Len(in) > 0 ∧ out' = Append(out, f[Head(in)]) ∧ in' = Tail(in) ∧ UNCHANGED f]_⟨f, in, out⟩ Now, I too fell victim to the Whorfian syndrome, and thought in terms of functions (subroutines), instead of thinking about the meaning of the map program. What does a map program mean? I.e., in the semantics of TLA, a program is the set of all its possible executions. Every parameter, is just another dimension of nondeterminism, which adds more possible execution. This holds for ordinary value parameters, but also for "function" arguments. What do we know about the function argument? Well, that it behaves like a partial function, meaning it could either never terminate, or return a response (which map will then write to the output list), but we also know (or, rather, choose to assume) that the argument isn't an arbitrary computation, but a pure "functions", which means that for every input it must return the same output. The above specification says exactly that (it may not terminate because we haven't added liveness conditions). Map can then be composed with another computation that implements the mapping, and, if you watch the talk you'll see that the other computation may take as many steps as it likes due to stuttering invariance. The f function merely encodes our assumption about the mapping computation's behavior, namely that it always yields the same output to the same input. Without this assumption, the specification will simply look like: CONSTANTS T, R (* the "type" of elements in the in/out list *) VARIABLES in, out Map ≜ ∧ in ∈ Seq(T) ∧ □[∧ Len(in) > 0 (* sorry, forgot this before; must stop when the list is empty *) ∧ out' = ∃ y ∈ R : Append(out, y) (* completely nondeterministic in R *) ∧ in' = Tail(in)]_⟨f, in, out⟩ Now, we just state that any other computation must yield a value in R, but may not be "pure" and so may yield different values for the same input. I may add this with the explanation to the posts.

Thanks. It will take me some time to digest this.

by tome 9y ago

Thanks. It will take me some time to digest this.

pron 9y ago

My 40 minute talk is a good intro to the theory, and the posts cover everything in great detail. Also, I've given it some more thought, and I think that my original (slightly corrected) answer is actually the better way (even when dealing with computation), and I'll explain why below: CONSTANTS T, R (* the "type" of elements in the in/out list *) VARIABLES in, out, f Map ≜ ∧ in ∈ Seq(T) ∧ f ∈ [T → R] ∧ □[∧ Len(in) > 0 ∧ out' = Append(out, f[Head(in)]) ∧ in' = Tail(in) ∧ UNCHANGED f]_⟨f, in, out⟩ Now, I too fell victim to the Whorfian syndrome, and thought in terms of functions (subroutines), instead of thinking about the meaning of the map program. What does a map program mean? I.e., in the semantics of TLA, a program is the set of all its possible executions. Every parameter, is just another dimension of nondeterminism, which adds more possible execution. This holds for ordinary value parameters, but also for "function" arguments. What do we know about the function argument? Well, that it behaves like a partial function, meaning it could either never terminate, or return a response (which map will then write to the output list), but we also know (or, rather, choose to assume) that the argument isn't an arbitrary computation, but a pure "functions", which means that for every input it must return the same output. The above specification says exactly that (it may not terminate because we haven't added liveness conditions). Map can then be composed with another computation that implements the mapping, and, if you watch the talk you'll see that the other computation may take as many steps as it likes due to stuttering invariance. The f function merely encodes our assumption about the mapping computation's behavior, namely that it always yields the same output to the same input. Without this assumption, the specification will simply look like: CONSTANTS T, R (* the "type" of elements in the in/out list *) VARIABLES in, out Map ≜ ∧ in ∈ Seq(T) ∧ □[∧ Len(in) > 0 (* sorry, forgot this before; must stop when the list is empty *) ∧ out' = ∃ y ∈ R : Append(out, y) (* completely nondeterministic in R *) ∧ in' = Tail(in)]_⟨f, in, out⟩ Now, we just state that any other computation must yield a value in R, but may not be "pure" and so may yield different values for the same input. I may add this with the explanation to the posts.