Let's say we have a simulation relation e′ ~ e ("e′ simulates e") and a proof that for any step in a specification semantics:

ewe have related terms e_{1}→ e_{2}

_{1}′ ~ e

_{1}and e

_{2}′ ~ e

_{2}such that

eIt's easy to show by induction that if the specification semantics converges to a value then the implementation semantics converges to a related value. If the specification semantics diverges, i.e. has an infinite reduction sequence, then we'd like to show the implementation diverges too._{1}′ →^{+}e_{2}′

König's Lemma states that for any finitely branching tree, if there exists a path of length n from the root for any n, then there exists an infinite path from the root. Consider the tree of possible reduction sequences from a term, where branches indicate points of non-determinism in the semantics. If every point of non-determinism has only a finite number of alternative reductions, then the tree is finitely branching.

So now consider a diverging term e in the specification semantics. For any finite prefix of the infinite reduction sequence, we can easily show by induction that there is a reduction sequence in the implementation semantics of equal or greater length. Since the computation tree of the implementation term is finitely branching, König's Lemma provides an infinite reduction of the implementation.

## 2 comments:

hello

i didn't know how to contact you, so i'm posting a message on your blog-- hope that's ok. i've been wanting to know how to write "timshel" in hebrew, and i was wondering how you found out how to write it. is that the word you have in hebrew in the lefthand corner of your home page?

thanks!

you can e-mail me at kimmi275@ufl.edu

-kim-

Hi Dave,

Google reader cunningly recommended your blog to me. It was a bit frightening how spot on it was :o)

Here is a small similar useage of the König's lemma:

http://seta07.blogspot.com/2007/09/solution-to-exercise-34-in-nn.html

cheers,

Arnar

Post a Comment