Information Technology Reference
In-Depth Information
would not be used.
Suppose the circular coinduction algorithm would add the equation
z
=
zz
in
its unfrozen form to the hypothesis. After applying the derivatives we obtain the
goals
hd
(
z
)=
hd
(
zz
)
,
tl
(
z
)=
tl
(
zz
). At this point, the prover could use the freshly
added equation, and according to the congruence rule, both goals would be proven
directly, though we would still be in the process of showing that the hypothesis
holds. By following a similar reasoning, we could then also prove that 0
∞
=1
∞
!In
order to avoid these situations, the hypotheses are frozen (
i.e.
, their sort is changed
from
Stream
to
Frozen
) and this stops the application of the congruence rule, forc-
ing the application of the derivatives according to their definition in the specifica-
tion. Therefore, the use of the freezing operator is vital for the soundness of circular
coinduction.
Next, we focus on using
CIRC
for automatically reasoning on the equivalence
Let us analyze what happens if the freezing operator
−
of
-expressions. As we will show, the implementation of both the algebraic
specifications associated to polynomial functors and the equational entailment
relation described in Section 3, is immediate. Given a polynomial functor
G
G
,we
define a
CIRC
theory
B
G
=(
S,
(
Σ,Δ
)
,
(
E,
I
)) as follows:
-
(
S, Σ, E
)is
E
G
-
Δ
=
{
δ
G
G
(
∗
:
Exp
)
}
-
I
consists of the following equational interpolants:
{
σ
1
,σ
2
} ⇒ {
σ
1
=
σ
1
,σ
2
=
σ
2
}
σ
1
,σ
2
=
(8)
k
i
(
σ
)=
k
i
(
σ
)
σ
=
σ
}
{
}⇒{
(9)
{
f
=
g
}⇒{
f
(
a
)=
g
(
a
)
|
a
∈
A
}
(10)
The interpolants (8), (9) and (10) in
I
extend the entailment relation
from
the system above to
PF
(see Definition 6) as follows:
E
e
E
PF
{
e
i
|
i
∈
I
}
if
e
⇒{
e
i
|
i
∈
I
}
in
I
E
PF
e
E
PF
e
G
G
Theorem 3 (Soundness).
Let
be a polynomial functor, and
a binary rela-
)
∗
tion on the set of
G
-expressions. If
(
B
G
,
F
0
=
{}
,
G
0
=
G
⇒
(
B
G
,
F
n
,
G
n
=
{}
)
using
G⊆∼
G
.
Proof.
The idea of the proof is to identify a bisimulation relation
[Reduce]
,
[Derive]
and
[Simplify]
,then
F
G⊆F
.
On a closer look, based on the reduction rules implemented in
CIRC
,itisquite
easy to see that the initial set of goals
s.t.
G
is a
PF
-consequence of
B
G
∪ F
,
where
is the set of hypothesis (or derived goals) collected during a proof
session. In other words,
F
G⊆
cl
(
F
id
). So, if we anticipate a bit, we should show
F
that
=
cl
(
F
id
)isabisimulation,
i.e.
, according to Corollary 1,
B
G
∪ F
PF
δ
G
G
(
F
) . This is achieved by proving that
B
G
∪ F
PF
G
i
(
i
= 0
..n
)(note
⊆
i
=0
..n
G
i
, according to
[
Derive]). The demonstration is by
induction on
j
,where
n
that
δ
G
G
(
F
)
j
is the current proof step, and by case analysis on
the
CIRC
reduction rules applied at each step.
−
Remark 1.
The soundness of the proof system we describe in this paper does not
follow directly from Theorem 3 in [12]. This is due to the fact that we do not have
Search WWH ::
Custom Search