The automata theoretic roots of process algebra.
Large State Machines and Sequential functions
Hartmanis “Loop free products”
Rabin-Scott Finite Automata and Their Decision Problems
One of the most important Computer Science papers introduced finite state machine language recognizers, the equivalence between non-deterministic and deterministic finite automata (in terms of what languages they recognize) , the Myhill congruences, etc.
A trivial theorem, more of a tautology, on networking and Turing’s deep theorem on decidability are both widely cited, widely misunderstood and widely misapplied in computer science. It is often claimed that Fischer, Lynch, Patterson (FLP) “theorem” on networks shows that we cannot reliably detect failure on a packet network and that Turing showed that no program exists that can always detect whether an arbitrary program will halt. Neither of those claims are true in computer programming. FLP applies only to “asynchronous networks” where there are no timeouts and where there are no probabilities to lean on so failures are not distinguishable from delays. These types of networks are rare. Turing’s result applies to abstract “programs” with unbounded memory and unbounded compute time, not to real programs that run on real computers. In both cases, people in computer science make the same error of conflating a precise definition of a term in a theorem with an informal definition used in engineering practice and this error leads to significant misunderstanding of how systems work.
There’s a good example of misuse of the FLP theorem in an ACM Queue article:
Perfect failure detectors are impossible to implement in a distributed system,9,15 in which it is impossible to distinguish between delay and failure. [ACM Queue]
The citation 15 above is to the FLP paper. In actual engineering systems, delay of over a certain duration is failure. This is easy to see in extreme: in the FLP model network nodes cannot distinguish between a peer that has not answered a query in 1 millisecond and a peer that has been silent for 10 years because the model excludes clocks of any kind. Is that a realistic model of a computer network? Consider a distributed consensus system in which the client cannot get responses from the coordinator. Normally, we can provide each device with a timer and have them enter a recovery mode if they don’t receive a response over a period chosen to meet the characteristics of the network and the requirements of the application. If a node does not receive a communication from the coordinator over the timeout period, it may be that the coordinator has crashed, or that there is a network problem, or that the coordinator is busy watching Sanctuary Moon and can’t be bothered to reply yet – in any of those cases, the important property is that the coordinator is not coordinating and a new one needs to be elected. Protocols for safe election of a new coordinator have been developed many times over the last 50 years or so – it is no mystery. Of course, like any engineered object, such a system is subject to failure when assumptions about probability or network properties are violated. We generally assume that spurious packets are not delivered and packets that have been corrupted in transit are detected, and that all participants follow the protocol (no Byzantine failure) and that Brownian motion doesn’t rip the network apart and deposit nodes into other networks, and that the power stays on etc. But none of these possibilities means we cannot have deterministically correct systems modulo reasonable assumptions.
As for Turing, according to Wikipedia,:
In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist. […] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input.
The link to the Wikipedia definition of “computer program” is what transforms this page from sloppy to wrong.
A computer program is a sequence or set of instructions in a programming language for a computer to execute. Computer programs are one component of software, which also includes documentation and other intangible components
And then “computer” is defined as one might expect:
A computer is a digital electronic machine that can be programmed to carry out sequences of arithmetic or logical operations (computation) automatically. Modern computers can perform generic sets of operations known as programs.
Turing machines are not either computers or computer programs under these definitions, so Turing’s theorem says nothing about the decision problem for computer programs. In fact, since computer programs executing on digital electronic devices correspond to finite state machines, the decision problem is trivial in terms of Turing machines. We can provide an actual computer program as an input to a Turing machine and have the Turing machine simulate execution until either a state repeats (which means the program would loop forever) or it terminates. Just because you call computer programs, programs, and can call Turing machine codes “programs” doesn’t mean they are the same things or that a theorem about one class of things applies to the other class of things.
There are several common, but incorrect rejoinders to this observation and one of them is on the Wikipedia page under a section titled “Common Pitfalls”. In this section it is noted that that finite state programs may have a lot of states so, in practice, it might be difficult to determine if they halt or otherwise verify system properties. Quoting Marvin Minsky:
…the magnitudes involved should lead one to suspect that theorems and arguments based chiefly on the mere finiteness [of] the state diagram may not carry a great deal of significance.
This exactly why one uses mathematics instead of hand waving. The “mere finiteness” of the state diagram is actually pretty important. A theorem that says no Turing Machine can solve the halting problem for all other Turing machines says absolutely nothing about how hard it is to validate large finite state machines. Big numbers are not unbounded numbers. In fact, Turing’s result does not even mean that some Turing machine could not, with very high probability, solve the halting program for a randomly chosen Turing machine. The undecidability of the halting problem for Turing machines has zero significance for engineering and, as Kurt Godel pointed out, not as much as it might initially appear for mathematics. There is a parallel Wikipedia page on decision problem which seems to be written more by mathematicians than computer scientists and it doesn’t make the same error but does discuss a number of computer programs that manage to work with very large numbers of states to solve real problems in mathematics and software engineering.
Practical decision procedures
Having practical decision procedures for classes of logical formulas is of considerable interest for program verification and circuit verification. Pure Boolean logical formulas are usually decided using SAT-solving techniques based on the DPLL algorithm. Conjunctive formulas over linear real or rational arithmetic can be decided using the simplex algorithm, formulas in linear integer arithmetic (Presburger arithmetic) can be decided using Cooper’s algorithm or William Pugh’s Omega test. Formulas with negations, conjunctions and disjunctions combine the difficulties of satisfiability testing with that of decision of conjunctions; they are generally decided nowadays using SMT-solving techniques, which combine SAT-solving with decision procedures for conjunctions and propagation techniques. Real polynomial arithmetic, also known as the theory of real closed fields, is decidable; this is the Tarski–Seidenberg theorem, which has been implemented in computers by using the cylindrical algebraic decomposition.
It turns out that in many important cases, it is possible to have one computer program evaluate another one or a mathematical theorem and tell us whether it is true or not. This is a hard problem, but not an impossible one. Mathematical results, even in computer science have meanings determined by the precise definitions of terms used in the theorems – they are not general statements about the world or metaphorical.
PAXOS – (c) Victor Yodaiken, 2022
These are the lecture notes, or see the paper.
1. Really clever distributed consensus algorithm by Leslie Lamport A. Infamously hard to understand - but not complicated B. Livelocks - can get stuck without reaching consensus C. Highly patented D. Widely used - supposedly. 2. Original paper: The Part Time Parliament, 1990 Most annoying CS paper ever published. 3. Paxos Made Simple, 2001. The key text: but it really describes 3 different algorithms. ==================================================== DISTRIBUTED CONSENSUS PROBLEM Network of computers (agents) that can lose messages but never corrupts them (semi-realistic) Agents can fail completely but don't lie or break the rules Proposer agents propose values Acceptor agents can accept proposals or reject them Goals: Majority of acceptors agree on value, Winning proposer sees agreement No more than one winning value (safety) ==================================================== SIMPLE SOLUTION - NOT PAXOS 1. One network "agent" is the only proposer 2. The proposer sends a proposed value to all acceptor agents until .. Acceptors send back acknowledgment messages 3. When the proposer has acks from a majority it knows it has won Use timeouts to make it more robust - Oki and Liskov, Viewstamped Replication, 1988 Use cycles for more efficiency Chang and Maxemchuk, Reliable Broacast Protocols, 1984 Use with "state machine" model for fault tolerance Borg, Baumbach, Glazer, A Message System Supporting Fault Tolerance 1983 ==================================================== PAXOS SOLVES THE PROBLEM OF TOO MUCH SIMPLICITY Key premise at start is the network is asynchronous (no clocks) (fashionable premise 1980s, not realistic) also that the algorithm needs multiple proposers (for fault tolerance, performance?) Clever idea: Multiple winning proposers ok - if they all propose the same value. 2 phase algorithm ensures that proposers converge on single winning value ==================================================== PAXOS MADE SIMPLE Pages 1-6 explain how the algorithm works Page 6, Lamport explains that the algorithm "livelocks" although it is safe Page 7: different algorithm also called Paxos that has a single proposer selected via timeouts (clocks) or randomization. Rest: the state machine model of fault tolerance using Paxos2 Question: What is advantage of Paxos2 over Simple Method? ==================================================== HOW DOES PAXOS1 SORT OF WORK? id numbers are unique per proposer and per proposal. (called "sequence numbers" in Paxos Made Simple) Proposers start in phase1 and ask acceptors to agree to their proposal id. When/if a majority of acceptors agree to the proposal id The proposer can pick a value, enter phase 2, and send its actual proposal When/if a majority of acceptors accept the proposal, the proposer wins Key: the messages agreeing to a proposal id carry the best (highest numbered) proposal the acceptor has accepted so far the proposer has to take (inherit) the value from the highest numbered one of those ==================================================== THERE ARE FOUR KINDS OF MESSAGES (phase1, id) - sent by proposers in phase 1 to acceptors (ok1, id, bestproposal ) -sent by acceptors to agree to phase 1 (phase2, id,value) - sent by proposers in phase 2 (ok2, id) - sent by acceptors to agree to phase 2 proposal Also messages reliably carry the identity of the original sender of the message ==================================================== ACCEPTORS ENFORCE ID ORDER Each acceptor A keeps track of A.BestID which is the highest id it has agreed to (either phase) A.BestID is initially 0 A.BestProposal =(phase2,id,value) the highest numbered proposal the acceptor has accepted A.BestProposal is initially null When an acceptor A receives m=(phase1,id) if m.id > A.BestID can send (ok1,m.id,A.BestProposal) back update A.BestId = m.id When an acceptor A receives m=(phase2,id,value) if m.id >= A.BestId can send (ok2,m.id) back and update A.BestProposal=m and A.BestId=m.id ==================================================== PROPOSERS CAN ABANDON THEIR NON-WINNING PROPOSALS They can pick a new id number that must be higher and still unique and start over at any time but it can still livelock forever Proposer 1 and 2 2 starts and gets a majority in phase 1 and then rests 1 starts and gets 1 less than a majority, blocks, increases number to 3, gets a majority for phase 1 ... repeat ===================================================== PROOF OF SAFETY: If only one proposal has won, nothing to prove If more than one proposal has won, let m_0 =(id0,value0) be the winning proposal with the lowest id number Let L = (m_0,m_1,m_2 ... m_N) add to m_0, in id order, the complete list of proposals with m_i.id > m_0.id that have been sent by some proposer, If m_i is on the list, the proposer of m_i reached phase2 with id m_i.id L includes all winning proposals plus more Claim: All of these must have the same value v = m_0.value. ==================================================== WHY? P0 sent m_0 and received (ok2,m_0.id) from a majority of acceptors because we chose it as the lowest numbered WINNING proposal if P sent proposal m_i, i>0, then P got (ok1,m_i.id, best) from a majority of acceptors The two majority sets of acceptors must intersect at some A A must have sent (ok2,m_0.id) BEFORE it sent (ok1,m_i.id,A.BestProposal) since m_i.id > m_0.id When A agrees to m_i.id it already accepted m_0, so A.BestProposal was not null and m_0.id <= A.BestProposal.id < m_i.id P must have inherited at least 1 proposal m with m_0.id <= m.id < m_i.id ==================================================== BACK TO LIST FOR INDUCTION L = (m_0,m_1,m_2 ... m_N) CLAIM i >= 0 implies m_i.value = m_0.value. Proof by induction. True for i=0 Suppose true for 0,... j-1 and consider j the proposer P of m_j inherited some best message m with m_0.id <= m.id < m_j.id and since m was sent, the proposer of m must have reached phase2 so m must be on the list. Since m.id < m_j.id and it is on the list, m.value = m_0.value and so m_j.value = m_0.value QED.
This paper is an experiment in presenting programming algorithms as recursive functions, without pseudo-code or genuine code. The algorithms presented are the standard basic sorting algorithms with some computational complexity analysis. The style is that of ordinary working mathematics although the case statements of the recursive functions look a lot like pattern matching.
“Turing’s work was of course a great contribution to the world of mathematics, but there is a question of exactly how it is related to the world of computing. – Wilkes
The undecidability of the halting problem for Turing machines is not relevant to computer programming and provides no information about whether there can be computer programs that automatically check the correctness of other computer programs. Knowing that some problem is Turing decidable or Turing undecidable doesn’t mean you know anything about how hard it is for actual computer programs on physical computers.
Much of the confusion comes from sloppy definitions of “program” and “halting problem”. Martin Davis appears to have coined the term halting problem to refer to the problem of deciding whether a Turing machine ever halts when started with a particular configuration. That halting problem is not Turing decidable. There is no Turing machine which given input \((n,m)\) is guaranteed to decide whether Turing machine \(T_n\) with input \(m\) will eventually halt. But there are Turing machines which take input \((s,n,m)\) and decide if \(T_n\) halts within \(s\) steps (or \(2^s\) steps or \(10^{10^{100000\times s}}\)) steps. It is Turing trivial to determine whether a Turing machine halts within the expected lifespan of the Milky Way given the most optimistic non-zero time for each step to complete. For most purposes, a Turing machine that takes galactic time to complete a computation never completes it.
Even in foundations of mathematics, the difference between “never halts” and “takes too long” is not always important. Kurt Gödel wrote that if decision processes worked in linear or exponential time, “this would have consequences of the greatest importance . Namely, it would obviously mean that in spite of the undecidability of the Entscheidungsproblem, the mental work of a mathematician concerning Yes-or-No questions could be completely replaced by a machine. After all, one would simply have to choose the natural number n so large that when the machine does not deliver a result, it makes no sense to think more about the problem.”
It’s trivially Turing decidable whether a Turing machine can complete within some time using some fixed number of states but is it feasible for computer programs to decide that? It seems hard. The two criteria: “feasible for computer programs” and “Turing decidable” are very different. However, the critical importance of the halting problem for Turing machines in computer science is folkloric and anyone bringing up these pesky facts will likely get one of the standard confused responses
Much of the confusion is caused by mixing-up informal explanations with mathematics. Turing’s Entscheidungsproblem paper proposes a specific model of “computable”, arguing that the informal notion of “algorithm” in mathematics can be formalized by a type of automata that is now known as Turing machine. Once this notion is made precise, it is possible to look at the properties of these algorithms and to prove some theorems about what Turing machines can and cannot compute. But “Turing machines” are not physical computers. The first sentence of the current Wikipedia page on “Halting Problem” is a good example of imprecision leading to error:
“In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running (i.e., halt) or continue to run forever. “
The definition of “computability theory” linked in the text starts “Computability theory, also known as recursion theory“, firmly placing the topic in metamathematics. But the definition of “computer program” linked in the text is concerned with programs on physical digital computers. Determining whether such a program halts is Turing Trivial yet the next sentence in the Wikipedia article jumps back to Turing machines:
“Alan Turing proved in 1936 that a general algorithm to solve the halting problem for all possible program-input pairs cannot exist”.
So we’ve jumped from recursion theory to computer programs on physical computers to calling Turing machines “programs”. And then a jump back:
“The theoretical conclusion of not solvable is significant to practical computing efforts, defining a class of applications which no programming invention can possibly perform perfectly.”
Nope. Similar sounding words don’t necessarily have the same meaning. A mathematical proof about the limitations of “computable functions” should not be handwaved around to show something about physical computers and programs running on those computers.
These remarks from “THE GENERAL AND LOGICAL THEORY OF AUTOMATA” 1947 are enormously insightful – no surprise. Von Neumann essentially predicts the emergence of the field of analysis of algorithms and algorithmic complexity. Not only does he point out the importance of understanding how many steps it will take to carry out a computation, but the use of asymptotic measures and other tools from analysis and working mathematics proved to be as important as von Neumann suggested. The cautions about formal logics are important still, because too much of theoretical CS is still fixated on foundational methods and formal logic, despite the “refractory” nature of of the methods.
There exists today a very elaborate system of formal logic, and, specifically, of logic as applied to mathematics. This is a discipline with many good sides, but also with certain serious weaknesses. This is not the occasion to enlarge upon the good sides, which I have certainly no intention to belittle. About the inadequacies, however, this may be said: Everybody who has worked in formal logic will confirm that it is one of the technically most refractory parts of mathematics. The reason for this is that it deals with rigid, all-or-none concepts, and has very little contact with the continuous concept of the real or of the complex number, that is, with mathematical analysis. Yet analysis is the technically most successful and best-elaborated part of mathematics. Thus formal logic is, by the nature of its approach, cut off from the best cultivated portions of mathematics, and forced onto the most difficult part of the mathematical terrain, into combinatorics. The theory of automata, of the digital, all-or-none type, as discussed up to now, is certainly a chapter in formal logic. It would, therefore, seem that it will have to share this unattractive property of formal logic. It will have to be, from the mathematical point of view, combinatorial rather than analytical.
Probable Characteristics of Such a Theory. Now it seems to me that this will in fact not be the case. In studying the functioning of automata, it is clearly necessary to pay attention to a circumstance which has never before made its appearance in formal logic. Throughout all modern logic, the only thing that is important is whether a result can be achieved in a finite number of elementary steps or not. The size of the number of steps which are required, on the other hand, is hardly ever a concern of formal logic. Any finite sequence of correct steps is, as a matter of principle, as good as any other. It is a matter of no consequence whether the number is small or large, or even so large that it couldn’t possibly be carried out in a lifetime, or in the presumptive lifetime of the stellar universe as we know it. In dealing with automata, this statement must he significantly modified. In the case of an automaton the thing which matters is not only whether it can reach a certain result in a finite number of steps at all but also how many such steps are needed. There are two reasons. First, automata are constructed in order to reach certain results in certain pre-assigned durations, or at least in pre-assigned orders of magnitude of duration. Second, the componentry employed has in every individual operation a small but nevertheless non-zero probability of failing. In a sufficiently long chain of operations the cumulative effect of these individual probabilities of failure may (if unchecked) reach the order of magnitude of unity-at whichpoint it produces, in effect, complete unreliability. The probability levels which are involved here are very low, but still not too far removed from the domain of ordinary technological experience. It is not difficult to estimate that a high-speed computing machine, dealing with a typical problem, may have to perform as much as \(10^{12}\) individual operations. The probability of error on an individual operation which can be tolerated must, therefore, be small compared to \(10^{12}\). I might mention that an electromechanical relay ( a telephone relay) is at present considered acceptable if its probability of failure on an individual operation is of the order \(10^{-5}\). It is considered excellent if this order of probability is \(10^-9\). Thus the reliabilities required in a high-speed computing machine are higher, but not prohibitively higher, than those that constitute sound practice in certain existing industrial fields. The actually obtainable reliabilities are, however, not likely to leave a very wide margin against the minimum requirements just mentioned. An exhaustive study and a nontrivial theory will, therefore, certainly be called for. Thus the logic of automata will differ from the present system of formal logic in two relevant respects. 1. The actual length of “chains of reasoning,” that is, of the chains of operations, will have to be considered. 2. The operations of logic (syllogisms, conjunctions, disjunctions, negations, etc., that is, in the terminology that is customary for automata, various forms of gating, coincidence, anti-coincidence, blocking, etc., actions) will all have to be treated by procedures which allow exceptions ( malfunctions ) with low but non-zero probabilities. All of this will lead to theories which are much less rigidly of an all-or-none nature than past and present formal logic. They will be of a much less combinatorial, and much more analytical, character.
Pearl: Of course, but you cannot see this noble aspiration in scientific equations. The language of algebra is symmetric: If x tells us about y, then y tells us about x. I’m talking about deterministic relationships. There’s no way to write in mathematics a simple fact—for example, that the upcoming storm causes the barometer to go down, and not the other way around.
Mathematics has not developed the asymmetric language required to capture our understanding that if x causes y that does not mean that y causes x. It sounds like a terrible thing to say against science, I know. If I were to say it to my mother, she’d slap me.
(from the Atlantic)
What is he talking about? Isn’t that exactly what state machines do?
