3 ms·

I mean "state" in the sense that we can distinguish time-dependent systems with internal state or memory from time-independent systems, whose outputs are a pure

I mean "state" in the sense that we can distinguish time-dependent systems with internal state or memory from time-independent systems, whose outputs are a pure function of their inputs. Combining pure functions to create pure functions does not introduce any state, in this sense. An entire program may have no observable state, like a command-line tool that reads stdin and writes stdout with no particular timing. It does have state inside it, of course, but only because it's running on a giant state machine. We can fully describe its behavior without making reference to any internal states, using functions or relations to talk about the relationship between its input and its output. > I would say that the main difference between TLA+ and the functional approaches, is that in TLA+ you reason purely mathematically, while in the functional approaches you reason within a (complex) programming language. This statement puzzles me, because we have great math for reasoning about pure functions (mappings). We have lambda calculus and category theory. You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. The recursion can be handled using the fixed point operator and the algebraic laws it obeys. Edit: In fairness, existing "functional approaches" to specification do seem complex and look like programming languages. I came across an old comment of yours (https://news.ycombinator.com/item?id=11835178 https://news.ycombinator.com/item?id=11835178) that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs, depending on whether they are more transformative or more reactive. I'm just as happy if learning more about TLA+ turns my idea of this on its head, though!

pron 9y ago
> Combining pure functions to create pure functions does not introduce any state, in this sense. Yes, but that's not the same as state in the TLA+ sense. You cannot have computation without state in the TLA+ sense, whether you call your functions pure or not. In TLA+, an algorithm that "purely" computes quicksort and one that outputs an interim result after each recursive step is the same algorithm. TLA+ doesn't talk about visible state, but state in the most fundamental way, without which there is no computation whatsoever. In part 3 I ask whether Euclid's algorithm or Quicksort are imperative or pure-functional. There is no way to answer that question, as their descriptions are at an abstraction level above where this distinction can be made. TLA+ can work at that level. You just can't look at Euclid's algorithm (or quicksort) in TLA+, and tell whether it's imperative or functional. It's an abstract mathematical description. > We have lambda calculus Lambda calculus is a state machine (or, more precisely, it is naturally described as a state machine). > You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. What you're calling state and what TLA+ calls state is not the same thing. Whichever way you prove Quicksort works is the way you'd do it in TLA+ with state. You just don't call it state. I would, however, be very much interested to see how you prove Quicksort works using category theory. AFAIK, all approaches to verify QS work the same way, using an inductive invariant, namely an invariant on state. > that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs I was talking about synchronous programming languages inspired by TLA+, and I agree. I would rather write a compiler in a pure-functional language than in a synchronous one, and an interactive program in a synchronous language than a pure-functional one. But that is a separate discussion from that about mathematical reasoning. I would agree that if one day there would be a FP-based verification tool that is aimed at engineers rather than researchers, then for ergonomics/syntax reasons, it's possible that it would be more convenient for reasoning about compilers. But there's nothing in the theory of TLA+ that makes it less convenient. I do, however, admit that there are tradeoffs between working in "pure math" as in TLA+, or within a programming language. There are often patterns that are specific to certain programming styles, and reasoning within a similar formalism may reduce effort. In other words, sometimes you may want to reason about a specific expression of an algorithm rather than about the algorithm in its pure abstract sense, and a formalism that shares the same expression style may make it easier. But I don't know how much of this is purely hypothetical. Most algorithms that are interesting or subtle, are essentially interesting or subtle, and verifying them in all formalisms is very similar (and usually involves the same proof technique: inductive invariants).
- dgreensp 9y ago
  Thanks for bearing with me, and responding, even if it might be more efficient for me to wait and read the next parts. It seems like if the quicksort of a list L is defined as equal to the concatenation of 1) the quicksort of the subsequence of L consisting of items less than the pivot item, 2) (the list containing) the pivot item, and 3) the quicksort of the subsequence of L consisting of items greater than the pivot, then we can prove properties like "any two items of the resulting list are in sorted order" by case analysis on whether each item is part of (1), (2), or (3). Maybe you would interpret "the quicksort of L is defined as..." to mean "if you're in state quicksort(L), you can proceed to state the-concatenation-of"? If we're working in the realm of mathematics, don't we get definitions, equations, and inductive proofs for free, without making a state machine do it? Edit: Reading more, I guess I'm just doing the sorting inside the "next-state relation" of a state machine, so it's done in one state transition, and saying you could look at quicksort as one way to factor the relation, which by math is equivalent to other ways to factor the relation that resemble other sorting algorithms.
  - pron 9y ago
    > Reading more, I guess I'm just doing the sorting inside the "next-state relation" of a state machine, so it's done in one state transition While you could describe all of quicksort as a function in TLA+ (taking place instantaneously), that's no what you've done. You described a single state transition, but one that doesn't capture all of quicksort, just one partitioning step. To show that the result is sorted, you'd need to do an induction over such concatenations; the thing you're doing the induction over is called state.

