NOTE: This transcription was contributed by Martin P.M. van der Burgt, who has devised a process for producing transcripts automatically. Although its markup is incomplete, we believe it serves a useful purpose by virtue of its searchability and its accessibility to text-reading software. It will be replaced by a fully marked-up version when time permits. —HR
Associons continued.
by | ||
Edsger W.Dijkstra, W.H.J.Feijen and M.Rem |
Up till now our original goal, that is high concurrency, has hardly been incorporated. We intend to introduce the possibility of high concurrency by introducing statements operating on sets. But rather than introducing variables, whose values are sets, we propose to characterize sets as “all the solutions of equations”. The unknowns of these equations will be names: in our equations we shall indicate them with the reserved identifiers x0, x1, x2 etc.
For instance, let the store contain a large number of associons of the form (fatherof,“n1”,“n2”), where “n1” and “n2” stand for names of persons. To derive from this genealogy the brother-relation, we would write
(fatherof,x0,x1) and (fatherof,x0,x2) ⇒ (brotherof,x1,x2) . |
Here the expression at the left-hand side of the implication sign is regarded as an equation in the names x0, x1 and x2, and it defines the set of all ordered triples “x0, x1, x2” such that, upon substitution, the two associons mentioned occur in store. For each solution for whivh (brotherof,x1,x2) is not in store it will be created; the amount of concurrency is up to the implementation. The statement terminates when for all solutions of the left-hand side the righthand side holds as well.
The above program records any person with a father as a brother of himself. If that is not the intention, the situation could be adjusted by adding a next statement
(brotherof,x0,x0) = non (brotherof,x0,x0) . |
() ⇒ non (brotherof,x0,x0); |
(brotherof,c0,c0) ⇒ non () |
For all unknowns that occur only once in a statement —i.e. once at the left-hand side and not at the right-hand side— it seems a bit superfluous to give that unknown a specific name. For instance, if we want to create associons indicating who is a father, we could of course do it with
(fatherof,c0,x1) = (isfather,x0) |
(fatherof,c0,?) ⇒ (isfather,c0) . |
The question-mark has the function of the existential quantifier: (fatherof,n, holds if and only if there exists at least one person of whom n has been recorded to be the father. Viewed in terms of “associon matching” refers to a don’t care position.
We may also have it at the right-hand side, provided that the term is negated:
() ⇒ non (fatherof,?,?); |
We do allow the question-mark in a negated term at the left-hand side as well, e.g.
(fatherof,?,c0) and non (fatherof,c0,?) ⇒ (nooffspring,x0) . |
To create the above set of associons “nooffspring” without a question-mark is very painful. It could be done by
(fatherof,x0,x1) ⇒ (nooffspring,x1); | |
(fatherof,c0,x1) ⇒ non (nooffspring,c0) |
What would have failed to work is
(fatheroff,x1,x0) and non (fatherof,x0,x2) = (nooffspring,x0) . |
| a negative trem at the left-hand side may contain no x that does not | |
| occur in a positive term of that left-hand side as well. |
* *
*
Let for any node name n, n1, n2,
(r0,n) <=> “n is the name of a node of a given directed graph” | ||
(r1,n1,n2) <=> “the directed edge from n1 to n2 belongs to the given directed graph.” |
(r2,n1,n2) <=> “from.n1 the node n2 can be reached.” |
(r0,x0) ⇒ (r2,x0,x0); | |
(r2,x0,x1) and (r1,x1,x2) ⇒ (r2,x0,x2) |
(r0,x0) = (r2,x0,x0); | |
(r1,x0,x1) = (r2,x0,x1); | |
(r2,x0,x1) and (r2,x1,x2) ⇒ (r2,x0,x2) |
* *
*
When no three points are on the same line, let
(r0,n) <=> “n is the name of a point in the plane”. | |
(r1,n1,n2,n3) <=> “n1,n2,n3 is a clock-wise triangle.” |
(r1,x0,x1,?) and non (r1,x1,x0,?) = (r2,x0,x1) . |
* *
*
Let
(r0,n) <=> “n is the name of a node”. |
(r1,n) <=> “n is the chosen node”. |
(r0,x0) = (r1,x0) |
(r0,x0) and non (r1,?) ⇒ (r1,x0) . | (1) |
This is OK under the assumption that the implementation selects only one solution of the left-hand side at a time: it would select e.g. x0 = nl, then create (r1,n1) and then it would stop. However, we would not like to impose this non-concurrency as a general requirement, i.e. we would like this statement also to allow that an unknown number of nodes is selected, n1 through nk, and that for all of them (r1,ni) is created. In short: our statement selects an arbitrary non-empty subset of the set of nodes. (If the given set is empty, the selected set is empty as well.) Well, (1) is a nice, non-deterministic tool, but it is still not a way for selecting exactly one!
Alternatively: if we cannot select one, can we remove all but one? With the aid of
(r1,n1,n2) <=> “n1 is n2” |
(r0,x0) = (r1,x0); | |
(r0,x0) = (r2,x0,x0); | |
(r1,x0) and (r1,x1) and non (r2,x0,x1) ⇒ non (r1,x1) |
A new tool seems indicated: we must be able to prescribe that we only need one solution. We shall do so by using instead of the x, the equally reserved identifier y and the selection of the unique node will be accomplished by
(r0,y0) and non (r1,?) ⇒ (r1,y0) . |
(r0,y0) ⇒ (r1,y0) |
Let it be required to order the nodes in an arbitrary permutation, i.e.
(r3,n1,n2) <=> “n1 is n2’s left-hand neighbour.” |
(r0,y0) and non (r3,?,?) ⇒ (r3,handle,y0); | |
(r3,?,y0) and non (r3,y0,?) and (r0,y1) and non (r3,?,y1) ⇒ (r3,y0,y1); | |
() ⇒ non (r3,handle,?) |
(r3,?,n) <=> “n has been placed in the sequence”. |
Here we have our first equation with two y’s. It means: select from all solutio —as if they had been x’es!- exactly one sing1e pair. What about x’es and y’s occurring in the same left-hand equation?
Let us have one x and one y in a left-hand side equation. The corresponding solution set could be either:
a) every possible value of x combined with one then possible value of y.
b) one value of y combined with all then possible values of x. The choice we have is due to the fact that the universal and the existential quantifier do not commute.
We propose to distinguish between the two cases by the way in which we number our unknowns; and to indicate
case a) | by | x0 y1 |
case b) | by | y0 x1. |
The set of solutions for an equation in
z0,z1, ... ,zn |
We start with one empty k-tuple for k = 0.
If zk = xk,
each k-tuple gives rise to as many k+1-tuples that we can form by extending | |
it with a permissible value for xk; each k-tuple gives rise to at least one | |
k+1-tuple; |
each k - tuple gives rise to exactly one k+1-tuple that we can form by | |
extending it with an arbitrary permissible value for yk. |
Note 1. The relative ordering of succesive x’es is irrelevant; so is the relative ordering of successive y’s. (End of note 1)
Note 2. When in a statement all x’es are replaced by y’s, its activity is equal to a possible activity of the original form, because the concurrency when x’es are present is not obligatory. They are therefore identical when the statement with the x’es is deterministic. (End of note 2)
Note 3. We don’t expect much use of complicated alternation of x’es and y’s in the ordered sequence of unknowns. (End of note 3)
* *
*
Let for N different values of n
(r0,n) <=> “n is the name of a node”. |
(r1,n1,n2) <=> “n1,n2 is a directed edge of an arbitrary rooted spanning tree.” |
(r0,y0) and non (r1,?,?) ⇒ (r1,handle,y0); | |
(r0,x0) and non (r1,?,x0) and (r1,?,y1) ⇒ (r1,y1,x0) | |
() ⇒ non (r1,handle,?) |
* *
*
(To be continued.)
Transcribed by Martin P.M. van der Burgt
Last revision 2014-11-15
.