4 ms·

> > There is a general purpose programming model which supports verification at a very fine grained level, encompassing both computation and effects > Of cours

• pron 9y ago
  > Any time you "manipulate a computation" you are doing "higher-order" computation. Ah, this is something I specifically address in my TLA+ post series, probably because I heard it come up from you and others. Higher-order is strictly a formal property, i.e., it is a quality of a description of a system, not of a system itself. The best example is from continuous dynamical system. If the derivative of a system is a dynamical system itself, using one formalization you get a higher-order ODE. But people usually prefer describing all dynamical systems using first-order ODEs. The system of equations is first-order, but it still describes a "system that modifies a system". How? Because the "higher-order" function composition can be expressed as first-order composition of a different kind. Instead of writing: x'' = 2 you can write: x' = y ∧ y' = 2 So this first-order composition corresponds to a higher order system in a world with only one variable. You don't even have to take my word about TLA. Robin Milner, who was one of the leading advocates and theoreticians of functional programming, moved in the eighties from the lambda calculus to process calculi. He still insisted on algebraic composition, but process calculi are "first-order" yet still equivalent to the lambda calculus. Instead of a function taking a function, you have two processes composed in parallel. > Now it's possible that the models you are describing do not allow you to abstract over computation and thus are not "higher-order". If that's the case then either they are weaker than needed to talk about computation in general or they are very remarkable demonstrations that higher-order computation is generally not needed in practice! Not only do they allow to abstract over computation, they organize all computations into a lattice. I.e. if computation b is an abstraction of a (or a is a refinement of b), then a ≤ b in the lattice. So instead of saying that b is a parameterized computation, and that there exists some x s.t. a = b(x), we have that nice order relation; order and nondeterminism are used instead of parameterization. In fact, in TLA this is even used for first-order computations. Instead of saying that F is a computation parameterized by some natural number parameter, we say that F has a "degree of nondeterminism freedom" of a dimension of natural numbers. That's one of the greatest strengths of such formalisms, as this greatly simplifies formal verification (and one of the reasons why synchronous languages are the languages most amenable so far to formal verification).
  • tome 9y ago
    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 computation over all elements of a list?
    • 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