Information Technology Reference
In-Depth Information
[Derive]
:(
e
When the current goal
e
has the same sort with the special variable
B
,
F
,
G∪{
e
}
)
⇒
(
B
,
F∪{
e
}
,
G∪
Δ
[
e
] )
if
B∪F
∗
, and it is
not a
-consequence, it is added to the specification and its derivatives to the
set of goals. In order to simplify the notation, we write
δ
(
e
)for
δ
(
ε
)=
δ
(
ε
),
whenever
e
is of shape
ε
=
ε
.
[Simplify]
:(
B
,
F
,
G∪{
θ
(
e
)
}
)
⇒
(
B
,
F
,
G∪{
θ
(
e
i
)
|
i
∈
I
}
)
if
e
⇒{
e
i
|
i
∈
I
}
is a simplification rule from the specification
and
θ
:
X
→T
Σ
(
Y
) is a substitution.
[Fail]
:(
e
:
Bool
This rule stops the reduction process with failure whenever the current goal
e
is of type
Bool
and the corresponding normal forms are different.
B
,
F
,
G∪{
}
⇒
B∪F
∧
e
)
failure
if
e
It is worth noting that there is a strong connection between a
CIRC
proof
and the construction of a bisimulation relation. We emphasize this fact and the
importance of the freezing operator with a simple example.
Example 2.
Consider the case of infinite streams. The set
B
ω
of infinite streams
over a set
B
is the final coalgebra of the functor
=
B
×
Id
, with a coalgebra
structure given by
hd
and
tl
, the functions that return the head and the tail of
the stream, respectively. Our purpose is to prove that 0
∞
= (00)
∞
.Let
z
and
zz
represent the stream on the left hand side and, respectively, on the right hand
side. These streams are defined by the equations:
hd
(
z
)=0
,
tl
(
z
)=
z,
hd
(
zz
)=
0
,
tl
(
zz
)=0:
zz
. In Fig. 2 we present the correlation between the
CIRC
proof
and the construction of the bisimulation relation. Note how
CIRC
collects the
elements of the bisimulation as frozen hypothesis.
R
CIRC
proof
Bisimulation construction
z
zz
(
zz
)
(add goal z = zz .)
0
0
0
(
B, {}, { z
=
zz }
)
F
=
{}
;
z ∼ zz
?
hd
(
z
)
=
hd
(
zz
)
tl
(
z
)
=
tl
(
zz
)
0
−→ z
[Derive]
−→
z
B, { z
=
zz },
F
=
{
(
z, zz
)
}
;
0
−→
(
zz
)
zz
[Reduce]
−→
F
=
{
(
z, zz
)
}
;
z ∼
(
zz
)
?
(
B, { z
=
zz }, { z
= 0:
zz }
)
hd
(
z
)
=
hd
(0:
zz
)
tl
(
z
)
=
tl
(0:
zz
)
z
=
zz
z
=
0:
zz
z −→ z
(
zz
)
−→ zz
[Derive]
−→
F
=
{
(
z, zz
)
,
(
z,
(
zz
)
)
}
;
B,
,
z
=
zz
z
=
0:
zz
F
=
{
(
z, zz
)
,
(
z,
(
zz
)
)
}
[Reduce]
−→
B,
, {}
Fig. 2.
Parallel between a
CIRC
proof and the bisimulation construction
Search WWH ::
Custom Search