On Extension of Parameterized Coinduction
パラメーター付き余帰納法の拡張についてby
Masaki Hara
原将己

A Senior Thesis
卒業論文

Submitted to
the Department of Information Science
the Faculty of Science, the University of Tokyo
on February 02, 2016
in Partial Fulfillment of the Requirements
for the Degree of Bachelor of Science
Thesis Supervisor: Ichiro Hasuo 蓮尾一郎
Associate Professor of Information ScienceABSTRACTMost properties on software correctness are described by means of (combinations of)greatest and least fixed points. Therefore it is of interest to provide techniques for proving
such specifications in a proof assistant.
In 2013, Chung-Kil Hur et al. proposed one of such techniques: parameterized coinduction. It assists one to interactively construct a loop invariant, which one can use toprove properties described by greatest fixed points.
We analyze the technique from two points of view. Firstly, we define a dual counterpart: parameterized induction to prove properties described by least fixed points.
Although it has a similar form to parameterized coinduction, one has to provide a ranking function to guarantee that the program in question halts eventually. Secondly, we
give a mathematical characterization of how powerful the technique is.

論文要旨
ソフトウェアの正しさは、最大不動点と最小不動点 (の組み合わせ) で記述される。したがって、証明支援系でこれらの仕様を証明するための手法を与えることには意味がある。

2013 年に Chung-Kil Hur et al. は、そういった手法のひとつである、パラメーター付き余帰納法と呼ばれる手法を提案した。この手法を用いると、最大不動点で表される性質を証明するために必要なループ不変条件を、対話的に構成することができる。
この論文では、パラメーター付き余帰納法を二つの観点から分析する。はじめに、この手法の双対にあたる、最小不動点で表される性質の証明のためのパラメーター付き帰納法
を定義する。これはパラメーター付き余帰納法とよく似た形だが、プログラムがいずれ停止することを保証するために、 ranking function を与える必要があるという違いがある。
続いて、この手法がどれほど強力であるかを数学的に特徴づける。

Acknowledgements
I appreciate Ichiro Hasuo’s helpful advice.

Contents

1 Introduction
1.1 Induction and Coinduction . . . . . . . . . . . . . . . . . . . . . .
1.2 Parameterized Coinduction . . . . . . . . . . . . . . . . . . . . . .
1.3 Our Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4 Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1
1
1
2
2

2 Preliminaries
2.1 Backgrounds on Induction and Coinduction . . . . . . . . . . . . .
2.2 Examples of Coinduction and Induction . . . . . . . . . . . . . . .
2.3 Parameterized Coinduction: A Review . . . . . . . . . . . . . . . .

3
3
5
6

3 Parameterized Induction
9
3.1 Motivating Example: Reachability Problem in Pushdown Systems
9
3.2 Parameterized Least Fixed Points . . . . . . . . . . . . . . . . . . . 9
3.3 The Indexed Accumulation Property . . . . . . . . . . . . . . . . . 10
3.4 Example Proof with Parameterized Least Fixed Points . . . . . . . 11
4 Functional Characterization of Parameterized (Co)Induction
4.1 Test Functions Generalizing Parameterized (Co)Induction . . . . .
4.2 Interderivability of Accumulation and Composition . . . . . . . . .
4.3 Characterization of Parameterized Coinduction . . . . . . . . . . .
4.4 Characterization of Parameterized Induction . . . . . . . . . . . .

13
13
13
14
14

5 Predicate Characterization and No-discovery Parameterized (Co)Induction 16
5.1 Motivating Example: Infinite State System . . . . . . . . . . . . . 16
5.2 Test Predicates Generalizing Test Functions . . . . . . . . . . . . . 17
5.3 Generalization of the Unfolding Property and the Accumulation
Property . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
5.4 Characterization of No-discovery Parameterized Induction . . . . . 19
5.5 Characterization of No-discovery Parameterized Coinduction . . . 20
5.6 Examples and Counterexamples . . . . . . . . . . . . . . . . . . . . 20
6 Conclusions and Future Work

22

References

23iv

Chapter 1
Introduction
1.1

Induction and Coinduction

Induction and coinduction are used to define models and properties of computer
systems, and therefore they are indispensable in computer science. Examples of
inductive and coinductive models include computer programs and their traces ofexecution. Properties of these systems are also described by means of induction
and coinduction: that a program halts eventually, that two parallel tasks areprocessed fairly, and that two programs behave in the same way.

1.2

Parameterized Coinduction

Consequently, techniques for automated theorem provers and proof assistants
aimed at induction and coinduction have been developed. Among these techniques, parameterized coinduction is proposed recently, especially for proof assistants.
In proof assistants like Coq, we do not need to write whole proof trees; instead,we specify how to construct proof trees. For example, a proof tree for ¬¬(P ∨¬P )is shown in Figure 1.1 and a proof in Coq for the same proposition is shownin Listing 1.1. There is a big diﬀerence: in the Coq proof script, there are
no appearances of intermediate propositions; there are only tactic names andhypotheses names. This is especially convenient if the proposition in question islong.
However, the standard proof technique for coinductive properties, which uses
the Knaster-Tarski theorem, does not work well in these proof assistants, in termsof giving short proofs. To use the Knaster-Tarski theorem, we have to provide
beforehand a proposition called “invariant.” To make matters worse, invariants
are often long and complex.
¬(P ∨ ¬P ), P ⊢ P¬(P ∨ ¬P ), P ⊢ ¬(P ∨ ¬P )¬(P ∨ ¬P ), P ⊢ P ∨ ¬P¬(P ∨ ¬P ), P ⊢ ⊥¬(P ∨ ¬P ) ⊢ ¬P¬(P ∨ ¬P ) ⊢ ¬(P ∨ ¬P )¬(P ∨ ¬P ) ⊢ P ∨ ¬P¬(P ∨ ¬P ) ⊢ ⊥⊢ ¬¬(P ∨ ¬P )Figure 1.1: A proof tree for ¬¬(P ∨ ¬P )1

Listing 1.1: A Coq proof for ¬¬(P ∨ ¬P )
1
2
3
4
5
6
7
8
9
10

Theorem DNLEM(P : Prop) : ¬¬(P ∨Proof.
intros H.
apply H.
right.
intros HP.
apply H.
left.
exact HP.
Qed.

¬P).

Parameterized coinduction is a technique for overcoming the problem. In
parameterized coinduction, we are to prove propositions called parameterized
greatest fixed points, instead of usual greatest fixed points. This enables us togradually increase during an interactive proof a coinductive hypothesis, which
will eventually be an invariant.

1.3

Our Contribution

We have two contributions regarding parameterized coinduction.
• We introduce parameterized induction, which is similar to parameterizedcoinduction, to prove inductively defined properties.
• Although parameterized greatest fixed points are more convenient thanusual greatest fixed points, there have been no mathematical backgrounds
to support this intuition. We give a mathematical characterization of thepower of parameterized induction and parameterized coinduction.

1.4

