1478:. There are two reasons for this. The first reason is that most power domains are simply generalizations of domains that have been used as semantic domains for conventional sequential programs, and such domains are all complete because of the need to compute fixed points in the sequential case. The second reason is that ω-completeness permits the solution of recursive domain equations involving the power domain such as
22:
549:
1902:
Timed
Diagrams denotational semantics constructs an ω-complete computational domain for Actor computations. In the domain, for each event in an Actor computation, there is a delivery time which represents the time at which the message is delivered such that each delivery time satisfies the following
1631:
From the Actor point of view, sequential computations are a special case of concurrent computations, distinguishable by their event diagrams. The event diagram of a sequential computation has an initial event, and no event activates more than one event. In other words, the activation ordering of a
1583:
The semantics presented in is a version of behavioral semantics. A program denotes a set of Actor event diagrams. The set is defined extensionally using power domain semantics rather than intensionally using causal axioms. The behaviors of individual Actors is defined functionally. It is shown,
1553:
can be defined for any domain whatsoever. Furthermore the power domain of a domain is essentially the power domain of its ω-completion, so recursive equations involving the power domain of an incomplete domain can still be solved, provide the domains to which the usual constructors (+, ×, →, and *)
1893:
Hewitt published a new denotational semantics for Actors based on Timed
Diagrams. The Timed Diagrams model stands in contrast to Clinger which constructed an ω-complete power domain from an underlying incomplete diagrammatic domain, which did not include time. The advantage of the domain Timed
1617:
The fact that there exist increasing sequences without least upper bounds may seem strange to those accustomed to thinking about the semantics of sequential programs. It may help to point out that the increasing sequences produced by sequential programs all have least upper bounds. Indeed, the
1372:
in which some pending event remains pending forever while the number of realized events grows without bound, contrary to the requirement of finite delay. Such a sequence cannot have a limit, because any limit would represent a completed nonterminating computation in which an event is still
1577:
Henry Baker has presented a nondeterministic interpreter generating instantaneous schedules which then map onto event diagrams. He suggested that a corresponding deterministic interpreter operating on sets of instantaneous schedules could be defined using power domain semantics
301:
1572:, the meaning of program is a specification of the computations that may be performed by the program. The computations are represented formally by Actor event diagrams. Greif specified the event diagrams by means of causal axioms governing the behaviors of individual Actors .
1584:
however, that the resulting set of Actor event diagrams consists of exactly those diagrams that satisfy causal axioms expressing the functional behaviors of Actors. Thus Greif's behavioral semantics is compatible with a denotational power domain semantics.
1735:
corresponding to the finite initial segments of a sequential execution sequence all have exactly one pending event, excepting the largest, completed element if the computation terminates. One property of the augmented event diagrams domain <
1910:
The delivery time is more than a fixed δ greater than the time of its activating event. It will later turn out that the value of δ doesn't matter. In fact the value of δ can even be allowed to decrease linearly with time to accommodate Moore's
739:). Thus there arose the problem of how to provide modular denotational semantics for concurrent programming languages. One solution to this problem is to use the Actor model of computation. In Actor model, programs are Actors that are sent
374:
2266:
The criterion of continuity for the graphs of functions that Scott used to initially develop the denotational semantics of functions can be derived as a consequence of the Actor laws for computation as shown in the next section.
1610:
Instead of beginning with a semantics for sequential programs and then trying to extend it for concurrency, Actor semantics views concurrency as primary and obtains the semantics of sequential programs as a special
170:
2263:, which is ω-complete, is important because it provides for the direct expression of the above representation theorem for the denotations of Actor systems by directly constructing a minimal fixed point.
1855:
1723:
1364:
1894:
Diagrams model is that it is physically motivated and the resulting computations have the desired property of ω-completeness (therefore unbounded nondeterminism) which provides guarantee of service.
743:
messages with the address of an environment (explained below) so that programs inherit their denotational semantics from the denotational semantics of the Actor model (an idea published in Hewitt ).
727:
provides a modern and very general way the compositionality of programs can be analyzed. Scott and
Strachey proposed that the semantics of programming languages be reduced to the semantics of the
1266:
represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of
1927:
represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of
1541:
1919:, ≤>. The diagrams are partial computation histories representing "snapshots" (relative to some frame of reference) of a computation on its way to being completed. For d1, d2ε
94:
The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. Collections of such objects are called
1593:, which represent messages on the way to their targets. Each pending event must become an actual (realized) arrival event sooner or later, a requirement referred to as
1384:
is incomplete because of the requirement of finite arrival delay, which allows any finite delay between an event and an event it activates but rules out infinite delay.
680:
of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example, consider the expression "
544:{\displaystyle \mathbf {progression} _{\mathtt {S}}(\lim _{i\to \infty }{\mathtt {x}}_{i})=\lim _{i\to \infty }\mathbf {progression} _{\mathtt {S}}({\mathtt {x}}_{i})}
1554:
are applied are ω-complete. It happens that defining Actor semantics as in
Clinger does not require solving any recursive equations involving the power domain.
2276:
Dana Scott and
Christopher Strachey. Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. PRG-6. 1971.
2105:
subject to the constraint that each event in X is scheduled at least δ after e and every event in X is scheduled at least once in every δ interval after that.
40:
1967:
is directed and x≤VD, there exists dεD with x≤d. In other words, x is finite if one must go through x in order to get up to or above x via the limit process.
1597:. Augmenting Actor event diagrams with sets of pending events helps to express the finite delay property, which is characteristic of true concurrency .
1182:
programs (see ). For example, it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as
566:
A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) according to the equation for
2487:
2364:
736:
1234:
below). The augmented diagrams are partial computation histories representing "snapshots" of a computation on its way to being completed. For
102:
uses the domain of event diagram scenarios. It is usual to assume some properties of the domain, such as the existence of limits of chains (see
1632:
sequential computation is linear; the event diagram is essentially a conventional execution sequence. This means that the finite elements of
1199:
296:{\displaystyle \mathbf {Denote} _{\mathtt {S}}\equiv \lim _{i\to \infty }\mathbf {progression} _{{\mathtt {S}}^{i}}(\bot _{\mathtt {S}})}
2375:
1618:
partial computations that can be produced by sequential computation form an ω-complete subdomain of the domain of Actor computations
2422:
2350:
2341:
1782:
1650:
1291:
1884:. Thus Actor semantics includes sequential programs as a special case, and agrees with conventional semantics of such programs.
1559:
In short, there is no technical impediment to building power domains from incomplete domains. But why should one want to do so?
2492:
1171:
1393:
In his doctoral dissertation, Will
Clinger explained how power domains are obtained from incomplete domains as follows:
1475:
868:
2087:
An Actor computation can progress in many ways. Let d be a diagram with next scheduled event e and X ≡ {e’ | e ─≈→
1606:
In his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:
2379:
1907:
The delivery time is a positive rational number that is not the same as the delivery time of any other message.
1487:
2347:
Proceeding of IFIP Working
Conference on Formal Description of Programming Concepts. August 1–5, 1977.
735:. However, it turned out that concurrent computation could not be implemented in the lambda calculus (see
50:
into an encyclopedic article, please do so and remove this message and/or add a link to the
Wikibook using
1231:
1167:
1163:
677:
103:
70:
1923:, d1≤d2 means d1 is a stage the computation could go through on its way to d2 The completed elements of
1769:
has at most one pending event, every pending event in the sequence becomes realized. Hence the sequence
106:) and a bottom element. Various additional properties are often reasonable and helpful: the article on
1187:
2095:), Flow(d) is defined to be the set of all timed diagrams with d and extensions of d by X such that
144:
is found by constructing increasingly better approximations from an initial empty denotation called
2467:
1183:
21:
117:, which can be understood as an order of definedness. For instance, given event diagram scenarios
2414:
2092:
1949:
54:
2102:
the events of X are scheduled in all possible orderings among the scheduled future events of d
1175:
1162:
The denotational compositional semantics presented above is very general and can be used for
47:
2320:
1881:
1420:
is given by the subset relation, least upper bounds do not in general coincide with unions.
2456:
Proceedings of the Winter School on Formal
Software Specification. Springer-Verlag. 1980.
2307:
1880:
The above proof applies to all sequential programs, even those with choice points such as
1119:
728:
1996:
M is closed under least upper bounds of directed sets, i.e. if D⊆M is directed, then VDεM
1272:. Concretely, the completed elements are those having non pending events. Intuitively,
1602:
Sequential computations form an ω-complete subdomain of the domain of Actor computations
1474:
Usually the partial order from which the power domain is constructed is required to be
1279:
1436:
represents a list of possible initial histories of a computation. Since for elements
2481:
2463:. MIT Mathematics Doctoral Dissertation, June 1981. (Quoted by permission of author.)
2314:
2291:
Denotational
Semantics: The Scott-Strachey Approach to Programming Language Semantics
1550:
1397:
732:
114:
107:
95:
79:
2400:
2386:
2370:
1948:
is directed, the least upper bound ⊔D exists; furthermore ⊔D obeys all the laws of
770:
below which implements a tree data structure when supplied with parameters for a
2410:
2337:
1569:
1123:
724:
99:
83:
74:
1974:
is the least upper bound of a countable increasing sequence of finite elements.
828:. One semantics for application expressions such as this one is the following:
1986:, ⊆> is the set of possible initial histories M of a computation such that
751:
Environments hold the bindings of identifiers. When an environment is sent a
2294:
36:
1410:
that are also closed under existing least upper bounds of directed sets in
32:
2286:
1931:. Concretely, the completed elements are those having no pending events.
2230:
of a timed diagram to be the diagram with the time annotations removed.
1282:
because there exist increasing sequences of finite partial computations
1214:
The augmented Actor event diagrams form a partially ordered set <
2109:(Recall that δ is the minimum amount of time to deliver a message.)
2446:
575:. A fundamental theorem of computational domain theory is that if
659:
Furthermore, this fixed point is least among all fixed points of
2432:
in Semantics of Concurrent Computation. Springer-Verlag. 1979.
2393:
2297:, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
1915:
The Actor event timed diagrams form a partially ordered set <
1210:
Clinger explained the domain of Actor computations as follows:
86:. The historical development of this subject is recounted in .
2192:
is given by the Concurrency Representation Theorem as follows:
766:
As an example of how this works consider the lambda expression
692:". Compositionality in this case is to provide a meaning for "
2001:
Note: Although Power is ordered by ⊆, limits are not given by
1202:
developed the first denotation semantics for the Actor model.
15:
2439:
Semantics of Concurrent Computation. Springer-Verlag. 1979.
1030:. When the composite expression Actor (process) receives an
2405:
Semantics of nondeterminism, concurrency, and communication
2099:
the arrival all of the events of X has been scheduled where
1850:{\displaystyle x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...}
1718:{\displaystyle x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...}
1359:{\displaystyle x_{0}\leq x_{1}\leq x_{2}\leq x_{3}\leq ...}
1002:
For another example consider the Actor for the expression "
2223:
of an Actor system S is the set of all computations of S.
1256:
is a stage the computation could go through on its way to
1589:
Baker's instantaneous schedules introduced the notion of
2468:
What is Commitment? Physical, Organizational, and Social
2407:
Journal of Computer and System Sciences. December 1979.
1406:
is the collection of downward-closed subsets of domain
1014:" which has addresses for two other actors (processes)
1785:
1653:
1490:
1294:
816:
Consider what happens when an expression of the form
377:
173:
1940:
is an ω-complete domain of Actor computations i.e.,
1224: > from which to construct the power domain
1849:
1717:
1549:which defines a domain of resumptions . However,
1535:
1468:be downward-closed has a clear basis in intuition.
1358:
952:message for any other identifier, it forwards the
634:The above equation motivates the terminology that
543:
295:
2419:On describing the behavior of distributed systems
2238:S of an Actor system S is the time abstraction of
2188:Furthermore, the least fixed point of Progression
778:. When such a tree is given a parameter message
1034:message with addresses for an environment Actor
797:λ(leftSubTree, rightSubTree) λ(message)
462:
426:
207:
1118:. In this way, the denotational semantics for
2403:, Daniel Lehmann, and Willem-Paul de Roever.
2437:An extensional treatment of dataflow deadlock
2357:MIT EECS Doctoral Dissertation. January 1978.
2283:MIT EECS Doctoral Dissertation. August 1975.
2281:Semantics of Communicating Parallel Professes
1458:is an initial segment of the initial history
759:, it returns the latest (lexical) binding of
733:denotational semantics of the lambda calculus
151:using some denotation approximating function
8:
2474:editors. LNAI 4386. Springer-Verlag. 2007.
2304:SIAM Journal on Computing September 1976.
1993:if dεM, then ∀d’εTimedDiagrams d’≤d ⇒ d’εM
1378:To repeat, the actor event diagram domain
755:message with the address of an identifier
2421:in Semantics of Concurrent Computation.
1829:
1816:
1803:
1790:
1784:
1697:
1684:
1671:
1658:
1652:
1489:
1338:
1325:
1312:
1299:
1293:
672:Compositionality in programming languages
532:
526:
525:
514:
513:
478:
465:
449:
443:
442:
429:
415:
414:
379:
376:
283:
282:
267:
261:
260:
258:
223:
210:
196:
195:
175:
172:
160:to construct a denotation (meaning ) for
140:The mathematical denotation for a system
41:Denotational semantics of the Actor model
2334:Theor. Comput. Sci. 2(2): 155-181 (1976)
344:. More generally, we would expect that
2365:Journal of Computer and System Sciences
2355:Actor Systems for Real-Time Computation
1536:{\displaystyle R\approx S\rightarrow P}
737:Indeterminacy in concurrent computation
1963:is finite (isolated) if and only if D⊆
1126:provide a denotational semantics for "
2444:Semantics of Unbounded Nondeterminism
2430:Denotational semantics of parallelism
2391:Concurrent processes and their syntax
2115:Let S be an Actor system, Progression
1158:Other programming language constructs
912:, it creates a new environment Actor
527:
515:
444:
416:
284:
262:
197:
7:
2454:On the semantics of fair parallelism
786:and likewise when given the message
596:It follows from the ω-continuity of
2325:Exercises in Denotational Semantics
2216:is the initial configuration of S.
1462:, the requirement that elements of
1424:For the actor event diagram domain
1414:. Note that while the ordering on
2376:Communicating Sequential Processes
2083:Concurrency Representation Theorem
1898:Domain of Timed Actor Computations
975:to the following actor (process):
472:
436:
279:
217:
14:
2345:Actors and Continuous Functionals
1959:are countable where an element xε
2112:Flow(d) ≡ {d} if d is complete.
1984:Definition: The domain <Power
1206:The domain of Actor computations
1138:" in terms of the semantics for
509:
506:
503:
500:
497:
494:
491:
488:
485:
482:
479:
410:
407:
404:
401:
398:
395:
392:
389:
386:
383:
380:
254:
251:
248:
245:
242:
239:
236:
233:
230:
227:
224:
191:
188:
185:
182:
179:
176:
20:
2078:Power is an ω-complete domain.
78:is the subject of denotational
2488:Actor model (computer science)
2461:Foundations of Actor Semantics
1530:
1527:
1515:
1506:
1500:
1198:In his doctoral dissertation,
704:" in terms of the meanings of
538:
521:
469:
455:
433:
422:
290:
275:
214:
1:
1754:, then some pending event of
1624:. An informal proof follows.
1260:. The completed elements of
1084:has received back two values
554:This last stated property of
2332:Least Fixed Points Revisited
916:which behaves as follows:
875:that has an address (called
2312:A Discipline of Programming
1867:has a least upper bound in
1762:. Since in this case each
938:message for the identifier
924:message for the identifier
90:Actor fixed point semantics
2509:
2302:A powerdomain construction
840:messages with environment
306:It would be expected that
1873:in accord with intuition.
971:message with environment
856:message with themselves.
852:immediately reply to the
824:message with environment
133:extends the computations
1889:The Timed Diagrams Model
990:(message == "getRight")
809:(message == "getRight")
563:is called ω-continuity.
113:A domain is typically a
2234:Representation Theorem:
1955:The finite elements of
982:(message == "getLeft")
883:and an address (called
801:(message == "getLeft")
676:An important aspect of
2493:Denotational semantics
1989:M is downward-closed,
1851:
1746: > is that if
1719:
1537:
1360:
1070:a new Actor (process)
998:Arithmetic expressions
867:message by creating a
678:denotational semantics
545:
297:
71:denotational semantics
2236:The denotation Denote
2219:The denotation Denote
1852:
1720:
1538:
1361:
1193:
1132:> + <expression
1008:> + <expression
909:receives the message
731:and thus inherit the
698:> + <expression
686:> + <expression
584:is ω-continuous then
546:
298:
1783:
1651:
1566:behavioral semantics
1488:
1396:From the article on
1292:
1230:(see the section on
963:The Actor (process)
375:
171:
46:If this page can be
2323:, J. W. de Bakker.
948:When it receives a
942:, it responds with
934:When it receives a
928:, it responds with
920:When it receives a
2442:Ralph-Johan Back.
2415:Michael J. Fischer
2093:Actor model theory
1950:Actor model theory
1847:
1715:
1533:
1356:
541:
476:
440:
293:
221:
110:has more details.
2385:George Milne and
2330:J. W. de Bakker.
2300:Gordon Plotkin.
2259:Using the domain
2145:is ω-continuous.
1970:Every element of
1062:with environment
986:leftSubTree
893:"(<L> 1 2)"
818:"(<L> 1 2)"
805:leftSubTree
461:
425:
206:
125:, one might let "
66:
65:
2500:
2435:William Wadge.
2428:Jerald Schwartz
2399:Nissim Francez,
2382:. August, 1978.
2360:Michael Smyth.
2321:Krzysztof R. Apt
2228:time abstraction
2160:then Progression
2068:
2036:
1882:guarded commands
1872:
1856:
1854:
1853:
1848:
1834:
1833:
1821:
1820:
1808:
1807:
1795:
1794:
1745:
1741:
1724:
1722:
1721:
1716:
1702:
1701:
1689:
1688:
1676:
1675:
1663:
1662:
1637:
1623:
1542:
1540:
1539:
1534:
1467:
1449:
1435:
1430:, an element of
1429:
1419:
1413:
1409:
1405:
1383:
1365:
1363:
1362:
1357:
1343:
1342:
1330:
1329:
1317:
1316:
1304:
1303:
1277:
1271:
1265:
1247:
1229:
1223:
1219:
1153:
1145:
1137:
1111:
1061:
1053:
1045:
1038:and a customer
1033:
1029:
1021:
1013:
978:λ(message)
970:
955:
951:
945:
941:
937:
931:
927:
923:
894:
882:
871:Actor (process)
866:
863:responds to the
862:
855:
851:
847:
844:. The integers
839:
835:
831:
823:
819:
793:
789:
785:
781:
777:
773:
769:
754:
742:
719:
711:
703:
691:
667:
655:
642:
630:
604:
592:
583:
574:
562:
550:
548:
547:
542:
537:
536:
531:
530:
520:
519:
518:
512:
475:
454:
453:
448:
447:
439:
421:
420:
419:
413:
368:
364:
359:
355:
351:
343:
326:
314:
302:
300:
299:
294:
289:
288:
287:
274:
273:
272:
271:
266:
265:
257:
220:
202:
201:
200:
194:
163:
159:
150:
143:
136:
132:
128:
124:
120:
61:
59:
53:
24:
16:
2508:
2507:
2503:
2502:
2501:
2499:
2498:
2497:
2478:
2477:
2423:Springer-Verlag
2396:. April, 1979.
2327:MFCS 1976: 1-11
2308:Edsger Dijkstra
2273:
2254:
2250:
2246:
2239:
2222:
2215:
2207:
2203:
2199:
2191:
2183:
2179:
2175:
2171:
2167:
2163:
2159:
2155:
2144:
2133:
2129:
2118:
2090:
2085:
2066:
2062:
2058:
2054:
2050:
2042:
2035:
2031:
2027:
2023:
2016:
2012:
2008:
1981:
1900:
1891:
1868:
1825:
1812:
1799:
1786:
1781:
1780:
1768:
1767:
1761:
1758:is realized in
1757:
1753:
1749:
1743:
1737:
1693:
1680:
1667:
1654:
1649:
1648:
1633:
1619:
1604:
1568:, developed by
1486:
1485:
1463:
1461:
1457:
1453:
1445:
1443:
1439:
1431:
1425:
1415:
1411:
1407:
1401:
1391:
1379:
1334:
1321:
1308:
1295:
1290:
1289:
1273:
1267:
1261:
1259:
1255:
1251:
1243:
1241:
1237:
1225:
1221:
1215:
1208:
1196:
1194:Clinger's Model
1160:
1151:
1147:
1143:
1139:
1135:
1131:
1127:
1120:process calculi
1116:
1109:
1107:
1096:
1089:
1082:
1075:
1059:
1055:
1051:
1047:
1043:
1031:
1027:
1023:
1019:
1015:
1011:
1007:
1003:
1000:
995:
968:
953:
949:
943:
939:
935:
929:
925:
921:
892:
880:
864:
860:
853:
849:
845:
837:
833:
829:
821:
817:
814:
791:
787:
783:
779:
775:
771:
767:
752:
749:
740:
729:lambda calculus
717:
713:
709:
705:
701:
697:
693:
689:
685:
681:
674:
666:
660:
654:
648:
641:
635:
629:
622:
615:
609:
603:
597:
591:
585:
582:
576:
573:
567:
561:
555:
524:
477:
441:
378:
373:
372:
370:
366:
362:
360:
357:
353:
349:
341:
334:
328:
324:
313:
307:
278:
259:
222:
174:
169:
168:
161:
158:
152:
149:
145:
141:
134:
130:
126:
122:
118:
92:
62:
57:
51:
45:
39:under the name
25:
12:
11:
5:
2506:
2504:
2496:
2495:
2490:
2480:
2479:
2476:
2475:
2470:Pablo Noriega
2464:
2459:Will Clinger,
2457:
2450:
2440:
2433:
2426:
2408:
2397:
2383:
2368:
2358:
2348:
2335:
2328:
2318:
2305:
2298:
2287:Joseph E. Stoy
2284:
2279:Irene Greif.
2277:
2272:
2269:
2257:
2256:
2252:
2248:
2244:
2237:
2220:
2213:
2210:
2209:
2205:
2201:
2197:
2189:
2186:
2185:
2181:
2177:
2173:
2169:
2165:
2161:
2157:
2153:
2142:
2136:
2135:
2131:
2127:
2124:
2116:
2107:
2106:
2103:
2100:
2088:
2084:
2081:
2080:
2079:
2073:
2072:
2071:
2070:
2069:
2060:
2056:
2052:
2048:
2040:
2037:
2033:
2029:
2025:
2021:
2014:
2010:
1999:
1998:
1997:
1994:
1980:
1977:
1976:
1975:
1968:
1953:
1913:
1912:
1908:
1899:
1896:
1890:
1887:
1886:
1885:
1877:
1876:
1875:
1874:
1862:
1861:
1860:
1859:
1858:
1857:
1846:
1843:
1840:
1837:
1832:
1828:
1824:
1819:
1815:
1811:
1806:
1802:
1798:
1793:
1789:
1773:
1772:
1771:
1770:
1765:
1763:
1759:
1755:
1751:
1747:
1730:
1729:
1728:
1727:
1726:
1725:
1714:
1711:
1708:
1705:
1700:
1696:
1692:
1687:
1683:
1679:
1674:
1670:
1666:
1661:
1657:
1641:
1640:
1639:
1638:
1626:
1625:
1615:
1612:
1603:
1600:
1599:
1598:
1591:pending events
1586:
1585:
1580:
1579:
1574:
1573:
1561:
1560:
1556:
1555:
1546:
1545:
1544:
1543:
1532:
1529:
1526:
1523:
1520:
1517:
1514:
1511:
1508:
1505:
1502:
1499:
1496:
1493:
1480:
1479:
1472:
1469:
1459:
1455:
1451:
1441:
1437:
1390:
1387:
1386:
1385:
1375:
1374:
1369:
1368:
1367:
1366:
1355:
1352:
1349:
1346:
1341:
1337:
1333:
1328:
1324:
1320:
1315:
1311:
1307:
1302:
1298:
1284:
1283:
1257:
1253:
1249:
1239:
1235:
1207:
1204:
1195:
1192:
1159:
1156:
1149:
1148:<expression
1141:
1140:<expression
1133:
1129:
1128:<expression
1114:
1105:
1094:
1087:
1080:
1073:
1057:
1056:<expression
1049:
1048:<expression
1025:
1024:<expression
1017:
1016:<expression
1009:
1005:
1004:<expression
999:
996:
977:
967:then sends an
961:
960:
946:
932:
836:are each sent
796:
748:
745:
715:
714:<expression
707:
706:<expression
699:
695:
694:<expression
687:
683:
682:<expression
673:
670:
664:
652:
639:
632:
631:
627:
620:
613:
601:
589:
580:
571:
559:
552:
551:
540:
535:
529:
523:
517:
511:
508:
505:
502:
499:
496:
493:
490:
487:
484:
481:
474:
471:
468:
464:
460:
457:
452:
446:
438:
435:
432:
428:
424:
418:
412:
409:
406:
403:
400:
397:
394:
391:
388:
385:
382:
365:
356:
339:
332:
311:
304:
303:
292:
286:
281:
277:
270:
264:
256:
253:
250:
247:
244:
241:
238:
235:
232:
229:
226:
219:
216:
213:
209:
205:
199:
193:
190:
187:
184:
181:
178:
156:
147:
91:
88:
64:
63:
28:
26:
19:
13:
10:
9:
6:
4:
3:
2:
2505:
2494:
2491:
2489:
2486:
2485:
2483:
2473:
2469:
2466:Carl Hewitt
2465:
2462:
2458:
2455:
2452:David Park.
2451:
2448:
2445:
2441:
2438:
2434:
2431:
2427:
2424:
2420:
2416:
2412:
2409:
2406:
2402:
2398:
2395:
2392:
2388:
2384:
2381:
2378:
2377:
2372:
2369:
2366:
2363:
2362:Power domains
2359:
2356:
2352:
2349:
2346:
2343:
2339:
2336:
2333:
2329:
2326:
2322:
2319:
2316:
2315:Prentice Hall
2313:
2309:
2306:
2303:
2299:
2296:
2292:
2288:
2285:
2282:
2278:
2275:
2274:
2270:
2268:
2264:
2262:
2261:TimedDiagrams
2242:
2241:
2240:
2235:
2231:
2229:
2224:
2217:
2195:
2194:
2193:
2151:
2148:
2147:
2146:
2140:
2125:
2122:
2121:
2120:
2119:is a mapping
2113:
2110:
2104:
2101:
2098:
2097:
2096:
2094:
2082:
2077:
2074:
2065:
2064:
2063:| k ≤i} then
2046:
2045:TimedDiagrams
2039:E.g., If ∀i d
2038:
2020:
2007:
2006:
2004:
2000:
1995:
1992:
1988:
1987:
1985:
1983:
1982:
1979:Power domains
1978:
1973:
1972:TimedDiagrams
1969:
1966:
1965:TimedDiagrams
1962:
1961:TimedDiagrams
1958:
1957:TimedDiagrams
1954:
1951:
1947:
1946:TimedDiagrams
1943:
1942:
1941:
1939:
1938:TimedDiagrams
1936:
1932:
1930:
1929:TimedDiagrams
1926:
1925:TimedDiagrams
1922:
1921:TimedDiagrams
1918:
1917:TimedDiagrams
1909:
1906:
1905:
1904:
1897:
1895:
1888:
1883:
1879:
1878:
1871:
1866:
1865:
1864:
1863:
1844:
1841:
1838:
1835:
1830:
1826:
1822:
1817:
1813:
1809:
1804:
1800:
1796:
1791:
1787:
1779:
1778:
1777:
1776:
1775:
1774:
1740:
1734:
1733:
1732:
1731:
1712:
1709:
1706:
1703:
1698:
1694:
1690:
1685:
1681:
1677:
1672:
1668:
1664:
1659:
1655:
1647:
1646:
1645:
1644:
1643:
1642:
1636:
1630:
1629:
1628:
1627:
1622:
1616:
1613:
1609:
1608:
1607:
1601:
1596:
1592:
1588:
1587:
1582:
1581:
1576:
1575:
1571:
1567:
1563:
1562:
1558:
1557:
1552:
1551:power domains
1548:
1547:
1524:
1521:
1518:
1512:
1509:
1503:
1497:
1494:
1491:
1484:
1483:
1482:
1481:
1477:
1473:
1470:
1466:
1448:
1434:
1428:
1423:
1422:
1421:
1418:
1404:
1399:
1398:Power domains
1394:
1388:
1382:
1377:
1376:
1371:
1370:
1353:
1350:
1347:
1344:
1339:
1335:
1331:
1326:
1322:
1318:
1313:
1309:
1305:
1300:
1296:
1288:
1287:
1286:
1285:
1281:
1276:
1270:
1264:
1246:
1233:
1228:
1218:
1213:
1212:
1211:
1205:
1203:
1201:
1191:
1189:
1185:
1181:
1177:
1173:
1169:
1165:
1157:
1155:
1125:
1121:
1117:
1108:
1101:
1097:
1090:
1083:
1076:
1069:
1065:
1041:
1037:
997:
994:rightSubTree
993:
989:
985:
981:
976:
974:
966:
959:
947:
933:
919:
918:
917:
915:
911:
908:
903:
901:
898:
891:. The Actor
890:
886:
878:
874:
870:
857:
843:
827:
813:rightSubTree
812:
808:
804:
800:
795:
764:
762:
758:
746:
744:
738:
734:
730:
726:
721:
679:
671:
669:
663:
657:
651:
646:
638:
626:
619:
612:
608:
607:
606:
600:
594:
588:
579:
570:
564:
558:
533:
466:
458:
450:
430:
347:
346:
345:
338:
331:
322:
318:
310:
268:
211:
203:
167:
166:
165:
155:
138:
129:" mean that "
116:
115:partial order
111:
109:
108:domain theory
105:
101:
97:
89:
87:
85:
81:
80:domain theory
77:
76:
72:
56:
49:
44:
42:
38:
34:
29:This article
27:
23:
18:
17:
2471:
2460:
2453:
2443:
2436:
2429:
2418:
2404:
2401:C.A.R. Hoare
2390:
2387:Robin Milner
2374:
2371:C.A.R. Hoare
2361:
2354:
2344:
2331:
2324:
2311:
2301:
2290:
2280:
2265:
2260:
2258:
2233:
2232:
2227:
2225:
2218:
2211:
2187:
2149:
2138:
2137:
2114:
2111:
2108:
2086:
2075:
2044:
2018:
2002:
1990:
1971:
1964:
1960:
1956:
1945:
1937:
1934:
1933:
1928:
1924:
1920:
1916:
1914:
1903:conditions:
1901:
1892:
1869:
1738:
1634:
1620:
1605:
1595:finite delay
1594:
1590:
1565:
1464:
1446:
1432:
1426:
1416:
1402:
1395:
1392:
1380:
1274:
1268:
1262:
1244:
1226:
1216:
1209:
1200:Will Clinger
1197:
1179:
1161:
1112:
1103:
1099:
1092:
1085:
1078:
1071:
1067:
1063:
1046:messages to
1039:
1035:
1001:
991:
987:
983:
979:
972:
964:
962:
957:
940:rightSubTree
913:
910:
906:
904:
900:
899:the message
896:
888:
884:
876:
872:
858:
841:
830:<L>, 1
825:
815:
810:
806:
802:
798:
792:rightSubTree
782:, it return
776:rightSubTree
765:
760:
756:
750:
747:Environments
722:
675:
661:
658:
649:
644:
636:
633:
624:
617:
610:
598:
595:
593:will exist.
586:
577:
568:
565:
556:
553:
336:
329:
320:
316:
308:
305:
164:as follows:
153:
139:
112:
93:
69:
67:
58:}}
52:{{
30:
2411:Nancy Lynch
2351:Henry Baker
2342:Henry Baker
2338:Carl Hewitt
2247:Progression
2226:Define the
2200:Progression
2176:Progression
2141:Progression
2126:Progression
2123:Power→Power
1570:Irene Greif
1454:means that
1389:Denotations
1232:Denotations
1124:Actor model
1098:, it sends
1042:, it sends
956:message to
926:leftSubTree
895:then sends
885:environment
820:is sent an
790:it returns
784:leftSubTree
772:leftSubTree
725:Actor model
662:progression
650:progression
645:fixed point
611:progression
599:progression
578:progression
557:progression
337:progression
330:progression
309:progression
154:progression
75:Actor model
2482:Categories
2271:References
1476:ω-complete
1280:ω-complete
1172:concurrent
1168:imperative
1164:functional
1102:the value
1066:and sends
788:"getRight"
2295:MIT Press
2091:e’} (see
2089:1-message
1836:≤
1823:≤
1810:≤
1797:≤
1704:≤
1691:≤
1678:≤
1665:≤
1522:×
1501:→
1495:≈
1345:≤
1332:≤
1319:≤
1306:≤
881:<L>
861:<L>
859:However,
780:"getLeft"
768:<L>
473:∞
470:→
437:∞
434:→
315:would be
280:⊥
218:∞
215:→
204:≡
55:wikibooks
48:rewritten
37:Wikibooks
31:has been
2425:. 1979.
2367:. 1978.
2317:. 1976.
2139:Theorem:
2076:Theorem:
2005:. I.e.,
1935:Theorem:
1870:Diagrams
1742:,
1739:Diagrams
1635:Diagrams
1621:Diagrams
1447:Diagrams
1427:Diagrams
1381:Diagrams
1373:pending.
1275:Diagrams
1269:Diagrams
1263:Diagrams
1245:Diagrams
1220:,
1217:Diagrams
1122:and the
1077:. When
317:monotone
33:imported
2212:where ⊥
2152:if ∀i M
2134:Flow(d)
2130:(M) ≡ U
2067:{{{1}}}
2009:(∀i∈ω M
1278:is not
1188:futures
988:else if
869:closure
807:else if
371:, then
327:then
98:. The
96:domains
73:of the
2472:et al.
1252:means
1184:delays
954:Lookup
950:Lookup
936:Lookup
922:Lookup
887:) for
879:) for
753:Lookup
637:Denote
625:Denote
618:Denote
587:Denote
569:Denote
323:, if
84:Actors
2449:1980.
2447:ICALP
2172:) = ⊔
2150:I.e.,
2055:and M
2047:and d
1991:i.e.,
1944:If D⊆
1611:case.
1176:logic
905:When
643:is a
605:that
100:Actor
2413:and
2394:JACM
2380:CACM
2340:and
2059:= {d
2017:) ⇒
1911:Law.
1750:and
1440:and
1186:and
1180:etc.
1152:>
1146:and
1144:>
1136:>
1091:and
1060:>
1054:and
1052:>
1044:Eval
1032:Eval
1028:>
1022:and
1020:>
1012:>
992:then
984:then
969:Eval
877:body
865:Eval
854:Eval
848:and
838:Eval
832:and
822:Eval
811:then
803:then
774:and
741:Eval
723:The
718:>
712:and
710:>
702:>
690:>
623:) =
348:If ∀
335:(x)≤
321:i.e.
121:and
82:for
68:The
2417:.
2389:.
2373:.
2310:.
2245:iεω
2198:iεω
2174:iεω
2166:iεω
2158:i+1
2132:dεM
2053:i+1
2030:i∈ω
2028:⊆ ⊔
2022:i∈ω
2015:i+1
1752:x≠y
1748:x≤y
1614:...
1564:In
1471:...
1452:x≤y
1444:of
1250:x≤y
647:of
463:lim
427:lim
352:∈ω
342:(y)
325:x≤y
208:lim
137:".
127:x≤y
104:cpo
35:to
2484::
2353:.
2293:.
2289:,
2251:(⊥
2204:(⊥
2180:(M
2164:(⊔
2156:⊆M
2051:≤d
2013:≤M
1450:,
1400::
1248:,
1190:.
1178:,
1174:,
1170:,
1166:,
1154:.
980:if
902:.
799:if
794:.
763:.
720:.
668:.
656:.
369:+1
361:≤
319:,
2255:)
2253:S
2249:S
2243:⊔
2221:S
2214:S
2208:)
2206:S
2202:S
2196:⊔
2190:S
2184:)
2182:i
2178:S
2170:i
2168:M
2162:S
2154:i
2143:S
2128:S
2117:S
2061:k
2057:i
2049:i
2043:ε
2041:i
2034:i
2032:M
2026:i
2024:M
2019:U
2011:i
2003:U
1952:.
1845:.
1842:.
1839:.
1831:3
1827:x
1818:2
1814:x
1805:1
1801:x
1792:0
1788:x
1766:i
1764:x
1760:y
1756:x
1744:≤
1713:.
1710:.
1707:.
1699:3
1695:x
1686:2
1682:x
1673:1
1669:x
1660:0
1656:x
1578:.
1531:]
1528:)
1525:R
1519:S
1516:(
1513:+
1510:S
1507:[
1504:P
1498:S
1492:R
1465:P
1460:y
1456:x
1442:y
1438:x
1433:P
1417:P
1412:D
1408:D
1403:P
1354:.
1351:.
1348:.
1340:3
1336:x
1327:2
1323:x
1314:1
1310:x
1301:0
1297:x
1258:y
1254:x
1242:∈
1240:y
1238:,
1236:x
1227:P
1222:≤
1150:2
1142:1
1134:2
1130:1
1115:2
1113:N
1110:+
1106:1
1104:N
1100:C
1095:2
1093:N
1088:1
1086:N
1081:0
1079:C
1074:0
1072:C
1068:C
1064:E
1058:2
1050:1
1040:C
1036:E
1026:2
1018:1
1010:2
1006:1
973:F
965:C
958:E
944:2
930:1
914:F
907:C
897:C
889:E
873:C
850:2
846:1
842:E
834:2
826:E
761:x
757:x
716:2
708:1
700:2
696:1
688:2
684:1
665:S
653:S
640:S
628:S
621:S
616:(
614:S
602:S
590:S
581:S
572:S
560:S
539:)
534:i
528:x
522:(
516:S
510:n
507:o
504:i
501:s
498:s
495:e
492:r
489:g
486:o
483:r
480:p
467:i
459:=
456:)
451:i
445:x
431:i
423:(
417:S
411:n
408:o
405:i
402:s
399:s
396:e
393:r
390:g
387:o
384:r
381:p
367:i
363:x
358:i
354:x
350:i
340:S
333:S
312:S
291:)
285:S
276:(
269:i
263:S
255:n
252:o
249:i
246:s
243:s
240:e
237:r
234:g
231:o
228:r
225:p
212:i
198:S
192:e
189:t
186:o
183:n
180:e
177:D
162:S
157:S
148:S
146:⊥
142:S
135:x
131:y
123:y
119:x
60:.
43:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
