PFL / λ–CCS

The following parallel functional language is based on PFL with the syntax and semantics generalised somewhat. (NB. This is a small experimental system to test the semantics of the language.)

<Exp> ::= <ident> | (<Exp>) | <Exp> <Exp>
| λ <ident> . <Exp>   -- abstraction (function exp, LambdaExp)
| let [rec] <Decs> in <Exp>
| if <Exp> then <Exp> else <Exp>
| <unOp> <Exp>
| <Exp> <binOp> <Exp>
| chan   -- return a new Channel
| stop

<Dec> ::= <ident> = <Exp>
<Decs> ::= <Dec>+

<unOp> ::= + | - | not | null | hd | tl   -- as usual
| ?   -- input operator, e.g., ?c, input from Channel c

<binOp> ::= + | - | ... = | != | ...   -- as usual in lala and...
| '||' | '|'   -- parallel & choice Processes
| '->'   -- "and then", e.g., c!7->p
| '!'   -- output operator, e.g., (if b then c1 else c2)!7

increasing priority: ||, |, ->, ?, !, {+,-}, {*,/}, ..., application, prefixOp{+,-,not,null,hd,tl,?}
right associative: ||, |, ->

(NB. '||' not allowed below '|')
-- Syntax of Expressions in PFL / λ-CCS --

Note, "->" can be read as carry out an action "and then" do the following process, "||" as run two processes in parallel, "|" as carry out just one of two processes.

An Expression is evaluated to produce a Value. Channels, input- and output-Actions and Processes are all first-class Values. To carry out an input Action is to get a Value from a Channel; binding a name to that Value and using it are matters for the following Process, after the '->', hence '?c->λx.f(x)'.
It is convenient to make '?' prefix, e.g., ?c, given that we put the "into variable" x after the '->' as in ?c->λx.f(x).

Value = Bool + Int + Char + Function
+ Channel
+ opAction
+ ipAction
+ Process

Environment = ident → Value   -- maps idents to Values

ipAction = [Channel]   -- input a Value from the Channel
opAction = [Channel, Value]   -- output the Value to the Channel
Process = ParallelProcess   -- [p1,p2] in parallel
+ ChoiceProcess   -- [p1,p2], events choose one
+ opProcess   -- [opAction,p], e.g., c!7->p
+ ipProcess    -- [ipAction,function], e.g., ?c->λx.f(x), f must return a Process
+ stop
-- Values, Semantic Domains --
stdIp = chan   -- the standard input Channel
stdOp = chan   -- the standard output Channel
opProc = ?stdOp -> λch.{write ch to a textarea}->opProc
ipProc = {ch is next char from stdIp} stdIp!ch->ipProc
NB. opProc and ipProc could be "secret"?
-- Special Members of the Starting Environment --



  1. A running state is a collection of Processes (i.e., opProc, ipProc and at least one of the user's) to be executed in parallel. Note, some of these Processes may be choices between several (sub-)Processes, i.e., (p1|p2|...).
    Each Process must be evaluated to WHNF so we see its first Action and the Channel thereof (although 'e' need not be WHNF in 'c!e').
  2. repeat: Find a pair of Processes that can interact, i.e., (p1=?c->...) and (p2=c!v->...) for some Channel 'c'. (Note that (?c->...|c!v->...) cannot communicate with itself).
    There is a matter of being "fair", maybe random, if there are multiple such pairs.
  3. Make the exchange of the value 'v'. Advance p1 and p2 and remove (i) any "stops" and (ii) choices, if any, that were alternatives to p1 and p2.
  4. until cannot find a pair.
  5. If any Process other than opProc and ipProc remains this may indicate 'deadlock'.
-- Execution --

In the 1980s and 1990s I wrote an interpreter for PFL / CCS / π-calculus in Pascal. When the wwweb came along I put the interpreter on the Computer Science web server as a runnable cgi-bin program. Changes to the (later) Faculty of Information Technology (FIT) and Monash University web servers broke quite a few cgi-bin programs. I had always intended to translate the interpreter from Pascal to Java but Mozilla etc. "went off" Java. Finally I translated it into Javascript instead. Inspired by CSP[Hoa78], CCS[Mil80] and the original PFL[Hol83,Mit84]. — L.A.

References

[Hoa78] C. A. R. Hoare. Communicating sequential processes (CSP). CACM, 21(8), pp.666-677, 1978.
[Hol83] S. Holmstrom. PFL: A functional language for parallel programming and its implementation. Programming Methodology Group, University of Goteborg and Chalmers University of Technology, 1983.
[Mil80] R.Milner. A Calculus of Communicating Systems (CCS). Springer Verlag, LNCS, vol.92, 1980 and ECS-LFCS-86-7, Laboratory for Foundations of Communicating Systems, University of Edinburgh, 1986.
[Mit84] K. Mitchell. A user's guide to PFL. Dept. of Computer Science, University of Edinburgh, 1984.