Related WorkFor model-checking purposes, assertions to be checked are often expressed in
the modal µ-calculus, and processes and programs are checked against theseproperties. For example, Pratt [14] and Kozen [12] each propose a model-checking
algorithm for a fragment of the modal µ-calculus. Wilke [19] proposes algorithms
for the model-checking and the satisfiability problem for the full modal µ-calculus,by translating propositions into alternating tree automata.
Non-classical variants of the modal µ-calculus are also considered. Baelde
and Miller [2] propose a first-order multiplicative-additive fragment of linear
logic augmented with equalities and fixed point operators µMALL= and prove
cut-elimination theorem for the logic. Hasuo et al. [8] propose a categoricalframework, which is called a coalgebraic modal µ-calculus CµΓ,Λ , and give amodel-checking algorithm for some of them.
The idea of adding parameters to fixed point operators is originally used formodel-checking purposes by Winskel [20]. The idea of accumulated knowledge isolder than parameterization and can be dated back to Kozen [12].
Stirling and Walker [17] propose local model checking, a top-down approach
to model checking. Interactive proof in proof assistants is similar to local model
checking in that we write a proof in a top-down manner.

2Chapter 2
Preliminaries
2.1

Backgrounds on Induction and Coinduction

Although many applications of induction and coinduction are about completeboolean algebras, inductive and coinductive properties can be described in apreordered set in general.
Definition 2.1.1 (Preordered sets). A preordered set (C, ⊑) is a set C with areflexive and transitive binary relation (⊑) ⊆ C × C.
We write x ≡ y if both x ⊑ y and y ⊑ x holds.
Minimum elements are unique up to equivalence, if they exist. We write ⊥for one of them. We write ⊤, x ⊔ y, and x ⊓ y for a maximum element, least upperbounds, and greatest lower bounds, respectively.
In this situation, coinductive and inductive properties are defined as greatest
and least fixed points. See e.g. [1] for details.
Definition 2.1.2 (Greatest fixed points and least fixed points). Let (C, ⊑) be apreordered set and f : C → C be a function.
An element x ∈ C is a fixed point of f if f (x) ≡ x holds.
An element x ∈ C is a least fixed point of f if x is a minimum element among
fixed points of f . Similarly, an element x ∈ C is a greatest fixed point of f if x isa maximum element among all the fixed points of f .
Least fixed points and greatest fixed points are unique (if they exist) up toequivalence. We write µf for a least fixed point of f , and νf for a greatest
fixed point of f . We write µx. t and νx. t as shorthands for µ(λx. t) and ν(λx. t),
respectively.
Especially, as proven later, (C, ⊑) has all greatest and fixed points of monotonefunctions, if it is a complete lattice.
Definition 2.1.3 (Complete lattices). A preordered set (C, ⊑) is a complete
lattice, if it has one of the following equivalent properties:
1. It has all joins: for each subset A ⊆ C, there is a minimum element among
the upper bounds of A.
2. It has all meets: for each subset A ⊆ C, there is a maximum element among
the upper bounds of A.
Usually only a partially ordered set with such a property is called a complete
lattice. This is a natural generalization of the definition.
Before presenting the Knaster-Tarski theorem, we first define prefixed points
and postfixed points.
3

Definition 2.1.4 (Prefixed points and postfixed points). Let (C, ⊑) be a preordered set and f : C → C be a function.
An element x ∈ C is a prefixed point of f if f (x) ⊑ x holds.
Dually, an element x ∈ C is a postfixed point of f if x ⊑ f (x) holds.
We show a less general form of the Knaster-Tarski theorem. See [18] for thegeneral statement.
Theorem 2.1.5 (Knaster-Tarski). Let (C, ⊑) be a complete lattice. For f : C →C a monotone function, there exists νf and the following equivalence holds:⊔
νf ≡{ r ∈ C | r ⊑ f (r) } .
Dually, for f : C → C a monotone function, there exists µf and the following
equivalence holds:lµf ≡{ r ∈ C | f (r) ⊑ r } .
In other words, greatest fixed points are greatest postfixed points and least fixed
points are least prefixed points.
⊔
Proof. Let x be { r ∈ C | r ⊑ f (r) }.
Let r be a postfixed point of f . We have r ⊑ x. By monotonicity of f , wehave r ⊑ f (r) ⊑ f (x).
Thereforex ⊑ f (x) by definition of x.
()
Since f (x) ⊑ f f (x) by monotonicity, f (x) is a postfixed point of f . Therefore f (x) ⊑ x by definition of x.
Since we have x ⊑ f (x) and f (x) ⊑ x, x is a fixed point. Let y be anotherfixed point of f⊔. Since y is a postfixed point, we have y ⊑ x by definition of x.
Therefore x = { r ∈ C | r ⊑ f (r) } is a greatest fixed point.
The Knaster-Tarski theorem describes µf as an infimum of a certain set. In
contrast, Kleene fixed point theorem, a special version of which appears in [11],describes µf as a supremum of a certain sequence. We give a more general
theorem, dropping Scott-continuity restriction. See the paper of Cousot andCousot [4] and the paper of Echenique [6] for detail.
Definition 2.1.6 (Upper iteration sequence). Let (C, ⊑) be a complete lattice,f : C → C be a monotone function, and x ∈ C be a postfixed point of f .
For an ordinal number α, an element of an upper iteration sequence f α (x) is
defined inductively as follows:f 0 (x) = x()
f α+1 (x) = f f α (x)⊔f α (x) =f β (x)if α is a limit ordinal.

β<αDually, for a prefixed point x ∈ C of f and an ordinal number α, an elementof a lower iteration sequence f α (x) is defined inductively as follows:f 0 (x) = x()
f α+1 (x) = f f α (x)lf α (x) =f β (x)if α is a limit ordinal.

β<αThere is no confusion, because these two definitions of f α (x) coincide if x is
both a prefixed point and a postfixed point of f .
4

a

b

c

d

e

f

Figure 2.1: A small example of a labelled transition system, where Σ = {∗}Theorem 2.1.7 (Cousot-Cousot fixed point theorem). Let (C, ⊑) be a complete
lattice, f : C → C be a monotone function, and κ be a cardinal number that isgreater than that of any chain in (C, ⊑).
Then we have µf ≡ f κ (⊥).
Dually, νf ≡ f κ (⊤).

2.2

Examples of Coinduction and Induction

