3 ms·

Can you give me a concrete example of a higher order computation in TLA? For example, can you show me how to construct a computation that runs another computat

• pron 9y ago
  It is actually very easy. I cover that in parts 3 and 4 of my series. I will answer your question, but the answer may sound a little tricky. Part of the problem is that simply in stating your question you have quite a few hidden assumptions that are natural in FP but don't take into account how an arbitrary computation can actually behave. 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: CONSTANTS T, R (* the "type" of elements in the in/out list *) VARIABLES in, out, f Map ≜ ∧ in ∈ Seq(T) ∧ f ∈ [T → R] ∧ □[∧ out' = Append(out, f[Head(in)]) ∧ in' = Tail(in) ∧ UNCHANGED f]_⟨f, in, out⟩ 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: Map(list, f) ≜ [i ∈ DOMAIN list ↦ f[list[i]]] 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": CONSTANTS T, R map[list ∈ Seq(T), f ∈ [T → R]] ≜ [i ∈ DOMAIN list ↦ f[list[i]]] 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 https://pron.github.io/posts/tlaplus_part3#plotkins-parallel... or here https://www.youtube.com/watch?v=15uy9Ga-14I https://www.youtube.com/watch?v=15uy9Ga-14I
  • 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
      • 9y ago