Database Reference
In-Depth Information
•
ACOM is function which assigns 0 to
x
3
;
•
DEC decrements the value of the register
x
4
;
RBACK assigns 1 to
x
3
and a physically stored consistent image of database
is loaded into the dynamic data memory (registers of
M
R
controlled by Buffer
Manager).
4. The initial input function
In
R
generates the initial state
st
(
0
)
by assigning 0 to
x
1
and
x
2
and 1 to
x
3
, and a physically stored consistent image of database is loaded
into the dynamic data memory (registers of
M
R
controlled by Buffer Manager so
that
Out
DB
(st
(
0
))
is this loaded and consistent database).
5. The extended input function
In
∗
ER
satisfies the following properties:
•
f
:
S
R
→
S
R
if
z
is
(n,m,L)
or a database;
λIn
∗
ER
(z)
=
id
:
S
R
→
S
R
(
identity function
)
otherwise
,
such that for a state
st
(k)
S
R
,
st
(k
f(st
(k))
∈
+
=
∈
1
)
S
R
is obtained from
st
(k)
by the following setting:
x
1
=
m
and the list of values in
L
is
loaded in the subset of registers of
S
R
used for the I/O memory if
z
x
4
=
n,x
2
=
(n,m,L)
.
Otherwise, if
z
is a database then it is loaded into the dynamic data-memory.
6. The output function
Out
R
satisfies the following properties:
=
Out
R
st
(k)
=
(
empty set
)
if
t
1
(st
(k))
∅
=
0
;
(
0
,n,R)
otherwise
,
where
R
is a relation in
I/O
memory of
M
R
(obtained by last execution of a
program
P
k
in the Application Plane) and
n
is the value of its register
x
2
, with
R
if
n>
0or
P
k
is not obtained from a SQL statement 'SELECT...'inthe
source program
P
. If the output is a triple
(
0
,n,R)
then it is transmitted to
M
U
.
7. The DB output function
Out
DB
:
=⊥
Ob
DB
such that, for each state
st
(k)
S
R
→
∈
S
R
,
Out
DB
(st
(k))
is the current database in the memory of Buffer Manager.
Notice that if
t
1
(st
(k))
1 and a database in data-memory is consistent then
VCON in this state
st
(k)
imposes the error condition register to
x
2
=
=
0.
A database in the memory of Buffer Manager obtained by RBACK is a just the
last version of database in the physical storage.
The name 'categorial machine' is based on the following theorem:
Theorem 10
(C
ATEGORIAL
M
ACHINE
)
3,
is obtained from an arrow f
k
:
t
RA
→
f
k
(t
RA
) of the 'syntax' category
RA
by sub-
stitution of the Σ
RA
operators with the corresponding variable-binding operators
.
An execution of P
k
in
M
R
corresponds to the transformation of such an Application
Plan into an arrow in
RA
(
by binding the bounded variables in the variable-binding
Every Application Plan P
k
in
M
R
,
k
≥
