Information Technology Reference
In-Depth Information
=
i∈
[1
,n
]
j∈
[1
,m
]
{K
1
,...,
K
n
}·{H
1
,...,
H
m
}
{K
i
}·{H
j
}
(1)
{
(
K,b
)
}·{
(
H,c
)
}
=
{
(
K
∪
H, b
c
)
}
(2)
The operation maintains the disjunctive form of the clause structure (1). Single
clauses are conjunctive and thus their meet is simply the union of the clauses.
The truth values are combined in terms of the meet on
B
4
(2).
Stack Control.
The actual transition function of
M
makes direct use of the
finite control function
δ
c
on internal action
a
int
∈
Σ
int
actions since they do not
involve a stack operation. Only the stack evaluation is used in the output:
δ
(
{ϕ
1
,...,ϕ
n
},
(
K,b
1
,b
2
)
,a
int
)=(
δ
c
(
{ϕ
1
,...,ϕ
n
},a
int
)
·{
(
∅,b
1
)
}
)
×{
(
K,b
1
,b
2
)
}
Σ
r
, the top-most stack symbol is removed and
combined to the current control state. That is, the obligation suspended to the
stack earlier on the matching call is now evaluated. Note, that the preliminary
verdictatcalltime(
b
1
) now is obsolete and the previous one (
b
2
) is evaluated.
On return operations
a
r
∈
δ
(
{
ϕ
1
,...,ϕ
n
}
,
(
K,b
1
,b
2
)
,a
r
)=(
δ
c
(
{
ϕ
1
,...,ϕ
n
}
,a
r
)
·{
(
K,b
2
)
}
)
×{
}
For a call
a
∈
Σ
c
we have
,γ,a
)
˜
...
˜
δ
(
{
ϕ
1
,...,ϕ
n
}
,γ,a
)=
δ
(
{
ϕ
1
}
δ
(
{
ϕ
n
}
,γ,a
)
X
a
ϕ
p
p
δ
(
{
}
,
(
K,b
1
,b
2
)
,a
)=
{
(
∅
,
⊥
b
1
,
(
{
ϕ
}
,
⊥
b
1
,b
1
)(
K,b
1
,b
2
))
}
p
p
δ
(
{
X
a
ϕ
}
,
(
K,b
1
,b
2
)
,a
)=
{
∅
,
b
1
,
(
{
ϕ
}
,
b
1
,b
1
)(
K,b
1
,b
2
))
}
(
δ
(
{ϕ
U
a
ψ},γ,a
)=
δ
(
{ψ ∨
(
ψ ∧
X
a
(
ϕ
U
a
ψ
))
},γ,a
)
δ
(
ϕ
R
a
ψ
X
a
(
ϕ
R
a
ψ
))
{
}
,γ,a
)=
δ
(
{
ψ
∧
(
ψ
∨
}
,γ,a
)
and for
ϕ
=X
a
ϕ
,
ϕ
=
ϕ
U
a
ψ
,
ϕ
= X
a
ϕ
and
ϕ
=
ϕ
R
a
ψ
δ
(
{
ϕ
}
,
(
K,b
1
,b
2
)
,a
)=(
δ
c
(
{
ϕ
}
,a
)
·{
(
∅
,b
1
)
}
)
×{
(
∅
,b
1
,b
1
)(
K,b
1
,b
2
)
}
Γ
2
be tuples of states
(i.e. conjunctive clauses), verdicts and the top-most stack symbols. Note, that
when ever a call occurs, the topmost stack symbol is not touched but a new
symbol is pushed onto the stack. Therefore, the pushed symbols
α
i
=(
A
i
,u
i
)
and
β
i
=(
B
i
,v
i
) may differ whilst the symbol underneath is the same
γ
=(
G,g
)
for all tuples
K
i
and
H
i
.
Sets of such tuples are combined by means of a the meet-like operation
K
i
=(
K
i
,b
i
,α
i
γ
)
,
H
j
=(
H
j
,c
j
,β
j
γ
)
∈
Q
×
B
4
×
Let
:2
Q×
B
4
×Γ
2
2
Q×
B
4
×Γ
2
2
Q×
B
4
×Γ
2
˜
×
→
