* 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