3 ms·

> In any event, f here is a function, not a computation. If for some reason you want to actually use a computation Yes, absolutely I want to use a computation!

by tome 9y ago

> In any event, f here is a function, not a computation. If for some reason you want to actually use a computation Yes, absolutely I want to use a computation! The point is that I want to understand how TLA+ can abstract over computations.

deleted 9y ago
[deleted]
pron 9y ago
First, take a look at the parallel or example [1]. It's a computation that manipulates two other completely arbitrary ones, in a simple, compositional way that's not possible in any other formalism I'm aware of. The idea is not too different from how continuous dynamical systems are composed to describe "higher order" systems, despite first-order representation. Doing a "map" of a completely arbitrary computation f, would look like this: CONSTANTS T (* the "type" of elements in the in/out list *) VARIABLES in, out, f_param, f_result, f_done Map ≜ ∧ in ∈ Seq(T) ∧ f_param = Head(in) ∧ □[∧ f_done = TRUE ∧ f_done' = FALSE (* wait for f to work *) ∧ out' = Append(out, f_result]) ∧ f_param' = Head(in) (* send another element to f *) ∧ in' = Tail(in) ∧ UNCHANGED f_result ]_⟨f_param, in, out⟩ (* we don't allow f to change f_param, in or out *) and then, the composition or the "application" would be: Map ∧ f Nothing here guarantees that the computation f does any of those and that it terminates. We could do that by adding an assumption about f's behavior, that states that f behaves like a subroutine: f ⇒ □(f_done = FALSE ↝ f_done = TRUE) which states that if ever f_done is false, f will cause it to eventually become true. This is similar to how ODEs and processes in process calculi are composed, and all of this can be abstracted nicely into a "subroutine call" operator as I do in part 4. It is more cumbersome than sequential formalisms as composition is parallel "by default", but the technique is never used in practice precisely because of the Boolean algebra of computation that allows you to abstract appropriate computations as functions. [1]: This is the exact spot in the video: https://youtu.be/15uy9Ga-14I?t=37m34s https://youtu.be/15uy9Ga-14I?t=37m34s
- 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.

by tome 9y ago

deleted 9y ago

[deleted]

pron 9y ago

First, take a look at the parallel or example [1]. It's a computation that manipulates two other completely arbitrary ones, in a simple, compositional way that's not possible in any other formalism I'm aware of. The idea is not too different from how continuous dynamical systems are composed to describe "higher order" systems, despite first-order representation. Doing a "map" of a completely arbitrary computation f, would look like this: CONSTANTS T (* the "type" of elements in the in/out list *) VARIABLES in, out, f_param, f_result, f_done Map ≜ ∧ in ∈ Seq(T) ∧ f_param = Head(in) ∧ □[∧ f_done = TRUE ∧ f_done' = FALSE (* wait for f to work *) ∧ out' = Append(out, f_result]) ∧ f_param' = Head(in) (* send another element to f *) ∧ in' = Tail(in) ∧ UNCHANGED f_result ]_⟨f_param, in, out⟩ (* we don't allow f to change f_param, in or out *) and then, the composition or the "application" would be: Map ∧ f Nothing here guarantees that the computation f does any of those and that it terminates. We could do that by adding an assumption about f's behavior, that states that f behaves like a subroutine: f ⇒ □(f_done = FALSE ↝ f_done = TRUE) which states that if ever f_done is false, f will cause it to eventually become true. This is similar to how ODEs and processes in process calculi are composed, and all of this can be abstracted nicely into a "subroutine call" operator as I do in part 4. It is more cumbersome than sequential formalisms as composition is parallel "by default", but the technique is never used in practice precisely because of the Boolean algebra of computation that allows you to abstract appropriate computations as functions. [1]: This is the exact spot in the video: https://youtu.be/15uy9Ga-14I?t=37m34s https://youtu.be/15uy9Ga-14I?t=37m34s

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.