Now we give examples of coinductive and inductive properties.
Behaviors of programs or processes are usually interpreted in terms of labelledtransition systems. See e.g. [15, 16] for details.
Definition 2.2.1 (Labelled transition systems and their modal operators). Alabelled transition system (LTS) is a set Q equipped with an indexed family of
relations {(→a ) ⊆ Q × Q}a∈Σ , where Σ is a fixed set called an alphabet.
A labelled transition system can be seen as a Kripke frame for the multimodal
variant of the modal logic K. For each a ∈ Σ, two modalities [a], ⟨a⟩ : P(Q) →P(Q) are defined as follows:[a]Y := { x ∈ Q | ∀y ∈ X. (x →a y) ⇒ y ∈ Y } ,⟨a⟩Y := { x ∈ Q | ∃y ∈ X, (x →a y) ∧ y ∈ Y } .
Both [a] and ⟨a⟩ are monotone.
We will use the small example shown in Figure 2.1 to explain how to use
parameterized coinduction.
Before we give translation rule from programs or processes to labelled transition systems, we present some properties of labelled transition systems that canbe expressed in the modal µ-calculus.
Example 2.2.2 (States that have an infinitely long path). Let (Q, →) be alabelled transition system over the alphabet Σ = {∗}. The set of states that havean infinitely long path starting from them can be expressed as:
infPath := ν⟨∗⟩.
Example 2.2.3 (States that have a path to an accepting state). Let (Q, →) bea labelled transition system over the alphabet Σ = {∗} and F ⊆ Q. The set ofstates that have a path from them to an accepting state can be expressed as:
acc := µZ. F ∪ ⟨∗⟩Z.

5

t →a ✓
t + t′ → a ✓a →a ✓
t →a t′′t + t′ →a t′′
t →a t′′t · t′ →a t′′ · t′t′ →a ✓
t + t′ → a ✓t →a ✓t · t′ → a t′t′ →a t′′t + t′ →a t′′

Table 2.1: Interpretation of basic process terms
Example 2.2.4 (States that have an infinitely long path visiting accepting states
infinitely often). Let (Q, →) be a labelled transition system over the alphabet
Σ = {∗} and F ⊆ Q. The set of states that have an infinitely long path startingfrom it visiting accepting states infinitely often can be expressed as:
infAcc := νZ. µW. (F ∩ ⟨∗⟩Z) ∪ ⟨∗⟩W.
Now we give an example of a process algebra from [7] and its interpretation
as a labelled transition system.
Definition 2.2.5 (Basic process algebra). Basic process terms are terms generated from the grammar:
t ::= a | t + t′ | t · t′
where a is an element of Σ, the fixed alphabet.
Algebra of basic process terms is called basic process algebra.
Definition 2.2.6 (Interpretations of basic process terms). Let Q be the disjoint
union of the set of closed basic process terms and {✓}. Interpretations of basic process terms is a labelled transition system (Q, {(→a )}a∈Σ ), where (→a ) is
inductively defined by the rules in Table 2.1.
Bisimilarity is used to define equivalence between two processes and it isstronger than trace-equivalence. Bisimilarity is also a coinductively defined relation.
Definition 2.2.7 (Bisimulation and bisimilarity). Fix a labelled transition system (Q, {(→a )}a∈Σ ). Define one-step simulation equation sim : P(Q × Q) →P(Q × Q) bysim(R) := {(q, q ′ ) | (∀a. ∀r. q →a r ⇒ ∃r′ . q ′ →a r′ ∧ (r, r′ ) ∈ R)∧(∀a. ∀r′ . q ′ →a r′ ⇒ ∃r. q →a r ∧ (r, r′ ) ∈ R)}.
A bisimulation is a postfixed point of sim. Two states q, q ′ ∈ Q are bisimilar
if (q, q ′ ) ∈ νsim.

2.3

Parameterized Coinduction: A Review

One way to prove a coinductive property is to use the Knaster-Tarski Theorem,i.e.
r ⊑ f (r) ⇒ r ⊑ νf.
For example, to prove a ∈ infPath in Figure 2.1, we give a proof like this:6a ∈ infPath⇐ {a, b, d} ⊆ ν⟨∗⟩(Discover an invariant)⇐ {a, b, d} ⊆ ⟨∗⟩({a, b, d})(Use the Knaster-Tarski)⇔ {a, b, d} ⊆ {a, b, d}(Expand the modality)

There is a problem, however: we have to give an invariant at an early stage ofthe proof. If we apply the Knaster-Tarski to the first goal, we will be confronted
by the unprovable goal {a} ⊆ ⟨∗⟩{a} = ∅.
To overcome this problem, Hur et al. [9] propose a proof technique, calledparameterized coinduction.
Parameterized greatest fixed points play a central role in parameterized coinduction.
Definition 2.3.1 (Parameterized greatest fixed points). Let (C, ⊑) be a complete lattice and f : C → C be a monotone function. For x ∈ C, we define theparameterized greatest fixed point Gf (x) by
Gf (x) := νy. f (x ⊔ y).
These elements Gf (x) are monotone in f and x.
As the name suggests, the notion of parameterized greatest fixed point is a
generalization of the ordinary notion of greatest fixed point.
Lemma 2.3.2 (Initialization of greatest fixed points). Let (C, ⊑) be a complete
lattice and f : C → C be a monotone function. Then we have νf ≡ Gf (⊥).
Proof. This is because we have f ≡ λy. f (⊥ ⊔ y).
When working with Gf (x) we use two important lemmas: the unfolding
lemma and the accumulation lemma.
Lemma 2.3.3 (The unfolding property of parameterized greatest fixed points).
Let (C, ⊑) be a complete lattice and( f : C →) C be a monotone function. Thenfor all x ∈ C, we have Gf (x) ≡ f x ⊔ Gf (x) .
Proof. This is exactly the fact that Gf (x) is a fixed point of λy. f (x ⊔ y).
Lemma 2.3.4 (The accumulation property of parameterized greatest fixed points).
Let (C, ⊑) be a complete lattice and f : C → C be a monotone function. Thenfor all x, y ∈ C, we have y ⊑ Gf (x) if and only if y ⊑ Gf (x ⊔ y).
Proof. The only-if direction is obvious. To prove the converse, we assume y ⊑Gf (x ⊔ y). Then Gf (x ⊔ y) is a postfixed point of λz. f (x ⊔ z), because()
Gf (x ⊔ y) ≡ f x ⊔ y ⊔ Gf (x ⊔ y)()
⊑ f x ⊔ Gf (x ⊔ y) .
Therefore, we have y ⊑ Gf (x ⊔ y) ⊑ Gf (x).

7Example 2.3.5 (Example Proof with Generalized Fixed Points). As a comparison to the Knaster-Tarski proof, we show below a proof of a ∈ infPath in
Figure 2.1 using Gf (x).
a ∈ infPath⇔ {a} ⊆ G⟨∗⟩ (∅)()⇔ {a} ⊆ ⟨∗⟩ ∅ ∪ G⟨∗⟩ (∅)(Initialization)(Unfolding)⇐ {b} ⊆ G⟨∗⟩ (∅)(Move to a next state)⇔ {b} ⊆ G⟨∗⟩ ({b})()⇔ {b} ⊆ ⟨∗⟩ {b} ∪ G⟨∗⟩ ({b})(Accumulation)(Unfolding)⇐ {d} ⊆ {b} ∪ G⟨∗⟩ ({b})(Move to a next state)⇐ {d} ⊆ G⟨∗⟩ ({b})()⇔ {d} ⊆ ⟨∗⟩ {b} ∪ G⟨∗⟩ ({b})(Unfolding)⇐ {b} ⊆ {b} ∪ G⟨∗⟩ ({b})(Move to a next state)⇐ {b} ⊆ {b}Although it is longer than the last proof, it has an advantage that it does notneed discovery of an invariant. Provers only have to specify Unfolding, Accumulation, or a next state to transition to.
We get another benefit from parameterized coinduction: compositionality.
Lemma 2.3.6 (Compositionality). Let (C, ⊑) be a complete lattice and f : C →C be a monotone function. For r, g1 , g2 ∈ C, if g1 ⊑ Gf (r⊔g2 ) and g2 ⊑ Gf (r⊔g1 )hold, then g1 ⊔ g2 ⊑ Gf (r).
Proof. From the assumptions we get g1 ⊔ g2 ⊑ Gf (r ⊔ g1 ⊔ g2 ). By Lemma 2.3.4,
g1 ⊔ g2 ⊑ Gf (r).

