* Introduction 

   All models are wrong but some are useful.

** FP?
   
   Lambda-calculus is a model of FP

** FP is not all of computation.

   What is a model of parallel programming? 

*** Want to solve 

       lambda-calculus               ???
    ----------------------  = --------------------
    functional programming    parallel programming

*** Answer

   Pi-calculus [1]

* Even better: asynchronous pi-calculus [2, 3]

   P   ::=   0            finished
        | x!y             output on x
        | x?(y).P         input on x
        | P || P          parallel 
        | (nu x).P        fresh name generation
        | !P              recursion

Here x, y range over a countably infinite set of variables (and might
be idential or distinct).  Note (.) means binder! So TWO binders.

** Free and bound variables:

   fv(0)        = empty
   fv(x!y)      = {x, y}
   fv(x?(y).P)  = {x} union (fv(P) minus {y})
   fv(P||Q)     = fv(P) union fv(Q) 
   fv((nu x).P) = fv(P) minus {x}
   fv(!P)       = fv(P)

   bv(0)        = empty
   bv(x!y)      = empty
   bv(x?(y).P)  = {y} union bv(P)
   bv(P||Q)     = bv(P) union bv(Q) 
   bv((nu x).P) = bv(P) union {x}
   bv(!P)       = bv(P)

** Graphical notation: pineapples
** Challenge 1: 

   How many asynchronous pi-calculus terms of size n are there 
   (up to alpha-convertibility)?

   Notions like affine/linear carry over

* Reductions (following a "chemical semantics" [4])

   x!y | x?(v).Q --> Q[y/v]

   P --> Q implies (nu x).P --> (nu x).Q

   P --> P' implies P|Q --> P'|Q

   !P --> P|!P

   P == P' --> Q' == Q implies P --> Q

** Here == is the structural congruence 

== is the least congruence containing alpha-convertibility such that

   P|Q == Q|P
   P|0 == P
   (nu x).0 == 0
   if x not free in P then (nu x).(P|Q) == P|(nu x).Q

Note that == is a syntactic relation and easily decidable.
Note also that there is a way defining reductions that does
not use ==, but instead labelled transitions

** Challenge 2: 

 How many asynchronous pi-calculus terms of size n are there
 (up to ==)?

I expect this to be more difficult than Challenge 2.

* Relationship with lambda-calculus

   The lambda-calculus embeds into pi [5]

   The key idea is simple: a lambda-term is a server.

   With types on pi-calculus, this embedding becomes precise (= sound
   and complete). In other words, lambda-calculus is a well-behaved
   form of message passing, thus fulfilling an old dream of
   Hewitt's [6].

* Typing systems for pi-calculus

   Super hot research area. Google "session types"

** Challenge 3: 

Lift questions about typability for 
random lambda terms to pi-calculus.

* Literature 

[1] R. Milner, J. Parrow, D. Walker, A Calculus of Mobile Processes

[2] K. Honda, M. Tokoro, On Asynchronous Communication Semantics.

[3] K. Honda, M. Tokoro, An Object Calculus for Asynchronous Communication.

[4] G. Berry, G. Boudol, The Chemical Abstract Machine.

[5] R. Milner, Functions as Processes.

[6] C. Hewitt, Viewing Control Structures as Patterns of Passing Messages.
* Questions?

Please contact me (Martin Berger).
Email: M.F.Berger@sussex.ac.uk