3 ms·
You can take this work much further in an "FP" kind of way by noting that the pi calculus is a good proof system for linear logic. Frank Pfenning has some lectu
by tel 11y ago
You can take this work much further in an "FP" kind of way by noting that the pi calculus is a good proof system for linear logic. Frank Pfenning has some lectures on this.
- mafribe 11y agoI don't fully agree with Pfenning here. The pi-calculus is not that good a proof system for linear logic: pi-calculus imposes sequentiality constraints on proofs that impede parallelism. Take for example the term x!<a> | y!<b> | x?(c).y?(d).P You have to sequentialise the two possible reductions on x and y. The culprit is the pi-calculus's input prefix, which combines two operations: blocking input and scoping of the bound variables (here c and d). This sequentialisation is not true to the spirit of linear logic proofs (think e.g. proof nets). Conversely, I don't think linear logic is a good typing system for pi-calculus for a variety of reasons: among them that linear logic does not track causality well, and because it doesn't take care of affine (at most once) interactions well.
- tel 11y agoThese are good points and I'll have to consider them. I was planning on going back through Pfenning's notes again in a bit and I'll keep a more critical eye this next time. Thanks! (Also, to be clear and with reference to other threads we've conversed on here, I think of linear logic and pi calculus, even if they aren't well-corresponding, as fantastic, unavoidable examples of non-function-application style programming.)