### Sorting and groups

I can't find much reference to this in the literature (see Maus for some hints and an interesting paper) , but surely people have looked at sorting as a problem in group theory? Given a sequence $latex s=[x_1\dots x_n]$ say a permutation $latex \pi$ sorts $latex s$ if and…

### Basic math for basic algorithms

It's odd that all the descriptions of basic programming operations, such as sorting, rely on pseudo code or complex formal logic. All we are doing is modifying finite sequences so it seems like we should be able to use ordinary algebra. I'm going to start by defi ning basic operations on…

### Understanding Paxos and Distributed Consensus

(minor wording correction and more complaining added 10/2/2016, minor edits 10/5/2016) Multi-proposer Paxos is a very clever and notoriously slippery algorithm for obtaining distributed consensus. In this note I try to explain it clearly and provide a correctness proof that gives some intuition why it works – to the extent…

### circularity problems in distributed consensus

Distributed consensus involves organizing a collection of independent agents - processes or network sites - to agree on some value or sequence of values.  Many distributed consensus methods depend on a leader-follower scheme in which the leader is an agent that essentially tells the followers what the values are. The…

### state equations in practice

When people think of mathematical models of state for programs and other computer systems, it's natural and conventional to consider state as a map from symbolic names of state variable to values. This is an error for a number of reasons including, most critically, the lack of any compositional…

### Operations and maps on finite sequences

A lot of what I'm trying to do with mathematical models of computer systems involves operations on finite sequences. Define a "finite sequence of length n>0" to be any total map f: {1 ... n} → X for some set X. The 0-length sequence is the null map  "nulls". If f…