[Prev][Next][Index][Thread]
Stability and Sequentiality
Date: Sat, 17 Jun 89 13:08:28 WET DST
apropos the MIT seminar announcement from craig@theory.lcs.mit.edu
"Reasoning about Sequential Functions via Logical Relations" by Kurt Sieber
This already seems to be an improvement over
previous purely semantic approaches, which are either
insufficient even for the first order case (like stability)
Clearly the equation stable=sequential was wrong, as Berry himself
showed. However this is not a reason for dismissing the idea of
stability in the analysis of sequential and parallel behaviour.
What is wrong with it is its use in a poset (qualitative) rather than
category (quantitative) setting.
Consider a program~$S$ consisting of several parallel processes
which merge their output indiscriminantly {\it without suppression of
duplication}; for instance ``parallel~or'' would output~${\bf t}$
{\it twice} on input $<{\bf t},{\bf t}>$. Suppose that on input~$X$ (a~bag
of tokens from~$A$) its output includes an instance~$Y=\{j\}$ of a
token~$j\in B$. This has come from a particular process, which itself
has pursued a {\it sequential} execution path, involving certain
``hurdles'' which amount to reading and matching a pattern~$X_0$ in~$X$;
moreover if~$X$ had contained only this pattern, $Y$~would still have
been output. The candidate is the function $u:Y\to SX_0$ which identifies
this instance of the token~$j$ in the output, but there may have been
many other ways in which this or other parallel processes could have
generated~$j$, but identified by different~$u$'s.
(Please excuse the TeX: this is an extract from my paper "Quantitative
Domains, Groupoids and Linear Logic" to be presented at the Manchester
"Category Theory and Computer Science" meeting in September; an early
version was circulated as "An Examination of Girard's Quantitative
Domains". My term "candidate" corresponds exactly to Berry's "modulus
of stability" and the definition is applicable to many constructions
in pure mathematics.)
I claim that "parallel or" resolves into a logical part, which itself
has three components matching ff, t? and ?t, and a merge part, which
suppresses duplicated output t from input tt and also merges this with
output f from ff. Only the suppression of duplication is non-stable,
so long as we work with (stable) domains which have "disjoint and
universal" coproducts.
I would suggest that suppression of duplication is itself a dubious operation.
An example: The Thatcher regime is busily selling off everything
in sight, some of it to the general public. I don't understand why, but
it is an imprisonable offence to submit two applications for shares, so they
have eleborate methods for spotting duplicate applications. As you
can imagine, considered simply as a programming problem, this is not
easy to do.