Information Technology Reference
In-Depth Information
MS
∗
:
MS
2
→
(
s
1
, true, true
)
(
s
2
, q
2
, r
2
)
=
(
s
1
♦
s
2
, q
2
, r
2
)
(
s
1
, q
1
, true
)
(
true, q
2
, r
2
)
=
(
s
1
, q
1
♦
q
2
, r
2
)
(
s
1
, q
1
, r
1
)
(
true, true, r
2
)
=
(
s
1
, q
1
, r
1
♦
r
2
)
m
1
m
2
=
m
1
, m
2
We then define microslot-sequence catenation using the binary merge-slot oper-
ator:
:
MS
∗
MS
∗
MS
∗
×
→
9
=
μ
2
μ
1
9
=
μ
1
9
μ
2
o
=(
m
1
m
2
)
μ
2
m
1
9
(
m
2
:
μ
2
)
o
(
m
1
:
μ
1
)
9
μ
2
=
m
1
:(
μ
1
9
μ
2
)
Consing Slots onto Traces.
We now consider the task of cons-ing a
Slot
onto
the start of a
Trc
in order to extend the
Trc
. Here, no type is specified, but
instead is inferred from the slot contents.
The only time this differs from ordinary list cons is when the trailing trace is
a singleton null slot or the slot is null or has no
act
action:
::
:
Slot
×
Trc
→
Trc
s
::
nils
=
s
nils
::
τ
=
τ
(
μ, true
)::((
ν, a
):
τ
)
=((
μ
9
ν
)
, a
):
τ
s
::
τ
=
s
:
τ
Catenation of Traces.
We can now define trace catenation in terms of slot-
consing:
:
Trc
×
Trc
→
Trc
9
9
τ
2
=
τ
2
s
9
τ
2
=
s
::
τ
2
(
s
1
:
τ
1
)
9
τ
2
=
s
1
:(
τ
1
9
τ
2
)
Traces are non-empty, but the first clause is needed simply to handle a base
case properly for the definition of the operator. We want the null trace to be an
identity for trace catenation, and trace catenation to be associative.
5.4
Merging Traces in Parallel
Merging traces in parallel is straightforward — they are merged on a slot by
slot basis, with slots merged on a micro-slot by micro-slot basis. We overload
Search WWH ::
Custom Search