<p>Legally speaking, the term "calculus" is almost always used to describe a language, i.e., a piece of syntax, with added rules of calculation or reasoning.  Examples include the good old predicate calculus, lambda calculus, process calculi, various type theories and logics (e.g., Martin-Lof type theory and linear logic).  From a programming language point of view, a "calculus" is just a bare bones programming language, that we take to be fundamental in some way.</p>

<p>People with an engineering bent of mind often take calculi to be good enough for using as a foundation, and describe the "semantics" of other languages in terms of such calculi.  (Prominent examples of such people include Christopher Strachey, Robin Milner, and Tony Hoare to some extent.)  People with a logical/philosophical bent of mind regard such calculi as being inadequate on their own, and needing a proper "semantics".  (Prominent examples include Dana Scott, Gordon Plotkin, John Reynolds and again Tony Hoare to some extent.)  A true "semantics" then is expressed in terms of abstract <em>concepts</em>, rather than pieces of syntax.</p>

<p>From this point of view, the F# paper that you cite is doing the right thing by describing the semantics in terms of concepts.  It is indeed the preferred way of describing the semantics of programming languages (at least for those of us with a logical bent of mind).</p>

<p>[Additional note: See also the previous question <a href="https://cstheory.stackexchange.com/questions/3577/what-constitutes-denotational-semantics?rq=1">What constitutes denotational semantics</a> for related discussion, even though it is dealing with denotational rather than operational semantics.]</p>

CC BY-SA 3.0
2012-11-07T07:53:19.670Z
This explanation is misleading. The distinction between lowly "People
with an engineering bent of mind" and the higher-ranked "People with a
logical/philosophical bent of mind" is specious, as is the claim that
"true "semantics" [...] is expressed in terms of abstract concepts,
rather than pieces of syntax". After all these magical abstract
concepts ultimately also boil down to mere calculi (some extension of
first-order logic such as set theory, which themselves have no
abstract semantics, only rules of operation) ...
Martin Berger
CC BY-SA 3.0
2012-11-07T07:53:49.357Z
... For example the number
of people who have understood a specific computational feature by
looking at a compiler, or an operational semantics vastly exceeds the
number of people who have understood that feature by looking at a
domain-theoretic semantics. Just look at undergraduate curricula.

