A Coinductive Formulation of the “Coinduction Theorem” by Michael and Appel

Andreas Abel^{∗}

June 26, 2000

1 Inductive Treatment of Safety

In [MA00] Neophytos G. Michael and Andrew W. Appel introduce machine safety for a transition relation ↦ on the set of machine states S as follows:

Safe(s) :⟺ ∀s′. s ↦^{∗} s′ ⇒ ∃s′′. s′ ↦ s′′

This expresses that a state is safe if after a finite number of transitions starting from this state there is still one more possible transition. Given an invariant Inv ⊆ S, written Inv(s) for s ∈ Inv, they define the properties progress and preservation by:

Prog(Inv) :⟺ ∀s. Inv(s) ⇒ ∃s′. s ↦ s′
Pres(Inv) :⟺ ∀s, s′. Inv(s) ∧ s ↦ s′ ⇒ Inv(s′)

Prog states that an invariant enables progress if it enables a further transition step. Pres expresses that the invariant is preserved by the step relation. It is clear that a progressive and preserved invariant that holds for the initial state guarantees safety, which they state in the “coinduction theorem”:

Inv(s_{0})  Prog(Inv)  Pres(Inv)
Safe(s_{0})

Assuming progression and preservation of Inv globally, the theorem can be reformulated as

{Inv(s_{0}) s_{0} ↦^{∗} s′ \atop ∃s′′.s′ ↦ s′′}

This is easily proven by induction on s_{0} ↦^{∗} s′:

• Case s_{0} = s′: Immediately by Prog(Inv).

∗abel@cs.cmu.edu, Carnegie Mellon University, Pittsburgh, PA, USA.

• Case s_{0} ↦ s ↦^{∗} s′: Preservation yields Inv(s), on which we apply the induction hypothesis for s ↦^{∗} s′. □

In the following we show how to define Safe as a coinductive set and how to prove the “coinduction theorem” by coinduction. But first we introduce the concepts of coinduction in duality to these of induction.

2 Induction and Coinduction

Given a complete lattice of sets (P(S), ⊆) and a monotone operator F : P(S) → P(S) we can use the theorem of Knaster and Tarski to construct the least fixpoint μ of F. It is characterized as the least pre-fixpoint of F, which we write down as follows:

(intro) F(μ) ⊆ μ
(elim) ∀P ⊆ S. F(P) ⊆ P ⇒ μ ⊆ P

This characterization is equivalent to the explicit definition of the least fixpoint via

μ := ⋂{P | F(P) ⊆ P }

The first condition stipulates that μ is a pre-fixpoint of F, and the second minimality. The names are not chosen by accident, since these two properties actually show how to introduce and eliminate members of the inductive set μ. This can be seen more clearly in rule notation.

(intro) {s ∈ F(μ) \atop s ∈ μ}  (elim) {s ∈ μ  ∀s′ ∈ F(P). s′ ∈ P \atop s ∈ P}

A simple example for an inductive set are the natural numbers ℕ which are generated by the operator F(Q) := {0, 1 + n | n ∈ Q}. The rule (elim) simply becomes the natural numbers induction scheme for predicate P.

Dually to inductive sets, a coinductive set ν is defined as the greatest fixpoint of a monotone operator ν. Post-fixpoint condition and maximality read

(coIntro) ν ⊆ F(ν)
(coElim) ∀P ⊆ S. P ⊆ F(P) ⇒ P ⊆ ν

This equals the definition

ν := ⋃{P | P ⊆ F(P)}

The condition (coIntro) is dual to (intro), thus it is actually an elimination rule. Likewise (coElim) is an introduction rule.

(coIntro) {s ∈ ν \atop s ∈ F(ν)}  (coElim) {s ∈ P  ∀s′ ∈ P. s′ ∈ F(P) \atop s ∈ ν}

As an example consider the set ℕ^{ω} of infinite streams of natural numbers. They are formed by the operator F(Q) := {a | head a ∈ ℕ, tail a ∈ Q} and obey the following instances of (coIntro) and (coElim)

(ℕ^{ω}Elim) a ∈ ℕ^{ω}

head a ∈ ℕ tail a ∈ ℕ^{ω}

(ℕ^{ω}Intro) a ∈ P ∀a′ ∈ P. head a′ ∈ ℕ ∧ tail a′ ∈ P

a ∈ ℕ^{ω}

To show that the stream of zeros 0^{ω} = (0, 0, …) is a stream of natural numbers, we use (ℕ^{ω}Intro) on the set P = {0^{ω}}.^{1}

Now back to our problem!

3 Coinductive Treatment of Safety

A state s is safe if from it a state s′ can never be reached s.th. no further step is possible. We also could say that every transition sequence starting with s is infinite. Hence safety is a candidate for coinduction. We can define Safe by the rule

(SafeE)

Safe(s)
s ↦ s′ Safe(s′)

This reads “from a safe state s there exists a transition to another safe state s′” which is a characterization of the safe states. Interpreting this rule in the coinductive manner, we obtain the operator F(Q) := {s ∈ Q | ∃s′ ∈ S. s ↦ s′ ∧ s′ ∈ Q} on sets of states Q ⊆ S. The co-elimination rule for Safe is

(SafeI) {P (s)  ∀s′. P (s′) ⇒ ∃s′′. s′ ↦ s′′ ∧ P (s′′) \atop Safe(s)}

Assuming Prog(Inv) and Pres(Inv) globally as before, we can restate the safety theorem as

{Inv(s_{0}) \atop Safe(s_{0})}

We prove it by coinduction on Safe(s_{0}), i.e., we apply the rule (SafeI). Therefore we need an instantiation for P with the properties:

1. P (s_{0})

2. P (s′) ⇒ ∃s′′. s′ ↦ s′′ ∧ P (s′′)

We choose P = Inv. The first condition is the assumption, the second follows immediately from Prog(Inv) and Pres(Inv). □

1This may sound a little strange and one could as oneself “How do I actually get a stream?”.

The point is that inductive data is constructed (synthesized), whereas coinductive codata like streams etc. is consumed (analyzed).

4 Conclusion

We have demonstrated that the definition of safety can be simplified by means of coinduction. The original formulation “a state is safe if every transition sequence starting in it can be extended” has been changed into “a state is safe if the next state is still safe”. Instead of defining the reflexive-transitive closure ↦^{∗} of the step relation as a means to define safety, we can define safety directly. The coinductive proof is very natural and makes clear that a progressive and preserved invariant implies safety immediately.

References

[JR97] B. Jacobs and J.J.M.M. Rutten. A tutorial on (co)algebras and (co)induction. In Bulletin of EATCS, volume 62, pages 222–259, 1997.

[MA00] Neophytos G. Michael and Andrew W. Appel. Machine Instruction Syntax and Semantics in Higher Order Logic. In David McAllester, editor, Automated Deduction – CADE-17, volume 1831 of Lecture Notes in Artificial Intelligence, pages 7–24. Springer, June 2000.