Yes, absolutely I want to use a computation! The point is that I want to understand how TLA+ can abstract over computations.
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 *)
Map ∧ f
f ⇒ □(f_done = FALSE ↝ f_done = 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
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⟩
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⟩
I may add this with the explanation to the posts.
This is an example of a computation that is specifically tailored for functional languages, so let's instead start with something conceptually simpler for TLA, but downright impossible in FP: Plotkin's parallel or. Here you have a computation that takes two arbitrary computations, and simulates them in lockstep. [1]
Doing what you ask is certainly possible in TLA (in part 4), but that's just not how it's normally done. TLA allows you to abstract computations, i.e., extract some of their arbitrary features. As sequential computations of the kind you describe can correspond to functions and can be abstracted into function, that's exactly what you'll do in TLA+. You won't say "my computation runs an arbitrary computation over all elements of a list" (as is possible for Plotkin's or) because in order for that to make sense, that other computation must have certain features and cannot be arbitrary. In particular, it needs to behave like a function. So, what you'll write is a computation that runs something that can be represented as a function over all elements of a list. So, it will simply be:
As you'll note, there are no parameters at all. Instead, we use nondeterminism, i.e., define the computation for all lists of "type" T and for all functions T -> R.Of course, this computation is then abstracted (for use by others) simply into:
which is how you'd normally write this in TLA+. This definition is fully polymorphic, as it's an operator, not a function. If we wanted a function instead, we need "type parameters": which is a proper higher-order function (but these functions are proper functions, not "functions" or computations).In any event, f here is a function, not a computation. If for some reason you want to actually use a computation, you would need to specify more precisely what your expectations are of that computation (e.g., that it can take an argument at all). But, again, that's not how it's normally done in TLA+.
[1]: See here https://pron.github.io/posts/tlaplus_part3#plotkins-parallel... or here https://www.youtube.com/watch?v=15uy9Ga-14I