<p>Here's an example from distributed computing:</p>

<hr>

<p><strong>1 Background</strong></p>

<p><strong>1.1 Asynchronous Shared Memory Model</strong></p>

<p>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 <em>asynchronous</em>, i.e., the 
adversary can delay the steps of nodes for any (finite) amount of time.<br>
You can think of a <em>step</em> 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.</p>

<p><strong>1.2 Safety and Liveness</strong></p>

<p>When formally reasoning about the properties of an asynchronous algorithm, 
we distinguish between safety and liveness properties. Informally, a 
<em>safety</em> 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.) <em>Liveness</em>, 
on the other hand, can be interpreted as "something good will eventually 
happen", e.g.: every node eventually terminates. </p>

<p>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 <em>execution</em> 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.</p>

<p>A safety property $S$ corresponds to some nonempty set $P\subseteq M$ that 
is <em>closed</em> 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 <em>finite</em> prefixes.</p>

<hr>

<p><strong>Applying Koenig's Infinity Lemma</strong></p>

<p>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 <a href="http://en.wikipedia.org/wiki/Linearizability" rel="nofollow">Linearizability</a>. 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. </p>

<p>[A] N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.</p>

CC BY-SA 3.0
2014-02-24T03:04:04.353Z
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)](http://iptps06.cs.ucsb.edu/papers/Chen-Cons06.pdf) 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.
hengxin
CC BY-SA 3.0
2014-02-26T08:34:59.427Z
I think that sequential consistency, causal consistency, and PRAM consistency are not safety properties, for they are not prefix-closed.
hengxin
CC BY-SA 3.0
2012-09-19T09:56:57.180Z
2012-09-19T09:56:57.180Z
Peter
<p>This is a follow-up question to <a href="https://cstheory.stackexchange.com/questions/12553/what-are-infinite-graphs-good-for">this one</a> about infinite graphs.</p>

<p>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, <a href="http://en.wikipedia.org/wiki/Koenig&#39;s_lemma" rel="nofollow noreferrer">Koenig's infinity lemma</a> is a very famous one.</p>

<p>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?</p>

CC BY-SA 3.0
2012-09-12T13:11:14.660Z
This seems a better fit for Mathematics.SE (or indeed, perhaps, MathOverflow).
Niel de Beaudrap
CC BY-SA 3.0
2012-09-13T14:23:35.823Z
As suggested by @NieldeBeaudrap, I posted the question over at Mathematics.SE. You can find it [here](http://math.stackexchange.com/questions/195224/what-can-we-prove-with-infinite-graphs-that-we-cannot-prove-without-them).
Gregor
<graph-theory><co.combinatorics><lo.logic>
What can we prove with infinite graphs that we cannot prove without them?
Gregor
# What can we prove with infinite graphs that we cannot prove without them?

(Asked by: username_0 on 2012-09-11)

This is a follow-up question to [this one](https://cstheory.stackexchange.com/questions/12553/what-are-infinite-graphs-good-for) 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](http://en.wikipedia.org/wiki/Koenig's_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?

**Tags:** graph-theory, co.combinatorics, lo.logic

> **Comments:**
> **username_1**: This seems a better fit for Mathematics.SE (or indeed, perhaps, MathOverflow).  
> **username_0**: As suggested by @NieldeBeaudrap, I posted the question over at Mathematics.SE. You can find it [here](http://math.stackexchange.com/questions/195224/what-can-we-prove-with-infinite-graphs-that-we-cannot-prove-without-them).  

---

## 1 answers

### Answer by username_2 on 2012-09-19. Score: 3

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](http://en.wikipedia.org/wiki/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.

> **Comments:**
> **username_3**: 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)](http://iptps06.cs.ucsb.edu/papers/Chen-Cons06.pdf) 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.  
> **username_3**: I think that sequential consistency, causal consistency, and PRAM consistency are not safety properties, for they are not prefix-closed.  

---

