WOSlinker: tt fix

2018-07-29T21:48:16Z

tt fix

Pi Delport: extract from parent discussion

2009-10-22T23:14:00Z

extract from parent discussion

New page

(The following article extract was moved here from the [[Talk:Denotational semantics#Material in "Compositionality in Programming Language" removed by Sam Staton|parent discussion]]. —[[User:Piet Delport|Piet Delport]] ([[User talk:Piet Delport|talk]]) 2009-10-22 23:13)

==Material in "Compositionality in Programming Language" removed by Sam Staton==
An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example consider the expression "8 / 4". Compositionality in this case is to provide a meaning for "8 / 4" in terms of the meanings of "8", "4" and "/".

===Functional approach===
A functional approach to denotational semantics in is compositional because it is given as follows. We start by considering program fragments, i.e. programs with free variables. A ''typing context'' assigns a type to each free variable. For instance, in the expression (''x'' / ''y'') might be considered in a typing context (''x'':<tt>nat</tt>,''y'':<tt>nat</tt>). We now give a denotational semantics to program fragments, using the following scheme.
#We begin by describing the meaning of the types of our language: the meaning of each type must be a domain. We write 〚τ〛 for the domain denoting the type τ. For instance, the meaning of type <tt>nat</tt> should be the domain of natural numbers: 〚<tt>nat</tt>〛=ℕ⊥.
#From the meaning of types we derive a meaning for typing contexts. We set 〚 ''x''1:τ1,…, ''x''n:τn〛 = 〚 τ1〛× … ×〚τn〛. For instance, 〚''x'':<tt>nat</tt>,''y'':<tt>nat</tt>〛= ℕ⊥×ℕ⊥. As a special case, the meaning of the empty typing context, with no variables, is the domain with one element, denoted 1.
#Finally, we must give a meaning to each program-fragment-in-typing-context. Suppose that ''P'' is a program fragment of type σ, in typing context Γ, often written Γ⊢''P'':σ. Then the meaning of this program-in-typing-context must be a continuous function 〚Γ⊢''P'':σ〛:〚Γ〛→〚σ〛. For instance, 〚⊢8:<tt>nat</tt>〛:1→ℕ⊥ is the constantly "8" function, while 〚''x'':<tt>nat</tt>,''y'':<tt>nat</tt>⊢''x''/''y'':<tt>nat</tt>〛:ℕ⊥×ℕ⊥→ℕ⊥ is the function that divides two numbers.

Now, the meaning of the compound expression (8/4) is determined by composing the three functions 〚⊢8:<tt>nat</tt>〛:1→ℕ⊥, 〚⊢4:<tt>nat</tt>〛:1→ℕ⊥, and 〚''x'':<tt>nat</tt>,''y'':<tt>nat</tt>⊢''x''/''y'':<tt>nat</tt>〛:ℕ⊥×ℕ⊥→ℕ⊥.

There is nothing specific about domains and continuous functions here. One can work with a different [[category (mathematics)|category]] instead. For example, in [[game semantics]], the category of games has games as objects and strategies as morphisms: we can interpret types as games, and programs as strategies. For a simple language without recursion, we can make do with the [[Category of sets|category of sets and functions]]. For a language with side-effects, we can work in the [[Kleisli category]] for a monad. For a language with state, we can work in a [[functor category]].

===Problems with the functional approach to compostionality in programming languages===

Unfortunately, the above is not a general scheme for compositional denotational semantics that is adequate for modern software engineering. An initial difficulty comes with expressions like <tt>8/0</tt>. An inital approach was to define a special element of the domain to be an "error element" and have <tt>8/0<tt> denote the error element. However, the error element approach is unsatisfactory for software engineering. One problem is that it becomes necessary for programs to continually test for the error element. Another problem is that the error element approach does not automatically propagate exceptions higher if they are not caught.

An even more serious problem with the above functional approach is that it does not encompass communication and change. Consider the following program in [[Actor_model#ActorScript|ActorScrip]]t:

<tt>
:SimpleCell ≡
::''serializer''
:::contents
:::''implements'' Cell
::::Read< > → ''return'' contents
::::Write<newContents> → ''return also become''(contents=newContents)</tt>

What is the denotation of the expression "<tt>''return also become''(contents=newContents)</tt>" in the above program?

Scott and Strachey [1971] proposed that the semantics of programming languages be reduced to the semantics of the [[lambda calculus]] and thus inherit the [[Domain_theory#Motivation_and_intuition|denotational semantics of the lambda calculus]]. However, it turned out that general computation could not be implemented in the lambda calculus (see [[Indeterminacy in concurrent computation]]). Thus there arose the problem of how to provide modular denotational semantics for general programming languages. One solution to this problem is to use the <tt>Eval</tt> messages with an environment so that programs obtain their denotational semantics from the methods explained earlier in this article.

===General compositionality in programming languages===
The general approach to compositonality in programming languages solves the above problems using [[environments]] and [[Actor_model#Customers|customers]] as explained below.

====Environments====
Environments hold the bindings of identifiers. When an environment is sent a <tt>Lookup</tt> message for an identifier '''x''', it returns the latest (lexical) binding of '''x'''.

As an example of how this works consider the lambda expression <tt><L></tt> below which implements a tree data structure when supplied with parameters for a <tt>leftSubTree</tt> and <tt>rightSubTree</tt>. When such a tree is given a parameter message <tt>"getLeft"</tt>, it return <tt>leftSubTree</tt> and likewise when given the message <tt>"getRight"</tt> it returns <tt>rightSubTree</tt>.

λ(leftSubTree, rightSubTree)
λ(message)
''if'' (message == "getLeft") ''then'' leftSubTree
''else if'' (message == "getRight") ''then'' rightSubTree

Consider what happens when an expression of the form <tt>"(<L> 1 2)"</tt> is sent an <tt>Eval</tt> message with environment '''E'''. One semantics for application expressions such as this one is the following: <tt><L>, 1</tt> and <tt>2</tt> are each sent <tt>Eval</tt> messages with environment '''E'''. The integers <tt>1</tt> and <tt>2</tt> immediately reply to the <tt>Eval</tt> message with themselves.

However, <tt><L><tt> responds to the <tt>Eval</tt> message by creating a [[Closure (computer science)|closure]] '''C''' that has a ''body'' <tt><L></tt> and environment '''E'''. <tt>"(<L> 1 2)"</tt> then sends '''C''' the message '''[1 2]'''.

When '''C''' receives the message '''[1 2]''', it creates a new environment '''F''' which behaves as follows:
#When it receives a <tt>Lookup</tt> message for the identifier <tt>leftSubTree</tt>, it responds with <tt>1</tt>
#When it receives a <tt>Lookup</tt> message for the identifier <tt>rightSubTree</tt>, it responds with <tt>2</tt>
#When it receives a <tt>Lookup</tt> message for any other identifier, it forwards the <tt>Lookup</tt> message to '''E'''

'''C''' then sends an <tt>Eval</tt> message with environment '''F''' to the following:

λ(message)
''if'' (message == "getLeft") ''then'' leftSubTree
''else if'' (message == "getRight") ''then'' rightSubTree

====Arithmetic expressions====
For another example consider the expression "<tt><expression1> / <expression2></tt>" which has the subexpressions <tt><expression1></tt> and <tt><expression2></tt>. When the composite expression receives an <tt>Eval</tt> message with an environment '''E''' and a customer '''C''', it sends <tt>Eval</tt> messages to <tt><expression1></tt> and <tt><expression2></tt> with environment '''E''' and sends '''C''' a newly created '''C0'''. When '''C0''' has received back two values '''N1''' and '''N2''', it sends "'''/'''" the message ['''N1''' '''N2'''] with customer '''C''' to perform the division.

====Other programming language constructs====
The denotational compositional semantics presented above is very general and can be used for [[Functional programming|functional]], [[Imperative programming|imperative]], [[Concurrent programming language|concurrent]], [[Logic programming|logic]], ''etc.'' programs.<ref>Carl Hewitt. [http://arxiv.org/abs/0812.4852 Common sense for concurrency and strong paraconsistency using unstratified inference and reflection] Arxiv 0812.4852. 2008.</ref> For example it easily provides denotation semantics for constructs that are difficult to formalize using other approaches such as [[Delay (programming)|delays]] and [[Future (programming)|futures]].

{{reflist|2}}[[Special:Contributions/76.254.235.105|76.254.235.105]] ([[User talk:76.254.235.105|talk]]) 02:59, 16 September 2009 (UTC)

← Previous revision		Revision as of 21:48, 29 July 2018
Line 16:		Line 16:
	===Problems with the functional approach to compostionality in programming languages===		===Problems with the functional approach to compostionality in programming languages===

	Unfortunately, the above is not a general scheme for compositional denotational semantics that is adequate for modern software engineering. An initial difficulty comes with expressions like <tt>8/0</tt>. An inital approach was to define a special element of the domain to be an "error element" and have <tt>8/0<tt> denote the error element. However, the error element approach is unsatisfactory for software engineering. One problem is that it becomes necessary for programs to continually test for the error element. Another problem is that the error element approach does not automatically propagate exceptions higher if they are not caught.		Unfortunately, the above is not a general scheme for compositional denotational semantics that is adequate for modern software engineering. An initial difficulty comes with expressions like <tt>8/0</tt>. An inital approach was to define a special element of the domain to be an "error element" and have <tt>8/0</tt> denote the error element. However, the error element approach is unsatisfactory for software engineering. One problem is that it becomes necessary for programs to continually test for the error element. Another problem is that the error element approach does not automatically propagate exceptions higher if they are not caught.

	An even more serious problem with the above functional approach is that it does not encompass communication and change. Consider the following program in [[Actor_model#ActorScript\|ActorScrip]]t:		An even more serious problem with the above functional approach is that it does not encompass communication and change. Consider the following program in [[Actor_model#ActorScript\|ActorScrip]]t:
Line 26:		Line 26:
	:::''implements'' Cell		:::''implements'' Cell
	::::Read< > → ''return'' contents		::::Read< > → ''return'' contents
	::::Write<newContents> → ''return also become''(contents=newContents)</tt>		::::Write<newContents> → ''return also become''(contents=newContents)
			</tt>

	What is the denotation of the expression "<tt>''return also become''(contents=newContents)</tt>" in the above program?		What is the denotation of the expression "<tt>''return also become''(contents=newContents)</tt>" in the above program?
Line 47:		Line 48:
	Consider what happens when an expression of the form <tt>"(<L> 1 2)"</tt> is sent an <tt>Eval</tt> message with environment '''E'''. One semantics for application expressions such as this one is the following: <tt><L>, 1</tt> and <tt>2</tt> are each sent <tt>Eval</tt> messages with environment '''E'''. The integers <tt>1</tt> and <tt>2</tt> immediately reply to the <tt>Eval</tt> message with themselves.		Consider what happens when an expression of the form <tt>"(<L> 1 2)"</tt> is sent an <tt>Eval</tt> message with environment '''E'''. One semantics for application expressions such as this one is the following: <tt><L>, 1</tt> and <tt>2</tt> are each sent <tt>Eval</tt> messages with environment '''E'''. The integers <tt>1</tt> and <tt>2</tt> immediately reply to the <tt>Eval</tt> message with themselves.

	However, <tt><L><tt> responds to the <tt>Eval</tt> message by creating a [[Closure (computer science)\|closure]] '''C''' that has a ''body'' <tt><L></tt> and environment '''E'''. <tt>"(<L> 1 2)"</tt> then sends '''C''' the message '''[1 2]'''.		However, <tt><L></tt> responds to the <tt>Eval</tt> message by creating a [[Closure (computer science)\|closure]] '''C''' that has a ''body'' <tt><L></tt> and environment '''E'''. <tt>"(<L> 1 2)"</tt> then sends '''C''' the message '''[1 2]'''.

	When '''C''' receives the message '''[1 2]''', it creates a new environment '''F''' which behaves as follows:		When '''C''' receives the message '''[1 2]''', it creates a new environment '''F''' which behaves as follows:

Talk:Denotational semantics/Compositionality in Programming Language - Revision history

WOSlinker: tt fix

Pi Delport: extract from parent discussion