Previous Contents Next

3.8   Processes and expressions

process ::= full-name (   expr-list )
  | reply expr-list   [ to name ]
  | process |   process
  | expr ;   process
  | if expr then {   process }   [ else { process }]
  | decl in   process
  | { process }
expr ::= constant
  | full-name
  | full-name (   expr-list )
  | expr   full-infix-name   expr
  | expr ;   expr
  | spawn { process }
  | if expr then   expr   [ else expr ]
  | decl in   expr
  | ( expr )
expr-list ::= [ expr   { , expr } ]
decl ::= let process-decl
  | let expr-decl
  | loc agent-decl end
process-decl ::= join-pattern =   process   { and join-pattern =   process }
expr-decl ::= name   { , name } =   expr   { and name   { , name } =   expr }
agent-decl ::= agent   { and agent }
agent ::= ident   [ with process-decl ]   [ init process ]

The join-calculus possesses two base syntactic classes: processes and expressions. Processes form the skeleton of the join-calculus as a concurrent language, whereas expressions are more oriented toward functional programming. Both processes and expressions have a similar concrete syntax. Generally, they are discriminated by context: expressions are adequate in a context where a result is needed (such as arguments to message sending), whereas processes occur where some actions are to be performed.

A noticeable exception to the uniformity of concrete syntax is grouping, which is performed using curly braces {...} in the process case, and parenthesis (...) in the expression case. Such groupings can be used to disambiguate between processes and expressions. This trick is mandatory in the branches of the conditional construct if... then... else... , where curly braces {...} must be used in the process case.

The table below shows the relative precedences and associativity of operators and non-closed constructions. The constructions with higher precedence come first. For infix symbols, we write ``*...'' to mean ``any symbol starting with *''.

Construction or operator Associativity
!... #... $... ``.''... ~... left
^...@... right
*.../...%... left
+...-... left
<...>...=... --
|...&... left
if --
, left
; left
| right
let loc --

3.8.1   Basic constructs

Empty process

The empty process ``'' does nothing. Its presence can be emphasized by using process grouping { } .


Expressions consisting in a constant evaluate to this constant.

Names as expressions

When occurring alone in an expression context, names evaluate to the value they are bound to. Names bound to primitives are not allowed as expressions, and cause a runtime-error.

Message passing

The construct a (   expr 1 , ... ,   expr n ) denotes sending the results of the evaluations of expr 1 , ..., expr n on the port name (or the primitive) a . The expressions expr 1 , ..., expr n are evaluated in some unspecified order. In a process context, the name a must be asynchronous, whereas in an expression context, the name a must be synchronous. This constraint is checked when typing programs.

Note that channels are polyadic in their arguments. Polyadicity also occur at the result level: a synchronous channel takes n arguments and gives back m result, where n and m are any integer greater than or equal to zero.

Some synchronous binary channels can be invoked using infix notation: expr 1   full-infix-name   expr 2 is equivalent to full-infix-name (   expr 1 ,   expr 2 ).

Continuation invocation

The process reply expr 1, ... ,   expr n to   name executes by sending the message expr 1, ..., expr n on the continuation of name . As the continuation of name is an implicit argument to name , the reply ... to name construct may only occur in a process guarded by a join pattern that defines name (see below). In the current implementation, some additional restrictions apply to continuation usage (see section 7.4).

When name is the only channel being defined, the to name part can be omitted.

Channel definitions

New channels are defined by the process-decl construct. The simple declaration join-pattern =   process is both a definition for some fresh channel names and the specification of a synchronization pattern on these names (see section 3.7). This synchronization guards process .

Channel definitions are recursive definitions: if a is a port named defined by join-pattern above, then a may occur free inside process and its occurrence refers to the channel defined by the declaration join-pattern =   process .

The composite declaration join-pattern 1 =   process 1 and ... and   join-pattern n =   process n is a definition for all the names that the simple declarations join-pattern 1 =   process 1, ...join-pattern n =   process n define. The same channel name a may be defined by several simple declarations inside a composite declaration. Then, only one fresh channel a is defined and channel a takes part to several synchronizations.

Value binding

Any value in the language can be bound to a name by using the expr-decl construct. Evaluating a declaration x 1 , ... ,   x n =   expr is evaluating expr , which must return n values, which are then bound to x 1 , ..., x n. Basically, expr is a message sending construct on a synchronous channel that gives back n results. Such basic n-ary expressions can be combined by using other language constructs such as conditionals or local definitions.

Value bindings are non-recursive: in x 1 , ... ,   x n =   expr , the scope of x 1, ..., x n does not comprise expr . Similarily, the scope of the x ji in x 11 , ... ,   x n1 =   expr 1 and ... and   x 1m , ... ,   x pm =   expr m , does not comprise the expr j. Such composite value binding are evaluated in some unspecified order and all the names they bind must be different.

Location definitions

The simple location definition loc name with   process-decl init   process end executes by making a new location, which is bound to name , whose initial active channels are defined by process-decl , and whose initial active process is process . Note that both initial active channels definition and initial active process may be omitted.

The composite location definition agent 1 and ... and   agent n is the simultaneous definition of n locations. Such a declaration is recursive, that is the scope of the location and initial port names defined by agent 1, ...agent n comprises the whole composite definition.

Local definitions

The decl in   process and decl in   expr constructs bind values locally both inside processes and expressions.

They are evaluated by first evaluating decl , binding some new names, then evaluating expr or executing process in an environment extended by the new names defined in decl . In an expression context, the result of evaluating the decl in   expr construct is the result of evaluating expr .

3.8.2   Control structures


The expression expr 1 ;   expr 2 evaluates expr 1 first, then expr 2, and returns the value of expr 2. The process expr 1 ;   process 2 executes expr 1 first, then it executes process 2. The expression expr 1 must return an empty result. In fact, sequence is a shorthand for a zero-ary local value binding let = expr in ....

Concurrent execution

The process process 1 |   process 2 executes by concurrently executing process 1 and process 2. The expression spawn { process } launches the concurrent execution of process and returns an empty result.


The process if expr 1 then {   process 2 } else {   process 3 } executes process 2 if expr 1 evaluates to the boolean true, and process 3 if expr 1 evaluates to the boolean false. The else process 3 part can be omitted, in which case it defaults to else {}.

The expression if expr 1 then   expr 2 else   expr 3 evaluates to the value of expr 2 if expr 1 evaluates to the boolean true, and to the value of expr 3 if expr 1 evaluates to the boolean false. The else expr 3 part can be omitted, in which case it defaults to an expression that returns zero result.

3.8.3   Operators

Symbols from the class infix-symbols can appear in infix position (between two expressions). Infix symbols do not have a fixed meaning: they are simply interpreted as message sending on the channels corresponding to the symbols.

The table below lists the symbols defined in the initial environment and their initial meaning. (See the description of the standard library module sys in chapter 4 for more details). Their meaning may be changed at any time using let infix-op (   x 1 ,   x 2 ) = ...

Operator Initial meaning
+ Integer addition.
- Integer subtraction.
* Integer multiplication.
/ Integer division. Crashes the system if the second argument is zero. The result is unspecified if either argument is negative.
% Integer modulus. Crashes the system if the second argument is zero. The result is unspecified if either argument is negative.
^ String concatenation.
= Structural equality test.
<> Structural inequality test.
< Test ``less than''.
<= Test ``less than or equal''.
> Test ``greater than''.
>= Test ``greater than or equal''
|| Boolean disjunction
&& Boolean conjunction
not Boolean negation

Previous Contents Next