8Chapter 3
Parameterized Induction
3.1

Motivating Example: Reachability Problem in Pushdown
Systems

Problems of proving coinductive properties x ⊑ νf and inductive propertiesx ⊑ µf are similar in that for both kinds of problems, we have to give an invariant, although we also have to give a ranking function for inductive properties.
Therefore, it may be convenient to introduce an inductive counterpart of parameterized coinduction.
For example, let us consider a (usually finite-state) system with parametersin each state: pushdown systems [3].
Definition 3.1.1 (Labelled pushdown systems). A labelled pushdown system isa tuple (Σ, P, Γ, ∆), where Σ is( an input alphabet,
P is a set of control locations,)
Γ is a stack alphabet, and ∆ ⊆ P × (Γ ∪ {ϵ}) × Σ × (P × Γ∗ ) is a set of transition
rules. Usually finiteness is also imposed on Σ, P , Γ, and ∆.
For p ∈ P and w ∈ Γ∗ , a pair (p, w) is called a configuration of the pushdown
system. The set of configurations( can be regarded) as a labelled transition system,
where(q, γw′ ) )→a (q ′ , ww′ ) if (q, γ), a, (q ′ , w) ∈ ∆ and (q, ϵ) →a (q ′ , w) if((q, ϵ), a, (q ′ , w) ∈ ∆.
Example 3.1.2 (Reachability problems for pushdown systems). Let ({∗}, P, Γ, ∆)be a pushdown system, c ∈ P × Γ∗ be an initial configuration, and F ⊆ P × Γ∗
be a set of accepting configurations.
The reachability problem is a problem to decide whether there is a path fromc to an element of F or not.
Since reachability can be expressed as {c} ⊆ µZ. F ∪ ⟨∗⟩Z, it is an inductive
property.

3.2

Parameterized Least Fixed Points

Here we define parameterized least fixed points.
Definition 3.2.1 (Parameterized least fixed points). Let (C, ⊑) be a complete
lattice and f : C → C be a monotone function. For x ∈ C, we define the parameterized least fixed point Lf (x) by
Lf (x) := µy. f (x ⊔ y).
These elements Lf (x) are monotone in f and x.
Note that, although it is a “dual” notion of Gf (x), it is not a genuine dual interms of dual order; the order-theoretical dual of Gf (x) is µy. f (x ⊓ y).
Some lemmas of Gf (x) are true for Lf (x) with no changes.
9Lemma 3.2.2 (Initialization of least fixed points). Let (C, ⊑) be a complete
lattice and f : C → C be a monotone function. Then we have µf ≡ Lf (⊥).
Proof. This is because we have f ≡ λy. f (⊥ ⊔ y).
Lemma 3.2.3 (The unfolding property of parameterized least fixed points). Let(C, ⊑) be a complete lattice( and f : C )→ C be a monotone function. Then for allx ∈ C, we have Lf (x) ≡ f x ⊔ Lf (x) .
Proof. This is exactly the fact that Gf (x) is a fixed point of λy. f (x ⊔ y).

3.3

The Indexed Accumulation Property

As stated later, Lemma 2.3.4 and Lemma 2.3.6 are strong enough to characterize
greatest fixed points. Therefore, least fixed points does not have such properties
with no change.
However, similar reasoning can be done, if we give a ranking function.
Lemma 3.3.1 (The indexed accumulation property of parameterized least fixed
points). Let (C, ⊑) be a complete lattice and f : C → C be a monotone function.
Let α′ be an ordinal number and x, y : α′ → C be indexed families of elements of
C. Also assume x is increasing. Then we have())(∀α ∈ α′ . y(α) ⊑ Lf x(α)
⊔y(β) .
⇐⇒ ∀α ∈ α′ . y(α) ⊑ Lf x(α) ⊔β<αProof. Again,
direction
is obvious. To prove the converse, we assume( the only-if)⊔y(α) ⊑ Lf x(α) ⊔ β<α y(β) for all α ∈ α′ .
()
We will prove y(α) ⊑ Lf x(α) by induction on α. By the inductive hypothesis and the monotonicity of x, we have⊔()y(β) ⊑ Lf x(α) .
β<α

(
)
(
(
))
⊔
We get Lf x(α) ⊔ β<α y(β) ⊑ Lf x(α) ⊔ Lf x(α) from this. Therefore, it
(
(
)
(
))
(
)
suﬃces to show Lf x(α)⊔Lf x(α) ⊑ Lf x(α) . This is true because Lf x(α))(()
is a prefixed point of λz. f x(α) ⊔ Lf x(α) ⊔ z .
Lemma 3.3.2 (The indexed composition property of parameterized least fixed
points). Let (C, ⊑) be a complete lattice and f : C → C be a monotone function.
Let α′ be an ordinal number and r, g1 , g2 : α′ → C be indexed families of elementsof C. Assume r is monotone.
(
)
(
)
⊔
Assume g1 (α) ⊑ Lf r(α) ⊔ β<α g2 (β) and g2 (α) ⊑ Lf r(α) ⊔ g1 (α) for all()α ∈ α′ . Then we have g1 (α) ⊔ g2 (α) ⊑ Lf r(α) for all α ∈ α′ .
Proof. Define r′ , g : 2α′ → C asg(2α) := g1 (α)
g(2α + 1) := g2 (α)
r′ (2α) := r(α)
r′ (2α + 1) := r(α).
10q0 ϵ → ϵ q2
⋆→ϵ

⋆→⋆
q1

Figure 3.1: A small example of a labelled pushdown system()⊔
Then r′ is monotone. From the assumptions, g(γ) ⊑ Lf r′ (γ)⊔ δ<γ g(δ) for()
all γ ∈ 2α. By Lemma 3.3.1, g(γ) ⊑( Lf r)′ (γ) for all γ ∈ 2α.
γ = 2α( Assigning)and γ = 2α + 1 leads to g1 (α) ⊑ Lf r(α) and g2 (α) ⊑ Lf r(α) .

3.4

Example Proof with Parameterized Least Fixed Points

Example 3.4.1 (An example of a pushdown system).
Let us consider() ( a push)downsystem
({∗},
{q
,
q
,
q
},
{⋆},
∆),
where
∆
=
{
(q
,
⋆),
∗,
(q
,
⋆)
, (q1 , ⋆), ∗, (q0 , ϵ) ,
0
1
2
0
1
(
)
(q0 , ϵ), ∗, (q2 , ϵ) } (Figure 3.1).
Let the set of accepting states F = { (q2 , w) | w ∈ {⋆}∗ }. Then for all w ∈∗{⋆} , from (q0 , w) one of accepting states can be reachable.
Proof.
∀n ≥ 0. {(q0 , ⋆n )} ⊆ µZ.F ∪ ⟨∗⟩Z
⇔ ∀n ≥ 0. {(q0 , ⋆n )} ⊆ LλZ.F ∪⟨∗⟩Z (∅)(Initialization)⇔ ∀n ≥ 0. {(q0 , ⋆ )} ⊆ LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆ ) | m < n }) (Indexed Accumulation)(⇔ ∀n ≥ 0. {(q0 , ⋆n )} ⊆ F ∪ ⟨∗⟩ { (q0 , ⋆m ) | m < n } ∪)LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n })(Unfolding)(nm⇐ ∀n ≥ 0. {(q0 , ⋆ )} ⊆ ⟨∗⟩ { (q0 , ⋆ ) | m < n } ∪)LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n })nmHere we do a case analysis:• For n = 0,(){(q0 , ϵ)} ⊆ ⟨∗⟩ LλZ.F ∪⟨∗⟩Z (∅)⇐ {(q2 , ϵ)} ⊆ LλZ.F ∪⟨∗⟩Z (∅)()⇔ {(q2 , ϵ)} ⊆ F ∪ ⟨∗⟩ LλZ.F ∪⟨∗⟩Z (∅)⇐ {(q2 , ϵ)} ⊆ F

