Processes and Lambda Calculus?

[Arkimedes]

I know there is some sort of process algebra (or possibly calculus?) out there, but unfortunately I only know Lambda calculus...and what I know is nothing too deep (just the basics for math, and logic). Is there any formulation of processes in terms of Lambda calculus? I tried searching google several times and it was useless.

[bballad]

Ok its been ten years for me, and well calc wasn't too bad but I never got past nonlinear algabra, so this may be something more advanced but what the hell is Lambda calculus I have never heard of it.calculus is calculs, you know intagrals, difirentials, defEQ. ext.

[dinowuff]

http://en.wikipedia.org/wiki/Lambda_calculus

[bballad]

Ahh ITs comeing back to me now...thats the theoritical programming languages crap that I slept through in college and have never seen after......I will leave taht t othe ivory tower folks

[bballad]

http://en.wikipedia.org/wiki/Process_calculi here you go for a starting point.



sad thing is I use to be a wiz at funtional languages, did my senior project in lisp (only one not useing c++) and worked in lisp++ for a while....still never dealt with lambda calculs outside of a few thory classes.

[Arkimedes]

I know lambda calculus, what I am wondering is if it can be formulated such that it incorporates something like pi calculus or process calculi.

Could the process be nothing more than lambda calculi in Hoare logic?

[sec_ware]

Hi

Let me elaborate and paraphrase your question, since I am interested
in this as well.


Lambda calculus has been successfully mapped onto pi calculus.
This seems reasonable even intuitively, as functions can be regarded
as a particular type of processes. [1,2] have written extensively
about this.


You are asking about the other way - can be pi calculus mapped onto
lambda calculus, or rather, can we map processes onto functions?

Now I am showing my ignorance - the topic is too involved for my basic
knowledge: as far as I understood, lambda calculus is not complete in
the concurrent state space. An concurrent lambda-calculus model has
been developed which seems to be complete[3,4,5]. I hope these readers
(and references therein) are of some use - if you can't access acm.org
or siam.org, just ask me.

Keep us updated!

/edit: If you want to look into the industrial application of formal
methods, have a look at Bowen/Hinchey's Ten Commandments Revisited[6].

Cheers


[1] http://www.cs.unibo.it/~sangio/Book_pi.html
[2] Niehren, J. Functional computation as concurrent computation
(http://portal.acm.org/citation.cfm?id=237721.237801)
[3] Boudol, G. 1989. Towards a Lambda-Calculus for Concurrent and Communicating Systems
(electronically not available, unfortunately)
[4] SIAM J. Comput. 27 (1998) 1376
(http://epubs.siam.org/sam-bin/getfil...cles/27586.pdf)
[5] http://ieeexplore.ieee.org/iel2/402/4748/00185524.pdf
[6] http://www.jpbowen.com/pub/fmics05.pdf

[Arkimedes]

I was discussing this with a friend last night, he suggested that rather than trying to incorporate pi calculus into lambda calculus, try to incorporate lambda calculus into pi calculus. And this is, coincidentally, just what you have suggested as well!

But, from my knowledge of the "Hamilton-Jacobi" equations of classical mechanics (in physics), when we show the path of a thing it is a time-derivative. Could we not as well show the path of information as a time derivative (or, better, as a light cone from special relativity)?

I don't really know...so I won't pretend to. But this seems logical to me as an incorporation of pi into lambda calculi.

If this is thus far correct (for lambda calculus), it would then present itself with several advantages...largely that lamda calculus is now dynamic. I can't grasp the consequences of this, but it would be fascinating to formalize.

The sources cited are of incalculable assistance. I'll read the ones I can before I do aything, thanks!