.
.
.
.
.
.
The
step parameter represents one step of the iteration. From a
current iteration state
a: A, it either returns a value of type
B,
meaning that iteration is over and that this
B value is the final
result of the iteration, or a value
a' : A which is the next state
of the iteration.
The naive way to define the iteration is:
Fixpoint iterate (a: A) : B :=
match step a with
| inl b => b
| inr a' => iterate a'
end.
However, this is a general recursion, not guaranteed to terminate,
and therefore not expressible in Coq. The standard way to work around
this difficulty is to use Noetherian recursion (Coq module
Wf).
This requires that we equip the type
A with a well-founded ordering
<
(no infinite ascending chains) and we demand that
step satisfies
step a = inr a' -> a < a'. For the types
A that are of interest to us
in this development, it is however very painful to define adequate
well-founded orderings, even though we know our iterations always
terminate.
Instead, we choose to bound the number of iterations by an arbitrary
constant.
iterate then becomes a function that can fail,
of type
A -> option B. The
None result denotes failure to reach
a result in the number of iterations prescribed, or, in other terms,
failure to find a solution to the dataflow problem. The compiler
passes that exploit dataflow analysis (the
Constprop,
CSE and
Allocation passes) will, in this case, either fail (
Allocation)
or turn off the optimization pass (
Constprop and
CSE).
Since we know (informally) that our computations terminate, we can
take a very large constant as the maximal number of iterations.
Failure will therefore never happen in practice, but of
course our proofs also cover the failure case and show that
nothing bad happens in this hypothetical case either.
The simple definition of bounded iteration is:
Fixpoint iterate (niter: nat) (a: A) {struct niter} : option B :=
match niter with
| O => None
| S niter' =>
match step a with
| inl b => b
| inr a' => iterate niter' a'
end
end.
This function is structural recursive over the parameter
niter
(number of iterations), represented here as a Peano integer (type
nat).
However, we want to use very large values of
niter. As Peano integers,
these values would be much too large to fit in memory. Therefore,
we must express iteration counts as a binary integer (type
positive).
However, Peano induction over type
positive is not structural recursion,
so we cannot define
iterate as a Coq fixpoint and must use
Noetherian recursion instead.
).
Proof.
.
.
Proof.
.
Proof.
.
.
).
Proof.
).
Proof.
).
Proof.
).
Proof.
.
Proof.
'.
Proof.
'.
Proof.
.
Proof.
).
Proof.
Invariance property.
.
.
Proof.
.
Proof.
.