Information Technology Reference
In-Depth Information
M
,
N
::
=
x
|
ʻx.M
|
MN
which says that
ʛ
is the least set satisfying the following three rules:
M
ʻx.M
MN
MN
x
A set of ground rules
R
determines an operator
R
:
X
ₒ
X
, which maps a set
S
to the set
R
(
S
)
S
ↆ
S
:(
S
,
x
)
={
x
|∃
∈
R
}
which includes all the elements derivable from those in
S
by using the rules in
R
.
A set
S
is
forward-closed
under
R
iff
R
(
S
)
ↆ
Definition 2.4
S
; a set
S
is
backward-
ↆ
R
(
S
).
In other words, if
S
is forward-closed, then
closed
under
R
iff
S
∃
S
ↆ
S
:(
S
,
x
)
∀
x
∈
X
:(
∈
R
)
⃒
x
∈
S
If
S
is backward-closed, then
S
ↆ
S
:(
S
,
x
)
∀
x
∈
X
:
x
∈
S
⃒
(
∃
∈
R
)
Given a set of rules
R
on
X
,welet
|
R
(
S
)
ↆ
R
(
S
)
S
f
=
{
S
ↆ
X
ↆ
S
}
and
S
b
=
{
S
ↆ
X
|
S
}
.
So
S
f
is the intersection of all forward-closed sets and
S
b
is the union of all backward-
closed sets. Note that
R
is monotone on the complete lattice (
). It follows
from Theorem
2.1
that
S
f
is in fact the least fixed point of
R
and
S
b
is the greatest
fixed point of
R
. Usually, an object is defined
inductively
(resp.
coinductively
)if
it is the
least
(resp.
greatest
) fixed point of a function. So the set
S
f
(resp.
S
b
)is
inductively (resp. coinductively) defined by the set of rules
R
.
P
(
X
),
ↆ
Example 2.6
The set of finite lists with elements from a set
A
is the set
List
induc-
tively defined by the following two rules, i.e. the least set closed forward under these
rules.
a
∈
Al
∈
List
(2.2)
nil
∈
List
a
·
l
∈
List
In contrast, the set of all finite or infinite lists is coinductively defined by the same
rules, i.e. the greatest set closed backward under the two rules above; the set of all
infinite lists is the set coinductively defined by the second rule above, i.e. the greatest
set closed backward under the second rule.
The two rules in (
2.2
) are not ground rules because they are not in the form shown
in (
2.1
). However, we can convert them into ground rules. Take
X
to be the set of all
Search WWH ::
Custom Search