[lmm]

> You can think of it as a lookup table all you want, but you will define your algorithm as some state machine. Maybe looking for the maximum value is too simple, as the use of a combinator is too trivial, but think of a program that sorts a list. You can imagine the program to be a function if you like, but when you design the algorithm, there is no way, no how, that you don't design it as a series of steps.

Again, disagree. I think of it more as defining what a sorted list is to the computer. (An extreme example would be doing it in Prolog or the like, where you just tell the computer what it can do and what you want the result to look like). It's very natural to write mergesort or bubblesort thinking of it a lookup table - "empty list goes to this, one-element list goes to this, more-than-one-element list goes to... hmm, this".

Now that's not an approach that's ever going to yield quicksort, but if we're concerned with correctness and not so much about performance then it's a very usable and natural approach.

> You are -- and I don't blame you, it's hard to shake away -- thinking in terms of a language, which has a given syntax and a given semantics and "implementation". When reasoning about algorithms mathematically, there are no "implementation" details, only the level of the algorithm you care to specify. In TLA+ you can define higher-order recursive operators like "reduce" that does a reduction in one step -- or zero-time if you like -- or you can choose to do so over multiple steps. It is up to you. There is no language, only an algorithm, so no "implementation", only the level of detail that interests you in order to reason about the algorithm.

I think you're begging the question. If you want to reason about an algorithm - a sequence of steps - then of course you want to reason about it as a sequence of steps. What I'm saying is it's reasonable and valuable, under many circumstances, to just reason about a function as a function. If we were doing mathematics - actual pure mathematics - it would be entirely normal to completely elide the distinction between 5 + (2 * 3) and 11, or between the derivative of f(x) = x^2 and g(x) = 2x. There are of course cases where the performance is important and we need to include those details - but there are many cases where it isn't.

> if you wanted to reason about, say, performance of a left-fold or a right-fold, you'll want to reason about how they do it, and how any computation is done is with a state machine.

Sure. (I think/hope we will eventually be able to find a better representation than thinking about it as a state machine directly - but I completely agree that the functional approach simply doesn't have any way of answering this kind of question at the moment).

[pron]

> Again, disagree. I think of it more as defining what a sorted list is to the computer. (An extreme example would be doing it in Prolog or the like, where you just tell the computer what it can do and what you want the result to look like).

Exactly, but the point is defining at what level. Take your Prolog example. This is how you can define what a sorted list is in TLA+:

    IsSorted(seq) ≜ ∀i,j ∈ 1..Len(seq) : i < j => seq[i] ≤ seq[j]
    Sorted(seq) ≜ CHOOSE res ∈ Perms(seq) : IsSorted(s)

So this is a definition, but it's not an algorithm. Yet, in TLA+ it could describe a state machine of sorts: the nondeterministic state machine that somehow yields a sorted list. Any particular sorting algorithm is a refinement of that machine. Of course, the refinement does not need to happen in one step. You can describe a mergesort as a machine that somehow merges, which is a refinement of the magical sorting machine. Any machine that merges, say, using a work area in a separate array, is then a refinement of that. You decide when to stop.

If there's a difference in how you "define" a sorted list via bubble-sort or mergesort in your lookup table image that difference is an abstract state machine. For example, in the mergesort case your composition "arrows" are merges. You have just described a (nondeterministic) state machine. Otherwise, if your lookup table algorithm doesn't have any steps, it must simply map the unsorted array to the sorted array and that's that. If there is any intermediate mappings, those are your transitions.

The state machines are nondeterministic, so you don't need to say "do this then do that". It's more like "this can become that through some transformation". Every transformation arrow is a state transition. You don't need to say in which order they are followed.

Here is a certain refinement level of describing mergesort

    ∃x, y ∈ sortedSubarrays : x ≠ y ∧ x[2] + 1 = y[1]
                     ∧ array' = Merge(array, x, y) 
                     ∧ sortedSubarrays' = {sortedSubarrays \ {x,y}} ∪ {<<x[1], y[2]>>}

That's it; That's the state machine for mergesort (minus the initial condition). It is completely declarative, and it basically says "any two adjacent sorted subarrays may be merged". Note that I didn't specify anything about the order in which subarrays are sorted; this machine is nondeterministic. Even that may be too specific, because I specified that only one pair of subarrays picked at each step. I could have said that any number of pairs is picked, and then my specification would be a refinement of that.

You can define an invariant:

   Inv ≜ [](∀x ∈ sortedSubarrays : IsSorted(x))

The box operator [] means "always". Then you can check that

    MergeSort => Inv

to assert that the sorted subarrays are indeed all sorted.

> I think/hope we will eventually be able to find a better representation than thinking about it as a state machine directly

There are two requirements: first, the formulation must be able to describe anything we consider an algorithm. Second, the formulation must allow refinement, i.e. the ability to say that a mergesort is an instance of a nondeterministic magical sorting algorithm, and that a sequential or a parallel mergesort are both instances of some nondeterministic mergesort.

[lmm]

> If there's a difference in how you "define" a sorted list via bubble-sort or mergesort in your lookup table image that difference is an abstract state machine.

Perhaps. But very often that's precisely the kind of difference I want to elide, since the two are equivalent for the purposes of verifying correctness of a wider program that uses one or the other.

I find it a lot more difficult to think about a state machine than about a function. What is it I'm supposed to be gaining (in terms of verifying correctness) by doing so? (I might accept that certain aspects of program behaviour can only be modeled that way - but certainly it's usually possible to model a large proportion of a given program's behaviour as pure functions, and I find pure functions easier to think about by enough that I would prefer to divide my program into those pieces so that I can think mostly about functions and only a little about states).

[pron]

I think we're talking at two different levels here. I am not talking about using a sorting routine in a program, but about writing a sorting routine. You want to know that your sorting routine actually sorts. Your routine is a state machine; its blackbox description is a function. You want to prove that your state machine implements the function. Our goal is to verify that mergesort actually sorts. Not that the air traffic control program using mergesort works (we could, but then the ATC program would be the state machine, and sorting would be just a function).

> Perhaps. But very often that's precisely the kind of difference I want to elide, since the two are equivalent for the purposes of verifying correctness of a wider program that uses one or the other.

This means that both are refinements of the "magical sorting machine". You can use "magical sorting" in another TLA+ spec, or, as in this running example, prove that mergesort is a refinement of "magical sorting". If what you want to specify isn't a mergesort program but an ATC program that uses sorting, of course you'd use "magical sorting" in TLA+. You specify the "what" of the details you don't care about, and the "how" of the details you do.

> I find it a lot more difficult to think about a state machine than about a function.

Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.

[lmm]

> Sure, but again when you want to verify an algorithm, it may use lots of black boxes, but the algorithm you are actually verifying is a white box. That algorithm is not a function; if it were, then you're not verifying the how just stating the what. The how of whatever it is that you actually want to verify (not the black boxes you're using) is a state machine. Other ways of thinking about it include, say, process calculi, lambda calculus etc., but at the point of verifying that, considering it a function is the one thing you cannot do, because that would be assuming what you're trying to prove.

Well a function is necessarily a function (if we enforce purity and totality at the language level). Presumably what we want to verify is that its output has certain properties, or that certain relations between input and output hold. But that seems like very much the kind of thing we can approach in the same way we'd analyse a mathematical function.