|
|
|
|
|
by mafribe
4459 days ago
|
|
As to (1) I disagree, it's difficult to express general concurrent/parallel computation in lambda-calculus. You need to resort to encodings. That's why process calculi were invented. Regarding (2), I'm afraid I also disagree. While continuations can express classical logic in some way, it's generally only possible to express certain cut elimination strategies (e.g. call-by-value, as in the Stewart-Ong lambda-mu-calculus). I don't think we know how to do all of classical logic yet. Moreover, adding jumps (which is what continuations are) to lambda-calculus results in an extremely complicated and hard to understand system (e.g. the reduction semantics of the lambda-mu-calculus is usually only handwaved). If you write the very same semantics in pi-calculus, it's trivial and extremely transparent (see "Control in the Pi-Calculus" by Honda et al). Finally, I think it's conceptually deeply confused to 'add' continuations to lambda-calculus. A much cleaner picture emerges when one understands that the call-return jumping discipline engendered by the function-calls of lambda-calculus is a special case of the general jumping that continuations can do. So really one should start with a continuation calculus, and can then see lambda-calculus as a strict sub-calculus of especially disciplined jumps (call-return with affine usage of the return jump). |
|