15
$\begingroup$

This is a follow-up question to this one about infinite graphs.

Answers and comments to that question list objects and situations which are naturally modeled by infinite graphs. But there are also numerous theorems about infinite graphs (see chapter 8 in Diestel's book) of which, for example, Koenig's infinity lemma is a very famous one.

Now I have the following question: What can we prove with infinite graphs that we cannot prove without them? Or more specifically, what is an example where we model something as an infinite graph, then invoke a theorem about infinite graphs, and in the end have proved something about the original problem -- without knowing how to prove it otherwise?

$\endgroup$
  • 5
    $\begingroup$ This seems a better fit for Mathematics.SE (or indeed, perhaps, MathOverflow). $\endgroup$ – Niel de Beaudrap Sep 12 '12 at 13:11
  • $\begingroup$ As suggested by @NieldeBeaudrap, I posted the question over at Mathematics.SE. You can find it here. $\endgroup$ – Gregor Sep 13 '12 at 14:23
3
$\begingroup$

Here's an example from distributed computing:


1 Background

1.1 Asynchronous Shared Memory Model

Let's consider a collection of distributed nodes that communicate using shared memory variables. There is an adversary that controls when a node take steps and when to deliver messages. The computation is asynchronous, i.e., the adversary can delay the steps of nodes for any (finite) amount of time.
You can think of a step of a node as a state transition of its local automaton (according to the algorithm) where the next state is determined by the current state and the observations of the node since the last step.

1.2 Safety and Liveness

When formally reasoning about the properties of an asynchronous algorithm, we distinguish between safety and liveness properties. Informally, a safety property can be interpreted as a guarantee that something "bad" never happens. (E.g., for mutual exclusion, a safety property would be that no two nodes enter the critical section simultaneously.) Liveness, on the other hand, can be interpreted as "something good will eventually happen", e.g.: every node eventually terminates.

To formalize safety, we consider the infinite set ${M}$ of all possible executions of all possible algorithms, taking into account all possible choices of the adversary. An execution is an infinite sequence of steps. We can define a metric on $M$ by taking the distance between two distinct runs $\alpha,\beta \in M$ to be $2^{-n}$ where $n$ is the first index where $\alpha$ and $\beta$ differ.

A safety property $S$ corresponds to some nonempty set $P\subseteq M$ that is closed in the sense that the limit of an infinite sequence of runs in $P$ cannot be in $M\setminus P$. So once we know that some property is a safety property, it is sufficient to show that this property holds on finite prefixes.


Applying Koenig's Infinity Lemma

It's not always straightforward to see whether a specific property is a safety property: Consider the implementation of read/write atomic objects on top of basic shared memory variables. Such an implementation should handle requests and their responses in a way that makes them look as if they happen at some instant in time and don't violate their order of invocation. (Due to the asynchronous operation, the actual duration between request and response might be nonzero.) Atomicity is also known as Linearizability. Section 13.1 of [A] gives a proof that Atomicity is a safety property. The proof uses Koenig's lemma to show that the limit of any infinite sequence of executions (each of which satisfies Atomicity) also satisfies Atomicity.

[A] N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.

$\endgroup$
  • $\begingroup$ Good to know that Atomicity is a safety property. Are there similar formal results about other consistency conditions, such as sequential consistency, causal consistency, PRAM consistency, and eventual consistency in the literature? The paper (section 2.2) claims that causal consistency is a safety property while eventual consistency is a liveness property. However, they are not formally stated. I am not sure whether these two terms are used in the formal way. $\endgroup$ – hengxin Feb 24 '14 at 3:04
  • $\begingroup$ I think that sequential consistency, causal consistency, and PRAM consistency are not safety properties, for they are not prefix-closed. $\endgroup$ – hengxin Feb 26 '14 at 8:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.