11(Step)(Unfolding)• For n > 0,(∀n > 0. {(q0 , ⋆n )} ⊆ ⟨∗⟩ { (q0 , ⋆m ) | m < n } ∪)LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n })(⇔ ∀n ≥ 0. {(q0 , ⋆n+1 )} ⊆ ⟨∗⟩ { (q0 , ⋆m ) | m < n + 1 } ∪)LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })⇐ ∀n ≥ 0. {(q1 , ⋆n+1 )} ⊆ { (q0 , ⋆m ) | m < n + 1 } ∪LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })⇐ ∀n ≥ 0. {(q1 , ⋆n+1(Step))} ⊆LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })Then,∀n ≥ 0. {(q1 , ⋆n+1 )} ⊆LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })⇔ ∀n ≥ 0. {(q1 , ⋆n+1 )} ⊆ F ∪(⟨∗⟩ { (q0 , ⋆m ) | m < n + 1 } ∪)LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })(⇐ ∀n ≥ 0. {(q1 , ⋆n+1 )} ⊆ ⟨∗⟩ { (q0 , ⋆m ) | m < n + 1 } ∪)LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })(Unfolding)⇐ ∀n ≥ 0. {(q0 , ⋆n )} ⊆ { (q0 , ⋆m ) | m < n + 1 } ∪LλZ.F ∪⟨∗⟩Z ({ (q0 , ⋆m ) | m < n + 1 })⇐ ∀n ≥ 0. {(q0 , ⋆ )} ⊆ { (q0 , ⋆ ) | m < n + 1 }
n

m

12

(Step)

Chapter 4
Functional Characterization of
Parameterized (Co)Induction
4.1

Test Functions Generalizing Parameterized (Co)Induction

