(* * THE DATATYPE OF (TOTAL, DETERMINISTIC) PROCESSES * *) data C -> proc(A, B) = pr: C -> A => B * C. (* COMPOSITION (WIRING IN SERIES): *) def ser: proc(A, B) * proc(B, C) -> proc(A, C) = pp => (| (c1, c2) => pr: a => { (b, c1') => { (c, c2') => (c, (c1', c2')) } pr (b, c2) } pr (a, c1) |) pp. (* PARALLELIZATION (WIRING IN PARALLEL): *) def par: proc(A, B) * proc(C, D) -> proc(A * C, B * D) = pp => (| (c1, c2) => pr: (a, c) => { ((b, c1'), (d, c2')) => ((b, d), (c1', c2')) } (pr (a, c1), pr (c, c2)) |) pp. (* * THE DATATYPE OF PARTIAL PROCESSES * *) data C -> Pproc(A, B) = Ppr: C -> A => SF(B * C). (* * THE DATATYPE OF NONDETERMINISTIC PROCESSES * *) data C -> NDproc(A, B) = NDpr: C -> A => list(B * C).