6
$\begingroup$

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 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.

Improve this question
$\endgroup$
6
  • 4
    $\begingroup$ Yes. This is an acceptable way of specifying the semantics of a concurrent language. $\endgroup$
    – Dave Clarke
    Nov 5, 2012 at 13:07
  • $\begingroup$ Thanks. Can you point me to any other papers that use a similar approach to the one used in the F# paper? $\endgroup$
    – Alex
    Nov 5, 2012 at 13:15
  • 3
    $\begingroup$ Maybe you can update your question to ask this. At present the question is a yes-no one. $\endgroup$
    – Dave Clarke
    Nov 5, 2012 at 13:22
  • 5
    $\begingroup$ @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. $\endgroup$
    – Martin Berger
    Nov 5, 2012 at 13:45
  • $\begingroup$ @Dave Clarke I updated the question accordingly. $\endgroup$
    – Alex
    Nov 5, 2012 at 13:47

1 Answer 1

Reset to default
5
$\begingroup$

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 for related discussion, even though it is dealing with denotational rather than operational semantics.]

Improve this answer
$\endgroup$
8
  • $\begingroup$ 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) ... $\endgroup$
    – Martin Berger
    Nov 7, 2012 at 7:53
  • $\begingroup$ ... 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. $\endgroup$
    – Martin Berger
    Nov 7, 2012 at 7:53
  • 1
    $\begingroup$ @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. $\endgroup$
    – Uday Reddy
    Nov 7, 2012 at 14:48
  • $\begingroup$ 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. $\endgroup$
    – Martin Berger
    Nov 10, 2012 at 8:48
  • $\begingroup$ @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: "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. $\endgroup$
    – Uday Reddy
    Nov 11, 2012 at 20:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.