We are interested in how “convenient” Gf (x) and Lf (x) are. To investigate this,
we introduce test functions F that share some properties with Gf (x) and Lf (x).
Definition 4.1.1 (Test functions for the parameterized fixed points). Let (C, ⊑)be a complete lattice and f : C → C be a monotone function. A test function for
f is a monotone function F : C → C.
(A) test function F for f has the unfolding property, if for all x ∈ C, f x ⊔F (x) ⊑ F (x) holds.
A test function F for f has the accumulation property, if for all x, y ∈ C,y ⊑ F (x ⊔ y) implies y ⊑ F (x).
A test function F for f has the composition property, if for all r, g1 , g2 ∈ C,
if g1 ⊑ F (r ⊔ g2 ) and g2 ⊑ F (r ⊔ g1 ), then g1 ⊔ g2 ⊑ F (r).
A test function F for f has the indexed accumulation property, if for all
ordinal numbers α′ and for all x, y : α′ → C where x is monotone, the following
two conditions are equivalent:()• For all α ∈ α′ , we have y(α) ⊑ F x(α) .
)(⊔• For all α ∈ α′ , we have y(α) ⊑ F x(α) ⊔ β<α y(β) .
A test function F for f has the indexed composition property, if the following
condition is satisfied:• Let α′ be an ordinal number and r, g1 , g2 : α′ → C be indexed families of′
elements
of(⊔ C, where)r is monotone. (Assume that )for all α ∈ α , g1 (α) ⊑F r(α) ⊔ β<α g2 (β) and g2 (α) ⊑ F r(α) ⊔ g1 (α) . Then for all α ∈ α′ ,()
we have g1 (α) ⊔ g2 (α) ⊑ F r(α) .

4.2Interderivability of Accumulation and Composition

The theorem below shows that the accumulation property and the composition
property are interderivable.
Theorem 4.2.1 (Accumulation is equivalent to composition). Let (C, ⊑) be acomplete lattice and f : C → C be a monotone function. For all test functions
F for f , F has the accumulation property if and only if it has the composition
property.

13

Proof. To prove the accumulation property from the composition property, justlet r = x and g1 = g2 = y.
To prove the converse, assume g1 ⊑ F (r ⊔ g2 ) and g2 ⊑ F (r ⊔ g1 ). Since
g1 ⊔ g2 ⊑ F (r ⊔ g1 ⊔ g2 ), we have g1 ⊔ g2 ⊑ F (r).
Therefore we identify the accumulation property and the composition property in this chapter.
In contrast, neither indexed accumulation nor indexed composition is notessential.
Theorem 4.2.2 (Unfolding implies indexed accumulation and indexed composition). Let (C, ⊑) be a complete lattice and f : C → C be a monotone function.
For all test functions F for f with the unfolding property, F has the indexed
accumulation and indexed composition properties.
Proof. Essentially the same as Lemma 3.3.1 and Lemma 3.3.2.

4.3

Characterization of Parameterized Coinduction

In this setting, Gf (x) is characterized by the unfolding property and the accumulation property.
Lemma 4.3.1 (Characterization of parameterized greatest fixed point). Let(C, ⊑) be a complete lattice and f : C → C be a monotone function. Assume
that a test function F for f has the unfolding property and the accumulation
property. Then we have Gf ⊑ F .
()
Proof. To prove Gf (x) ⊑ F (x), It(suﬃces to show Gf (x) ⊑ F) x ⊔ Gf (x) . This()()
is equivalent to f x ⊔ Gf (x) ⊑ f x ⊔ Gf (x) ⊔ F x ⊔ Gf (x) .
Note that a similar theorem to the above lemma appears in [9]. Since weemploy a looser condition for the unfolding property, the result of our lemma isa bit weaker.
Using the lemma above, we can derive the following equivalence theorem.
Theorem 4.3.2 (Characterization of the unfolding property and the accumulation property). Let (C, ⊑) be a complete lattice and f : C → C be a monotonefunction. For all x, y ∈ C, the following are equivalent:
1. For all test functions F for f with the unfolding property and the accumulation property, we have y ⊑ F (x).
2. y ⊑ Gf (x).
Proof. 1. implies 2. because we can use Gf as F .
2. implies 1. because we have Gf ⊑ F .

4.4

Characterization of Parameterized Induction

There is also the least fixed point variant of the theorem above.
Lemma 4.4.1 (Characterization of parameterized least fixed point). Let (C, ⊑)be a complete lattice and f : C → C be a monotone function. Assume that a test
function F for f has the unfolding property. Then we have Lf ⊑ F .

14

Proof. Since F is a prefixed point of λw. f (x ⊔ w) and Lf is the least prefixed
point of λw. f (x ⊔ w), we have Lf (x) ⊑ F (x).
Theorem 4.4.2 (Characterization of the unfolding property). Let (C, ⊑) be acomplete lattice and f : C → C be a monotone function. For all x, y ∈ C, thefollowing are equivalent:
1. For all test functions F for f with the unfolding property, we have y ⊑ F (x).
2. We have y ⊑ Lf (x).
Proof. This is because Lf (x) is the least prefixed point of λz. f (x ⊔ z).

15

Chapter 5
Predicate Characterization and No-discovery
Parameterized (Co)Induction
5.1

Motivating Example: Infinite State System

In Chapter 4, we showed that Lemma 2.3.3 and Lemma 2.3.4 are enough tocharacterize Gf . However, still there is a possibility that one have to discover aninvariant.
Our motivating example is the labelled transition system below:
Example 5.1.1. We consider the labelled transition system in Figure 5.1.
Below is an unsuccessful attempt to prove q0 ∈ infPath.
{q0 } ⊆ infPath⇔ {q0 } ⊆ G⟨∗⟩ ({q0 })()⇔ {q0 } ⊆ ⟨∗⟩ {q0 } ∪ G⟨∗⟩ ({q0 })(Accumulation)(Unfolding)⇐ {q1 } ⊆ {q0 } ∪ G⟨∗⟩ ({q0 })(Step)⇐ {q1 } ⊆ G⟨∗⟩ ({q0 })⇔ {q1 } ⊆ G⟨∗⟩ ({q0 , q1 })()⇔ {q1 } ⊆ ⟨∗⟩ {q0 , q1 } ∪ G⟨∗⟩ ({q0 , q1 })(Accumulation)(Unfolding)⇐ {q2 } ⊆ {q0 , q1 } ∪ G⟨∗⟩ ({q0 , q1 })(Step)⇐ {q2 } ⊆ G⟨∗⟩ ({q0 , q1 })..
.
In the attempt, we acquire accumulated knowledge about states that we havegone through. However, we have no opportunity to use it.
By discovering an invariant, though, q0 ∈ infPath can be proven.
q0

q1

q2

q3

q4

···

Figure 5.1: A small example of an infinite state labelled transition system16

{q0 } ⊆ infPath⇐ { qi | i ≥ 0 } ⊆ infPath⇐ { qi | i ≥ 0 } ⊆ ⟨∗⟩ { qi | i ≥ 0 }(Tarski)⇐ { qi | i ≥ 1 } ⊆ { qi | i ≥ 0 }(Step)

Although there is an intuition that we have to discover an invariant in theexample above, Theorem 5.5 does not capture that intuition.

5.2

Test Predicates Generalizing Test Functions

To model the problem mathematically, we should define what “can be provenwithout discovering an invariant.” There arise two problems:• If the goal is of the form y ⊑ F (x), we can always use the strategy of
discovering an invariant: it suﬃces to show y ⊑ Gf (x) and Gf (x) ⊑ F (x).
We have to give appropriate generalization of y ⊑ F (x).
• What can be done to the goal of the form y ⊑ g(x) depends on the lattice
C and the function g : C → C that we are working on. We have to defineit.
We would like to resolve the first problem by generalizing test functions totest predicates.
Definition 5.2.1 (Test predicates for parameterized fixed points). Let (C, ⊑) be
a complete lattice and f : C → C be a monotone function. A test predicate forthe parameterized fixed points of f is a predicate P ⊆ C × C.
A test predicate P has the downward closure property, if for all x, y, y ′ ∈ C,y ⊑ y ′ and P (x, y ′ ) implies P (x, y).
(A test) predicate P hasthejoin
closureproperty,
if
for
all
Y
⊆
C,
∀y ∈
⊔
Y. P (x, y) implies P (x, Y ).
Test predicates are actually generalization of test functions, as shown in thetheorem below:
Theorem 5.2.2 (Test predicates generalize test functions). Let (C, ⊑) be a complete lattice and P ⊆ C × C be a test predicate. The following are equivalent:
1. We have the downward closure property and the join closure property forP.
2. There exists a test function F : C → C such that for all x, y ∈ C, y ⊑F (x) ⇐⇒ P (x, y).
Furthermore, such F : C → C are unique up to equivalence.
Proof. Obviously 2. implies 1.
()⊔
To prove 2. from 1., let F (x) := { y | P (x, y) }. By join closure, P x, F (x) .
By downward closure, P (x, y).
Assume that both F and F ′ satisfies the property in 2. Then from F ′ (x) ⊑F ′ (x) we have F (x) ⊑ F ′ (x), and F ′ (x) ⊑ F (x) alike.
17

5.3

Generalization of the Unfolding Property and the Accumulation Property

For the second problem, we want to use a left adjoint: a monotone function hsuch that y ⊑ g(x) ⇐⇒ h(y) ⊑ x. However, the left adjoint need not exist in
general. Instead, we define a looser condition:
Definition 5.3.1 (Minimal witnesses). Let (C, ⊑) be a complete lattice. For amonotone function g : C → C and y, z ∈ C, z is a minimal witness from y to g if
and only if it is a minimal element of { z ′ ∈ C | y ⊑ g(z ′ ) }.
Note that, if we replace “minimal” with “minimum,” we get a universal arrow
and a left adjoint.
Minimal witnesses have enough power to prove propositions of the form y ⊑g(x).
Lemma 5.3.2 (Characterization of adjoint-like reasoning). Let (C, ⊑) be a complete lattice and g : C → C be a monotone function preserving directed infima.
Then for all x, y ∈ C, the following are equivalent:
1. There exists z ∈ C such that z ⊑ x and z is a minimal witness from y to g.
2. y ⊑ g(x).
Proof. To prove 2. from 1., just use the fact that z is a minimal witness.
To prove 1. from 2., let A := { z ′ ∈ C | z ′ ⊑ x ∧ y ⊑ g(z ′ ) } and apply Zorn’s
lemma to A ⊆ C (in a reverse order).
• A is nonempty because x ∈ A.
• Let B ⊆ A be a nonempty chain of A. Thenbound of B.

d

B ∈ A and this is a lower

Using minimal witnesses, we can generalize the unfolding condition.
Definition 5.3.3 (The unfolding property of test predicates). Let (C, ⊑) be acomplete lattice and f : C → C be a monotone function. A test predicate P has
the unfolding property, if for all minimal witnesses z ∈ C from y to λw. f (x ⊔ w),
P (x, z) implies P (x, y).
Theorem 5.3.4 (The unfolding property of test predicates generalizes that oftest functions). Let (C, ⊑) be a complete lattice and f : C → C be a monotonefunction. Assume for all w ∈ C, λw. f (x ⊔ w) preserves directed infima. Let
P ⊆ C × C be a test predicate of f . Then the following are equivalent:
1. We have the downward closure property, the join closure property, and theunfolding property for P .
2. There exists a test function F : C → C such that F satisfies the unfolding
property and for all x, y ∈ C, y ⊑ F (x) ⇐⇒ P (x, y).
Proof. 1. is immediate from 2. and Lemma 5.3.2.
⊔( To prove) 2. from( 1., as )in Theorem 5.2.2, let F (x) := { y | P (x, y) }. Sincef x ⊔ F (x) ⊑ f x ⊔ F((x) , there) exists z ∈ C such that z ⊑ F (x) and z is aminimal witnessf x ⊔ F)(x) to λw. f (x ⊔ w). By the unfolding property of( from
()()
P , we have P x, f x ⊔ F (x) i.e. f x ⊔ F (x) ⊑ F (x).

18The accumulation property can also be generalized to test predicates.
Definition 5.3.5 (The accumulation property of test predicates). Let (C, ⊑) be
a complete lattice and f : C → C be a monotone function. A test predicate P
has the accumulation property, if for all x, y ∈ C, P (x ⊔ y, y) implies P (x, y).
Theorem 5.3.6 (The accumulation property of test predicates generalizes thatof test functions). Let (C, ⊑) be a complete lattice and f : C → C be a monotonefunction. Assume for all w ∈ C, λw. f (x ⊔ w) preserves directed infima. Let
P ⊆ C × C be a test predicate of f . Then the following are equivalent:
1. We have the downward closure property, the join closure property, and theaccumulation property for P .
2. There exists a test function F : C → C such that F satisfies the accumulation property and for all x, y ∈ C, y ⊑ F (x) ⇐⇒ P (x, y).
Proof. 1. is immediate from 2.
⊔
To prove 2. from 1., as in Theorem 5.2.2, just let F (x) := { y | P (x, y) }.
Generalization means dropping the downward closure condition.

5.4

Characterization of No-discovery Parameterized Induction

Before characterizing no-discovery parameterized coinduction, we show that thesimilar result to Theorem 4.4.2 holds with a little restriction.
Theorem 5.4.1 (Characterization of unfolding, without discovery of an invariant). Let (C, ⊑) be a complete lattice and f : C → C be a monotone function.
Assume λw. f (x ⊔ w) preserves directed infima and for all z ∈ C, λw. z ⊓ wpreserves directed suprema. For all x, y ∈ C, the following are equivalent:
1. For all test predicates P of f , if f satisfies the join closure property and theunfolding property, then P (x, y) holds.
2. y ⊑ Lf (x).
Proof. We define g(w) := f (x ⊔ w).
1. implies 2. because we can use y ⊑ Lf (x) as P (x, y).
To prove 2. from 1., we use Theorem 2.1.7. By the theorem, y ⊑ g α (⊥) forsome α. Do induction on α.
If α = 0, then y ≡ ⊥ by the hypothesis. The join closure property can beapplied to prove P (x, ⊥).
( ′)If α = α′ + 1, then y ⊑ g g α (⊥) . By Lemma 5.3.2, there exists z ∈ C′such that z is a minimal witness from y to g and z ⊑ g α (⊥). By the inductive
hypothesis, P (x, z). By unfolding, ⊔P (x, y).
If α is a limit ordinal, then y ⊑ β<α g β (⊥). By the inductive hypothesis, for
( ⊔
(
)
(
all β < α, P x, y ⊓ g β (⊥) . By the join closure property, we have P x, β<α y ⊓))g β (⊥) . This equivalent to P (x, y).

19

5.5

Characterization of No-discovery Parameterized Coinduction

Here we prove a similar theorem to for finite lattices.
Theorem 5.5.1 (Characterization of unfolding and accumulation, without discovery of an invariant). Let (C, ⊑) be a finite lattice and f : C → C be a monotonefunction. Assume λw. f (x ⊔ w) preserves directed infima. For all x, y ∈ C, thefollowing are equivalent:
1. For all test predicates P of f , if P satisfies the join closue property, theunfolding property, and the accumulation property, then P (x, y) holds.
2. y ⊑ Gf (x).
Proof. 2. is immediate from 1. We prove 1. from 2.
We construct a pair of sequences {xi }i≥0 , {yi }i≥0 satisfying following conditions:• x0 = x, y0 = y.
• xi+1 = xi ⊔ yi
• yi+1 is a minimal witness from yi to λw. f (xi+1 ⊔ w).
()
Assume x′ , y ′ ∈ C and y ′ ⊑ Gf (x′ ). Since y ′ ⊑ f x′ ⊔ y ′ ⊔ Gf (x′ ⊔ y ′ ) , there
exists y ′′ ∈ C such that y ′′ ⊑ Gf (x′ ⊔ y ′ ) and y ′′ is a minimal witness from y ′to λw. f (x′ ⊔ y ′ ⊔ w). Therefore, by dependent choice, there is such a pair ofsequences.
For all i ≥ 0, P (xi+1 , yi+1 ) implies P (x, y). We prove this by induction on i.
Assume that P (xi+1 , yi+1 ). Since yi+1 is a minimal witness, we have P (xi ⊔yi , yi ).
Therefore we have P (xi , yi ) by the accumulation property.
Since {xi }i≥0 is monotone and C is finite, there exists i > 0 such that xi ≡xi+1 . This means yi ⊑ xi . Therefore, by the fact that yi is a minimal witness,yi ⊑ f (xi ).
Since ⊥ is also a minimal witness from yi to λw. f (xi ⊔ yi ⊔ w), P (xi−1 , yi−1 )is true. Therefore we have P (x, y).

5.6

Examples and Counterexamples

In Lemma 5.3.2, we assumed f preserves directed infima. An example is ⟨a⟩.
Theorem 5.6.1. Let (Q, {→a }a∈Σ ) be a labelled transition system and a ∈ Σ.
Assume Q has finite branches labelled a i.e. for all q ∈ Q, a set { q ′ | q →a q ′ } is
finite.
Then ⟨a⟩ preserves directed infima.
Proof.
∩ Let S ⊆∩P(Q) be a downward directed set. It is straightforward to show⟨a⟩ A∈S A ⊆ A∈S ⟨a⟩A. We prove the∩ converse.
Let q ∈ Q and assume q ̸∈ ⟨a⟩ A∈S A, i.e. for all q →a q ′ , there exists
Aq′ ∈ S such that q ′ ̸∈ Aq′ . Since { q ′ | q →a q ′ } is finite and S is downward
directed,
there exists A ∈ S such that for all q →a q ′ , q ′ ̸∈ A. Therefore we have∩q ̸∈ A∈S ⟨a⟩S.
The theorem below shows that minimal witnesses correctly capture the proof
strategy in Example 2.3.5 and Example 5.1.1.
20

Theorem 5.6.2. Let (Q, {→a }a∈Σ ) be a labelled transition system and a ∈ Σ.
For all q ∈ Q and x, z ⊆ Q, z is a minimal witness from {q} to λw. ⟨a⟩(x ∪ w)
if and only if one of the following conditions are satisfied:• q ̸∈ ⟨a⟩w, z = {q ′ }, and q →a q ′ , or
• q ∈ ⟨a⟩w and z = ∅.

In addition, the theorem below shows that minimal witnesses correctly capture
the intuition that the proof strategy in Example 5.1.1 fails.
Example 5.6.3. We consider the labelled transition system in Figure 5.1.
We define a test predicate P for ⟨∗⟩. Let x, y ⊆ Q. Let x̄ := { i | qi ∈ x }∪{−1}and ȳ := { i | qi ∈ y } ∪ {−2}• If either x̄ or ȳ is unbounded, then (x, y) ∈ P .
• If both x̄ and ȳ are bounded and max x > max y, then (x, y) ∈ P .
• If both x̄ and ȳ are bounded and max x ≤ max y, then (x, y) ̸∈ P .
Lemma 5.6.4. Example 5.6.3 satisfies the join closure property, the unfolding
property, and the accumulation property.
Using this counterexample, we can conclude:
Theorem 5.6.5 (Failure of no-discovery parameterized coinduction). Unlike
Theorem 5.5.1, it is not the case that the following proposition is true.
• Let (C, ⊑) be a complete lattice and f : C → C be a monotone function. Assume λw. f (x ⊔ w) preserves directed infima. For all x, y ∈ C, the following
are equivalent:
1. For all test predicates P of f , if P satisfies the join closue property,
the unfolding property, and the accumulation property, then P (x, y)holds.
2. y ⊑ Gf (x).

21

Chapter 6
Conclusions and Future WorkWe gave the inductive counterpart of parameterized coinduction. This can beused in finite state systems with decreasing parameters. As there are parameterized induction and coinduction, generalization to mixed induction and coinduction is of interest.
Parametric corecursion [13] is similar to parameterized coinduction, but it isdefined in a category, not only in a preordered set. Therefore it can be used todefine coinductive sets rather than coinductive propositions. It may be convenient
to generalize parameterized induction to parametric recursion.
We gave the characterization of the power of parameterized coinduction andparameterized induction, and confirmed that parameterized coinduction is stronger
than usual coinductive proof in this respect. This result may be extended to infinite state systems with looser finiteness condition, like symbolic automata [5].
Syntactic approaches to characterization of such an advantage can also be
considered. One way is to provide a cut-eliminable calculus. Although there
is already a cut-eliminable calculus for the propositional modal µ-calculus [10],another approach is worth investigating.

22References[1] A. Arnold and D. Niwiński. Rudiments of µ-Calculus, volume 146 of Studies
in Logic and the Foundations of Mathematics. Elsevier, 2001.
[2] David Baelde and Dale Miller. Least and greatest fixed points in linear logic.
In Nachum Dershowitz and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 14th International Conference,
LPAR 2007, Yerevan, Armenia, October 15-19, 2007, Proceedings, volume4790 of Lecture Notes in Computer Science, pages 92–106. Springer, 2007.
[3] Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In Antoni W.
Mazurkiewicz and Józef Winkowski, editors, CONCUR ’97: Concurrency
Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings, volume 1243 of Lecture Notes in Computer Science, pages 135–150.
Springer, 1997.
[4] Patrick Cousot and Radhia Cousot. Constructive versions of Tarski’s fixed
point theorems. Pacific J. Math., 82(1):43–57, 1979.
[5] Loris D’Antoni and Margus Veanes. Minimization of symbolic automata.
In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages,
POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 541–554.
ACM, 2014.
[6] Federico Echenique. A short and constructive proof of tarski’s fixed-point
theorem. Int. J. Game Theory, 33(2):215–218, 2005.
[7] Wan Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2000.
[8] Ichiro Hasuo, Shunsuke Shimizu, and Corina Cı̂rstea. Lattice-theoretic
progress measures and coalgebraic model checking. In Rastislav Bodik and
Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, POPL 2016,
St. Petersburg, FL, USA, January 20 - 22, 2016, pages 718–732. ACM, 2016.
[9] Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The powerof parameterization in coinductive proof. In Roberto Giacobazzi and Radhia
Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL ’13, Rome, Italy - January 23- 25, 2013, pages 193–206. ACM, 2013.
[10] Gerhard Jäger, Mathis Kretz, and Thomas Studer. Canonical completenessof infinitary mu. J. Log. Algebr. Program., 76(2):270–292, 2008.

23

[11] Stephen C. Kleene. Introduction to metamathematics. Bibliotheca Mathematica. North-Holland, Groningen;Amsterdam;, 1952.
[12] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput.
Sci., 27:333–354, 1983.
[13] Lawrence S. Moss. Parametric corecursion. Theor. Comput. Sci., 260(12):139–163, 2001.
[14] Vaughan R. Pratt. A decidable mu-calculus: Preliminary report. In 22nd
Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981, pages 421–427. IEEE Computer Society,1981.
[15] Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge
University Press, 2012.
[16] Colin Stirling. Bisimulation and logic. In Davide Sangiorgi and Jan Rutten,
editors, Advanced Topics in Bisimulation and Coinduction, number 52 in
Cambridge Tracts in Theoretical Computer Science, chapter 4, pages 173–
196. Cambridge University Press, 2012.
[17] Colin Stirling and David Walker. Local model checking in the modal mucalculus. Theor. Comput. Sci., 89(1):161–177, 1991.
[18] Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications.
Pacific J. Math., 5:285–309, 1955.
[19] Thomas Wilke. Alternating tree automata, parity games, and modal µcalculus. Bull. Belg. Math. Soc. Simon Stevin, 8(2):359–391, 2001. Journées
Montoises d’Informatique Théorique (Marne-la-Vallée, 2000).
[20] Glynn Winskel. A note on model checking the modal nu-calculus. Theor.
Comput. Sci., 83(1):157–167, 1991.

24