pron 9y ago

> Combining pure functions to create pure functions does not introduce any state, in this sense. Yes, but that's not the same as state in the TLA+ sense. You cannot have computation without state in the TLA+ sense, whether you call your functions pure or not. In TLA+, an algorithm that "purely" computes quicksort and one that outputs an interim result after each recursive step is the same algorithm. TLA+ doesn't talk about visible state, but state in the most fundamental way, without which there is no computation whatsoever. In part 3 I ask whether Euclid's algorithm or Quicksort are imperative or pure-functional. There is no way to answer that question, as their descriptions are at an abstraction level above where this distinction can be made. TLA+ can work at that level. You just can't look at Euclid's algorithm (or quicksort) in TLA+, and tell whether it's imperative or functional. It's an abstract mathematical description. > We have lambda calculus Lambda calculus is a state machine (or, more precisely, it is naturally described as a state machine). > You don't need a state machine to prove QuickSort works in a purely mathematical way, either, just statements about the equivalence of functions. What you're calling state and what TLA+ calls state is not the same thing. Whichever way you prove Quicksort works is the way you'd do it in TLA+ with state. You just don't call it state. I would, however, be very much interested to see how you prove Quicksort works using category theory. AFAIK, all approaches to verify QS work the same way, using an inductive invariant, namely an invariant on state. > that seemed to support the idea that FP and TLA+ have strengths for different kinds of programs I was talking about synchronous programming languages inspired by TLA+, and I agree. I would rather write a compiler in a pure-functional language than in a synchronous one, and an interactive program in a synchronous language than a pure-functional one. But that is a separate discussion from that about mathematical reasoning. I would agree that if one day there would be a FP-based verification tool that is aimed at engineers rather than researchers, then for ergonomics/syntax reasons, it's possible that it would be more convenient for reasoning about compilers. But there's nothing in the theory of TLA+ that makes it less convenient. I do, however, admit that there are tradeoffs between working in "pure math" as in TLA+, or within a programming language. There are often patterns that are specific to certain programming styles, and reasoning within a similar formalism may reduce effort. In other words, sometimes you may want to reason about a specific expression of an algorithm rather than about the algorithm in its pure abstract sense, and a formalism that shares the same expression style may make it easier. But I don't know how much of this is purely hypothetical. Most algorithms that are interesting or subtle, are essentially interesting or subtle, and verifying them in all formalisms is very similar (and usually involves the same proof technique: inductive invariants).

dgreensp 9y ago
Thanks for bearing with me, and responding, even if it might be more efficient for me to wait and read the next parts. It seems like if the quicksort of a list L is defined as equal to the concatenation of 1) the quicksort of the subsequence of L consisting of items less than the pivot item, 2) (the list containing) the pivot item, and 3) the quicksort of the subsequence of L consisting of items greater than the pivot, then we can prove properties like "any two items of the resulting list are in sorted order" by case analysis on whether each item is part of (1), (2), or (3). Maybe you would interpret "the quicksort of L is defined as..." to mean "if you're in state quicksort(L), you can proceed to state the-concatenation-of"? If we're working in the realm of mathematics, don't we get definitions, equations, and inductive proofs for free, without making a state machine do it? Edit: Reading more, I guess I'm just doing the sorting inside the "next-state relation" of a state machine, so it's done in one state transition, and saying you could look at quicksort as one way to factor the relation, which by math is equivalent to other ways to factor the relation that resemble other sorting algorithms.
- pron 9y ago
  > Reading more, I guess I'm just doing the sorting inside the "next-state relation" of a state machine, so it's done in one state transition While you could describe all of quicksort as a function in TLA+ (taking place instantaneously), that's no what you've done. You described a single state transition, but one that doesn't capture all of quicksort, just one partitioning step. To show that the result is sorted, you'd need to do an induction over such concatenations; the thing you're doing the induction over is called state.