{"history":[],"article":{"id":"7adf248c-d337-4f74-968b-d908e78698f0","title":"Denotational semantics of the Actor model","slug":"denotational-semantics-of-the-actor-model","content":":::summary\n:::\n\n# \nThe **[denotational semantics](https://bliptext.com/articles/denotational-semantics) of the [Actor model](https://bliptext.com/articles/actor-model)** is the subject of denotational [domain theory](https://bliptext.com/articles/domain-theory) for [Actors](https://bliptext.com/articles/actor-model).\nThe historical development of this subject is recounted in [Hewitt 2008b].\n\n# Actor fixed point semantics\nThe denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do.\nCollections of such objects are called [domains](https://bliptext.com/articles/domain-theory).\nThe [Actor](https://bliptext.com/articles/actor-model) uses the domain of event diagram scenarios.\nIt is usual to assume some properties of the domain, such as the existence of limits of chains (see [cpo](https://bliptext.com/articles/complete-partial-order)) and a bottom element.\nVarious additional properties are often reasonable and helpful: the article on [domain theory](https://bliptext.com/articles/domain-theory) has more details.\nA domain is typically a [partial order](https://bliptext.com/articles/partial-order), which can be understood as an order of definedness.\nFor instance, given event diagram scenarios x and y, one might let \"x≤y\" mean that \"y extends the computations x\".\nThe mathematical denotation for a system S is found by constructing increasingly better approximations from an initial empty denotation called ⊥S using some denotation approximating function progressionS to construct a denotation (meaning ) for S as follows:\nIt would be expected that progressionS would be monotone, i.e., if x≤y then progressionS(x)≤progressionS(y).\nMore generally, we would expect that\nThis last stated property of progressionS is called ω-continuity.\nA central question of denotational semantics is to characterize when it is possible to create denotations (meanings) according to the equation for DenoteS.\nA fundamental theorem of computational domain theory is that if progressionS is ω-continuous then DenoteS will exist.\nIt follows from the ω-continuity of progressionS that\nThe above equation motivates the terminology that DenoteS is a fixed point of progressionS.\nFurthermore, this fixed point is least among all fixed points of progressionS.\n\n# Compositionality in programming languages\nAn important aspect of [denotational semantics](https://bliptext.com/articles/denotational-semantics) of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts.\nFor example, consider the expression \" + \".\nCompositionality in this case is to provide a meaning for \" + \" in terms of the meanings of and .\nThe [Actor model](https://bliptext.com/articles/actor-model) provides a modern and very general way the compositionality of programs can be analyzed.\nScott and Strachey [1971] proposed that the semantics of programming languages be reduced to the semantics of the [lambda calculus](https://bliptext.com/articles/lambda-calculus) and thus inherit the denotational semantics of the [lambda calculus](https://bliptext.com/articles/lambda-calculus).\nHowever, it turned out that concurrent computation could not be implemented in the lambda calculus (see [Indeterminacy in concurrent computation](https://bliptext.com/articles/indeterminacy-in-concurrent-computation)).\nThus there arose the problem of how to provide modular denotational semantics for concurrent programming languages.\nOne solution to this problem is to use the Actor model of computation.\nIn Actor model, programs are Actors that are sent Eval 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 [2006]).\n\n## Environments\nEnvironments hold the bindings of identifiers.\nWhen an environment is sent a Lookup message with the address of an identifier ****x****, it returns the latest (le****x****ical) binding of ****x****.\nAs an example of how this works consider the lambda expression below which implements a tree data structure when supplied with parameters for a leftSubTree and rightSubTree.\nWhen such a tree is given a parameter message \"getLeft\", it return leftSubTree and likewise when given the message \"getRight\" it returns rightSubTree.\nλ(leftSubTree, rightSubTree)\nλ(message)\n**if** (message == \"getLeft\") **then** leftSubTree\n**else if** (message == \"getRight\") **then** rightSubTree\nConsider what happens when an expression of the form \"( 1 2)\" is sent an **E**val message with environment **E**.\nOne semantics for application expressions such as this one is the following: , 1 and 2 are each sent **E**val messages with environment **E**.\nThe integers 1 and 2 immediately reply to the Eval message with themselves.\nHowever, responds to the **E**val message by creating a [closure](https://bliptext.com/articles/closure-computer-science) Actor (process) **C** that has an address (called body) for and an address (called environment) for **E**.\nThe Actor \"( 1 2)\" then sends **C** the message **[1 2]**.\nWhen **C** receives the message **[1 2]**, it creates a new environment Actor **F** which behaves as follows:\nThe Actor (process) **C** then sends an Eval message with environment **F** to the following actor (process):\nλ(message)\n**if** (message == \"getLeft\") **then** leftSubTree\n**else if** (message == \"getRight\") **then** rightSubTree\n\n## Arithmetic expressions\nFor another example consider the Actor for the expression \" + \" which has addresses for two other actors (processes) and .\nWhen the composite expression Actor (process) receives an ****E****val message with addresses for an environment Actor ****E**** and a customer ****C****, it sends ****E****val messages to and with environment ****E**** and sends ****C**** a new Actor (process) ****C****0.\nWhen ****C**0** has received back two values ****N1**** and ****N2****, it sends **C** the value ****N1**** + ****N2****.\nIn this way, the denotational semantics for [process calculi](https://bliptext.com/articles/process-calculi) and the [Actor model](https://bliptext.com/articles/actor-model) provide a denotational semantics for \" + \" in terms of the semantics for and .\n\n## Other programming language constructs\nThe denotational compositional semantics presented above is very general and can be used for [functional](https://bliptext.com/articles/functional-programming), [imperative](https://bliptext.com/articles/imperative-programming), [concurrent](https://bliptext.com/articles/concurrent-programming-language), [logic](https://bliptext.com/articles/logic-programming), etc. programs (see [Hewitt 2008a]).\nFor example, it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as [delays](https://bliptext.com/articles/delay-programming) and [futures](https://bliptext.com/articles/future-programming).\n\n# Clinger's Model\nIn his doctoral dissertation, [Will Clinger](https://bliptext.com/articles/william-clinger-computer-scientist) developed the first denotation semantics for the Actor model.\n\n## The domain of Actor computations\nClinger [1981] explained the domain of Actor computations as follows:\n\n## Denotations\nIn his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows:\nFrom the article on [Power domains](https://bliptext.com/articles/power-domains): P[D] is the collection of downward-closed subsets of domain D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions.\n\n## Sequential computations form an ω-complete subdomain of the domain of Actor computations\nIn his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:\n\n# The Timed Diagrams Model\nHewitt [2006b] published a new denotational semantics for Actors based on Timed Diagrams.\nThe Timed Diagrams model stands in contrast to Clinger\n[1981] which constructed an ω-complete power domain from an underlying incomplete\ndiagrammatic domain, which did not include time.\nThe advantage of the domain\nTimed Diagrams model is that it is physically motivated and the resulting\ncomputations have the desired property of ω-completeness (therefore unbounded nondeterminism) which provides guarantee of service.\n\n## Domain of Timed Actor Computations\nTimed Diagrams denotational semantics constructs an ω-complete computational\ndomain for Actor computations.\nIn the domain, for each event\nin an Actor computation, there is a delivery time which represents the time at which\nthe message is delivered such that each delivery time satisfies the following conditions:\nThe Actor event timed diagrams form a partially ordered set <**TimedDiagrams**, ≤>.\nThe diagrams are partial computation histories representing \"snapshots\" (relative to some frame of reference) of a computation on its way to being completed.\nFor\nd1, d2ε****TimedDiagrams****, d1≤d2 means d1 is a stage the computation could go through on its way to d2 The completed elements of ****TimedDiagrams**** represent computations that have\nterminated and nonterminating computations that have become infinite.\nThe completed\nelements may be characterized abstractly as the maximal elements of **TimedDiagrams**.\nConcretely, the completed elements are those having no pending events.\nTheorem: **TimedDiagrams** is an ω-complete domain of Actor computations i.e.,\n\n## Power domains\n\n## Concurrency Representation Theorem\nAn Actor computation can progress in many ways.\nLet d be a diagram with next scheduled event e and\nX ≡ {e’ | e ─≈→1-message e’} (see [Actor model theory](https://bliptext.com/articles/actor-model-theory)),\nFlow(d) is defined to be the set of all timed diagrams with d and extensions of d by X such that\n(Recall that δ is the minimum amount of time to deliver a message.)\nFlow(d) ≡ {d} if d is complete.\nLet S be an Actor system, ProgressionS is a mapping\nTheorem: ProgressionS is ω-continuous.\nFurthermore, the least fixed point of ProgressionS is given by the Concurrency Representation Theorem as follows:\nwhere ⊥S is the initial configuration of S.\nThe denotation DenoteS of an Actor system S is the set of all computations of S.\nDefine the time abstraction of a timed diagram to be the diagram with the time annotations\nremoved.\nRepresentation Theorem: The denotation Denote S of an Actor system S is the\ntime abstraction of\nUsing the domain **TimedDiagrams**, which is ω-complete, is important because it provides for the direct expression of the above representation theorem for the denotations\nof Actor systems by directly constructing a minimal fixed point.\nThe 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.","current_revision":null,"created_by":"kACnuQmH5k9Nr5VNVEpVeg7XpvUmMctD","created_at":"2025-01-26T07:01:32.578Z","updated_at":"2025-01-26T07:01:32.578Z","search_vector":"'actor':5 'denot':1 'model':6 'semant':2","search_content":" \n \n\n# \nThe **[denotational semantics](https://bliptext.com/articles/denotational-semantics) of the [Actor model](https://bliptext.com/articles/actor-model)** is the subject of denotational [domain theory](https://bliptext.com/articles/domain-theory) for [Actors](https://bliptext.com/articles/actor-model).\nThe historical development of this subject is recounted in [Hewitt 2008b].\n\n# Actor fixed point semantics\nThe denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do.\nCollections of such objects are called [domains](https://bliptext.com/articles/domain-theory).\nThe [Actor](https://bliptext.com/articles/actor-model) uses the domain of event diagram scenarios.\nIt is usual to assume some properties of the domain, such as the existence of limits of chains (see [cpo](https://bliptext.com/articles/complete-partial-order)) and a bottom element.\nVarious additional properties are often reasonable and helpful: the article on [domain theory](https://bliptext.com/articles/domain-theory) has more details.\nA domain is typically a [partial order](https://bliptext.com/articles/partial-order), which can be understood as an order of definedness.\nFor instance, given event diagram scenarios x and y, one might let \"x≤y\" mean that \"y extends the computations x\".\nThe mathematical denotation for a system S is found by constructing increasingly better approximations from an initial empty denotation called ⊥S using some denotation approximating function progressionS to construct a denotation (meaning ) for S as follows:\nIt would be expected that progressionS would be monotone, i.e., if x≤y then progressionS(x)≤progressionS(y).\nMore generally, we would expect that\nThis last stated property of progressionS is called ω-continuity.\nA central question of denotational semantics is to characterize when it is possible to create denotations (meanings) according to the equation for DenoteS.\nA fundamental theorem of computational domain theory is that if progressionS is ω-continuous then DenoteS will exist.\nIt follows from the ω-continuity of progressionS that\nThe above equation motivates the terminology that DenoteS is a fixed point of progressionS.\nFurthermore, this fixed point is least among all fixed points of progressionS.\n\n# Compositionality in programming languages\nAn important aspect of [denotational semantics](https://bliptext.com/articles/denotational-semantics) of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts.\nFor example, consider the expression \" + \".\nCompositionality in this case is to provide a meaning for \" + \" in terms of the meanings of and .\nThe [Actor model](https://bliptext.com/articles/actor-model) provides a modern and very general way the compositionality of programs can be analyzed.\nScott and Strachey [1971] proposed that the semantics of programming languages be reduced to the semantics of the [lambda calculus](https://bliptext.com/articles/lambda-calculus) and thus inherit the denotational semantics of the [lambda calculus](https://bliptext.com/articles/lambda-calculus).\nHowever, it turned out that concurrent computation could not be implemented in the lambda calculus (see [Indeterminacy in concurrent computation](https://bliptext.com/articles/indeterminacy-in-concurrent-computation)).\nThus there arose the problem of how to provide modular denotational semantics for concurrent programming languages.\nOne solution to this problem is to use the Actor model of computation.\nIn Actor model, programs are Actors that are sent Eval 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 [2006]).\n\n## Environments\nEnvironments hold the bindings of identifiers.\nWhen an environment is sent a Lookup message with the address of an identifier ****x****, it returns the latest (le****x****ical) binding of ****x****.\nAs an example of how this works consider the lambda expression below which implements a tree data structure when supplied with parameters for a leftSubTree and rightSubTree.\nWhen such a tree is given a parameter message \"getLeft\", it return leftSubTree and likewise when given the message \"getRight\" it returns rightSubTree.\nλ(leftSubTree, rightSubTree)\nλ(message)\n**if** (message == \"getLeft\") **then** leftSubTree\n**else if** (message == \"getRight\") **then** rightSubTree\nConsider what happens when an expression of the form \"( 1 2)\" is sent an **E**val message with environment **E**.\nOne semantics for application expressions such as this one is the following: , 1 and 2 are each sent **E**val messages with environment **E**.\nThe integers 1 and 2 immediately reply to the Eval message with themselves.\nHowever, responds to the **E**val message by creating a [closure](https://bliptext.com/articles/closure-computer-science) Actor (process) **C** that has an address (called body) for and an address (called environment) for **E**.\nThe Actor \"( 1 2)\" then sends **C** the message **[1 2]**.\nWhen **C** receives the message **[1 2]**, it creates a new environment Actor **F** which behaves as follows:\nThe Actor (process) **C** then sends an Eval message with environment **F** to the following actor (process):\nλ(message)\n**if** (message == \"getLeft\") **then** leftSubTree\n**else if** (message == \"getRight\") **then** rightSubTree\n\n## Arithmetic expressions\nFor another example consider the Actor for the expression \" + \" which has addresses for two other actors (processes) and .\nWhen the composite expression Actor (process) receives an ****E****val message with addresses for an environment Actor ****E**** and a customer ****C****, it sends ****E****val messages to and with environment ****E**** and sends ****C**** a new Actor (process) ****C****0.\nWhen ****C**0** has received back two values ****N1**** and ****N2****, it sends **C** the value ****N1**** + ****N2****.\nIn this way, the denotational semantics for [process calculi](https://bliptext.com/articles/process-calculi) and the [Actor model](https://bliptext.com/articles/actor-model) provide a denotational semantics for \" + \" in terms of the semantics for and .\n\n## Other programming language constructs\nThe denotational compositional semantics presented above is very general and can be used for [functional](https://bliptext.com/articles/functional-programming), [imperative](https://bliptext.com/articles/imperative-programming), [concurrent](https://bliptext.com/articles/concurrent-programming-language), [logic](https://bliptext.com/articles/logic-programming), etc. programs (see [Hewitt 2008a]).\nFor example, it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as [delays](https://bliptext.com/articles/delay-programming) and [futures](https://bliptext.com/articles/future-programming).\n\n# Clinger's Model\nIn his doctoral dissertation, [Will Clinger](https://bliptext.com/articles/william-clinger-computer-scientist) developed the first denotation semantics for the Actor model.\n\n## The domain of Actor computations\nClinger [1981] explained the domain of Actor computations as follows:\n\n## Denotations\nIn his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows:\nFrom the article on [Power domains](https://bliptext.com/articles/power-domains): P[D] is the collection of downward-closed subsets of domain D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions.\n\n## Sequential computations form an ω-complete subdomain of the domain of Actor computations\nIn his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:\n\n# The Timed Diagrams Model\nHewitt [2006b] published a new denotational semantics for Actors based on Timed Diagrams.\nThe Timed Diagrams model stands in contrast to Clinger\n[1981] which constructed an ω-complete power domain from an underlying incomplete\ndiagrammatic domain, which did not include time.\nThe advantage of the domain\nTimed Diagrams model is that it is physically motivated and the resulting\ncomputations have the desired property of ω-completeness (therefore unbounded nondeterminism) which provides guarantee of service.\n\n## Domain of Timed Actor Computations\nTimed Diagrams denotational semantics constructs an ω-complete computational\ndomain for Actor computations.\nIn the domain, for each event\nin an Actor computation, there is a delivery time which represents the time at which\nthe message is delivered such that each delivery time satisfies the following conditions:\nThe Actor event timed diagrams form a partially ordered set .\nThe diagrams are partial computation histories representing \"snapshots\" (relative to some frame of reference) of a computation on its way to being completed.\nFor\nd1, d2ε****TimedDiagrams****, d1≤d2 means d1 is a stage the computation could go through on its way to d2 The completed elements of ****TimedDiagrams**** represent computations that have\nterminated and nonterminating computations that have become infinite.\nThe completed\nelements may be characterized abstractly as the maximal elements of **TimedDiagrams**.\nConcretely, the completed elements are those having no pending events.\nTheorem: **TimedDiagrams** is an ω-complete domain of Actor computations i.e.,\n\n## Power domains\n\n## Concurrency Representation Theorem\nAn Actor computation can progress in many ways.\nLet d be a diagram with next scheduled event e and\nX ≡ {e’ | e ─≈→1-message e’} (see [Actor model theory](https://bliptext.com/articles/actor-model-theory)),\nFlow(d) is defined to be the set of all timed diagrams with d and extensions of d by X such that\n(Recall that δ is the minimum amount of time to deliver a message.)\nFlow(d) ≡ {d} if d is complete.\nLet S be an Actor system, ProgressionS is a mapping\nTheorem: ProgressionS is ω-continuous.\nFurthermore, the least fixed point of ProgressionS is given by the Concurrency Representation Theorem as follows:\nwhere ⊥S is the initial configuration of S.\nThe denotation DenoteS of an Actor system S is the set of all computations of S.\nDefine the time abstraction of a timed diagram to be the diagram with the time annotations\nremoved.\nRepresentation Theorem: The denotation Denote S of an Actor system S is the\ntime abstraction of\nUsing the domain **TimedDiagrams**, which is ω-complete, is important because it provides for the direct expression of the above representation theorem for the denotations\nof Actor systems by directly constructing a minimal fixed point.\nThe 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.","revisionCount":0},"hasMore":false,"nextCursor":null}

History