Information Technology Reference
In-Depth Information
Gordon [13] and Dave Schmidt [10] used uppercase Roman letters, and other
authors (including myself) have used abbreviated English words.
3.2
Domains and Operations
The domain constructors used in the Oxford style include:
-
A
;
-
A
+
B
: sum domain containing elements injected from
A
and
B
;
-
A
×
B
: product domain containing tuples
a, b
B
: function domain with elements expressed by
λ
-abstractions
λa.b
.
Note that
A
→
→
B
→
C
groups as
A
→
(
B
→
C
), and
A
→
B
×
C
groups as
A
→
(
B
×
C
).
The above domains are equipped with some natural operations. Scott and Stra-
chey used the following:
-
pairing and projection for product domains
D
=
A
×
B
:
B
-
injection and projection for sum domains
D
=
A
+
B
:
|
A
:
D
P
:
A
→
B
→
D
,
M
0
:
D
→
A
,
M
1
:
D
→
→
A
,
|
B
:
D
→
B
,
in
D
:
A
→
D
,
in
D
:
B
→
D
-
least fixed points of functions on any domain
D
:
Y
:(
D
D
;and
-
identity function on any domain
D
:
I
:
D
→
D
)
→
→
D
.
They also introduced a couple of combinators simply as abbreviations:
-
composition
f
◦
g
=
λa.f
(
g
(
a
)):
f
◦
g
:
A
→
C
when
f
:
B
→
C
and
g
:
A
→
B
;
-
composition
f
∗
g
=
λa.
(
λb.f
(
M
0
b
)(
M
1
b
))(
g
(
a
)):
f
∗
g
:
A
→
C
when
f
:
B
0
→
B
1
→
C
and
g
:
A
→
B
0
×
B
1
.
Finally, they introduced some operations in connection with the given domain
T
of truth values and the (loosely specified) domain
S
of stores:
-
Cond
(
a
0
,a
1
) mapping
true
to
a
0
and
false
to
a
1
:
Cond
:
A
A
;
-
Contents
(
α
) mapping
σ
to the value stored in it at location
α
:
Contents
:
L → S → V
;
-
Assign
(
α, β
) mapping
σ
to
σ
such that the value stored at
α
in
σ
is
β
:
Assign
:
L
×
A
→
T
→
×
V
→
S
→
S
.
(The definition of the domain
V
of values returned by evaluating expressions
depends on the language being described [14]; for the examples give here, we
shall assume that it includes
L
and
T
as summands.) Later papers by other
authors introduced considerably more auxiliary notation, mainly to improve
the readability of the
λ
-expressions arising in the equations used to define
denotations.
Search WWH ::
Custom Search