The point of formal modeling is (1) to omit some detail of the thing
being modeled, in order to bring our in more clarity some other
detail, and (2) to communicate some feature of the thing under
discussion.
Martin Berger
CC BY-SA 3.0
2012-11-07T14:48:44.180Z
@MartinBerger.  If you are trying to say that I implied Strachey, Milner and Hoare as being "lowly" in any way, I would say you are out of your mind!  By the way, everything I wrote is thoroughly researched, and I can back it up with direct quotes from the people that I mentioned.
Uday Reddy
CC BY-SA 3.0
2012-11-10T08:48:26.623Z
I'd be interested to learn where/how the statement "People with a logical/philosophical bent of mind regard such calculi as being inadequate" has been thoroughly researched.
Martin Berger
CC BY-SA 3.0
2012-11-11T20:50:48.613Z
@MartinBerger How is thoroughly researched?  By reading, obviously.  And paying close to attention to what they are saying.  Here is Scott in the [LCF paper](http://www.sciencedirect.com/science/article/pii/030439759390095B#): *"My point is that formalism without eventual interpretation is in the end useless.*" Or, Milner, in the original CCS book, Section 0.4 Evolution, traces the history of CCS.  First a *model* of interacting agents was constructed.  Second, it was refined and grew more *algebraic*.  Third a *language* (calculus) was derived from these insights.
Uday Reddy
CC BY-SA 3.0
2012-11-16T17:34:24.017Z
Neither Scott's nor Milner's quote provide evidence that "People
with a logical/philosophical bent of mind regard such calculi as being
inadequate".  Scott's claim, using the narrow interpretation of
interpretation that you seem to employ is clearly false, because 99.9%
of all the world's software is written in languages that don't have an
interpretation in this sense, see [here](http://langpop.com) for an
overview of such languages. Milner gives a linearised (presumably for
the sake of simplicity) narrative of the genesis of CCS. (Continued below.)
Martin Berger
CC BY-SA 3.0
2012-11-16T17:35:58.193Z
So Milner
took a detour, presumably because domain theoretic methods were on
everyone's mind at the time, following Scott's breakthrough.  He
didn't take that detour in the development of $\pi$ or bigraphs as far
as I'm aware. Moreover, CCS was developed in the context of existing
operational models for concurrency like Petri nets.
Martin Berger
CC BY-SA 3.0
2012-11-18T14:30:40.297Z
@MartinBerger. If you believe that Dana Scott is someone with a logical/philosophical bent of mind, he said exactly what I wrote, "such calculi are inadequate on their own."  Whether you agree with him or or not is an entirely separate issue.
Uday Reddy
CC BY-SA 3.0
2012-11-06T23:36:54.530Z
2012-11-07T21:24:20.763Z
2017-04-13T12:32:28.167Z
Uday Reddy
<p>I've seen that the preferred way to specify the semantics of a concurrent language is to use a process calculus (e.g. pi calculus, join calculus). But in the paper presenting the <a href="http://blogs.msdn.com/cfs-file.ashx/__key/communityserver-components-postattachments/00-10-07-89-59/async_2D00_padl.pdf" rel="nofollow">F# asynchronous programming model</a> the authors have a different approach: they first perform a CPS conversion to a core language, and then, define the semantics in terms of a transition system in which states are tuples of the form (A, Q, P), where A is the set of active computations, Q is the set of queued computations, and P is the set of pending computations--i.e. Waiting for an event. Each computation is of the form e@ctx, where ctx is a label corresponding to a synchronization context. Finally, they give transition rules for reduction (which uses the reduction rule of the core language), suspension of computations waiting on events, activation of computations (i.e. moving computations from Q to A), and event signaling.</p>

<p>I was wondering if this is an acceptable (i.e. accurate enough) way of specifying the semantics of a concurrent language.</p>

<p>EDIT: can anyone point me to papers that use a similar approach to the one taken in the F# paper?</p>

<p>Thanks.</p>

CC BY-SA 3.0
2012-11-05T13:07:13.317Z
Yes. This is an acceptable way of specifying the semantics of a concurrent language.
Dave Clarke
CC BY-SA 3.0
2012-11-05T13:15:02.447Z
Thanks. Can you point me to any other papers that use a similar approach to the one used in the F# paper?
Alex
CC BY-SA 3.0
2012-11-05T13:22:37.580Z
Maybe you can update your question to ask this. At present the question is a yes-no one.
Dave Clarke
CC BY-SA 3.0
2012-11-05T13:45:58.293Z
@Alex, whether that's accurate enough depends on what you are modelling. The point of a model is to leave out irrelevant detail and focus on some specific issue. E.g. most process algebraic approaches leave out timing, energy consumption, routing of messages or the stucture of non-determinism. This works well in some contexts. A second dimension of models is that models are a _language_ to communicate ideas. Ideally you want to use a language that your target audience already understands, or is close to something they understand. Use whatever works in your social and technological context.
Martin Berger
CC BY-SA 3.0
2012-11-05T13:47:42.260Z
@Dave Clarke I updated the question accordingly.
Alex
CC BY-SA 3.0
2012-11-05T13:52:08.753Z
@Martin Berger, your comment is very insightful. Thanks.
Alex
<reference-request><pl.programming-languages><semantics><concurrency><process-algebra>
Semantics of concurrent languages
Alex
# Semantics of concurrent languages

(Asked by: username_0 on 2012-11-05)

I've seen that the preferred way to specify the semantics of a concurrent language is to use a process calculus (e.g. pi calculus, join calculus). But in the paper presenting the [F# asynchronous programming model](http://blogs.msdn.com/cfs-file.ashx/__key/communityserver-components-postattachments/00-10-07-89-59/async_2D00_padl.pdf) the authors have a different approach: they first perform a CPS conversion to a core language, and then, define the semantics in terms of a transition system in which states are tuples of the form (A, Q, P), where A is the set of active computations, Q is the set of queued computations, and P is the set of pending computations--i.e. Waiting for an event. Each computation is of the form e@ctx, where ctx is a label corresponding to a synchronization context. Finally, they give transition rules for reduction (which uses the reduction rule of the core language), suspension of computations waiting on events, activation of computations (i.e. moving computations from Q to A), and event signaling.

I was wondering if this is an acceptable (i.e. accurate enough) way of specifying the semantics of a concurrent language.

EDIT: can anyone point me to papers that use a similar approach to the one taken in the F# paper?

Thanks.

**Tags:** reference-request, pl.programming-languages, semantics, concurrency, process-algebra

> **Comments:**
> **username_1**: Yes. This is an acceptable way of specifying the semantics of a concurrent language.  
> **username_0**: Thanks. Can you point me to any other papers that use a similar approach to the one used in the F# paper?  
> **username_1**: Maybe you can update your question to ask this. At present the question is a yes-no one.  
> **username_2**: @username_0, whether that's accurate enough depends on what you are modelling. The point of a model is to leave out irrelevant detail and focus on some specific issue. E.g. most process algebraic approaches leave out timing, energy consumption, routing of messages or the stucture of non-determinism. This works well in some contexts. A second dimension of models is that models are a _language_ to communicate ideas. Ideally you want to use a language that your target audience already understands, or is close to something they understand. Use whatever works in your social and technological context.  
> **username_0**: @username_1 I updated the question accordingly.  
> **username_0**: @username_2, your comment is very insightful. Thanks.  

---

## 1 answers

### Answer by username_3 on 2012-11-06. Score: 5

Legally speaking, the term "calculus" is almost always used to describe a language, i.e., a piece of syntax, with added rules of calculation or reasoning. Examples include the good old predicate calculus, lambda calculus, process calculi, various type theories and logics (e.g., Martin-Lof type theory and linear logic). From a programming language point of view, a "calculus" is just a bare bones programming language, that we take to be fundamental in some way.

People with an engineering bent of mind often take calculi to be good enough for using as a foundation, and describe the "semantics" of other languages in terms of such calculi. (Prominent examples of such people include Christopher Strachey, Robin Milner, and Tony Hoare to some extent.) People with a logical/philosophical bent of mind regard such calculi as being inadequate on their own, and needing a proper "semantics". (Prominent examples include Dana Scott, Gordon Plotkin, John Reynolds and again Tony Hoare to some extent.) A true "semantics" then is expressed in terms of abstract *concepts*, rather than pieces of syntax.

From this point of view, the F# paper that you cite is doing the right thing by describing the semantics in terms of concepts. It is indeed the preferred way of describing the semantics of programming languages (at least for those of us with a logical bent of mind).

[Additional note: See also the previous question [What constitutes denotational semantics](https://cstheory.stackexchange.com/questions/3577/what-constitutes-denotational-semantics?rq=1) for related discussion, even though it is dealing with denotational rather than operational semantics.]

> **Comments:**
> **username_2**: This explanation is misleading. The distinction between lowly "People with an engineering bent of mind" and the higher-ranked "People with a logical/philosophical bent of mind" is specious, as is the claim that "true "semantics" [...] is expressed in terms of abstract concepts, rather than pieces of syntax". After all these magical abstract concepts ultimately also boil down to mere calculi (some extension of first-order logic such as set theory, which themselves have no abstract semantics, only rules of operation) ...  
> **username_2**: ... For example the number of people who have understood a specific computational feature by looking at a compiler, or an operational semantics vastly exceeds the number of people who have understood that feature by looking at a domain-theoretic semantics. Just look at undergraduate curricula.  The point of formal modeling is (1) to omit some detail of the thing being modeled, in order to bring our in more clarity some other detail, and (2) to communicate some feature of the thing under discussion.  
> **username_3**: @MartinBerger.  If you are trying to say that I implied Strachey, Milner and Hoare as being "lowly" in any way, I would say you are out of your mind!  By the way, everything I wrote is thoroughly researched, and I can back it up with direct quotes from the people that I mentioned.  
> **username_2**: I'd be interested to learn where/how the statement "People with a logical/philosophical bent of mind regard such calculi as being inadequate" has been thoroughly researched.  
> **username_3**: @MartinBerger How is thoroughly researched?  By reading, obviously.  And paying close to attention to what they are saying.  Here is Scott in the [LCF paper](http://www.sciencedirect.com/science/article/pii/030439759390095B#): *"My point is that formalism without eventual interpretation is in the end useless.*" Or, Milner, in the original CCS book, Section 0.4 Evolution, traces the history of CCS.  First a *model* of interacting agents was constructed.  Second, it was refined and grew more *algebraic*.  Third a *language* (calculus) was derived from these insights.  
> **username_2**: Neither Scott's nor Milner's quote provide evidence that "People with a logical/philosophical bent of mind regard such calculi as being inadequate".  Scott's claim, using the narrow interpretation of interpretation that you seem to employ is clearly false, because 99.9% of all the world's software is written in languages that don't have an interpretation in this sense, see [here](http://langpop.com) for an overview of such languages. Milner gives a linearised (presumably for the sake of simplicity) narrative of the genesis of CCS. (Continued below.)  
> **username_2**: So Milner took a detour, presumably because domain theoretic methods were on everyone's mind at the time, following Scott's breakthrough.  He didn't take that detour in the development of $\pi$ or bigraphs as far as I'm aware. Moreover, CCS was developed in the context of existing operational models for concurrency like Petri nets.  
> **username_3**: @MartinBerger. If you believe that Dana Scott is someone with a logical/philosophical bent of mind, he said exactly what I wrote, "such calculi are inadequate on their own."  Whether you agree with him or or not is an entirely separate issue.  

---

