Prev: "a new cosmology"
Next: solutions manual
From: JohnF on 28 Jul 2010 13:51 Is there some kind of typed lambda calculus analogous to temporal logics? Note that I'm not quite sure what I'm asking here, but maybe some way to make sense of and complete the following kind of vague diagram, combinatory (or typed or untyped other) logic > lambda calculus       V V temporal logics > ??????? "temporal lambda calculus" Again, let me be the first to admit I don't really know what I'm asking for, or even talking about. And I couldn't dig up much help from google trying to clarify it. Thanks,  John Forkosh ( mailto: j(a)f.com where j=john and f=forkosh )
From: Jose Juan Mendoza Rodriguez on 2 Aug 2010 09:17 Hello, I do not understand your square quite well, but perhaps Robin Milner's picalculus is what you are looking for. It is a calculus for concurrent mobile processes. There is another calculus related to temporal properties of processes, Dexter Kozen's modal mucalculus, but it is completely different since its expressions are formulae, not terms (as are the picalculus or the lambdacalculus expressions). Kind regards.  Jose Juan Mendoza Rodriguez let me=josejuanmr in let privacy=iespana in let net=es in me(a)privacy.net
From: Hans H�ttel on 2 Aug 2010 15:45 In article <i2pqnk$t09$1(a)reader1.panix.com>, JohnF <john(a)please.see.sig.for.email.com> wrote: > Is there some kind of typed lambda calculus analogous > to temporal logics? Note that I'm not quite sure what > I'm asking here, but maybe some way to make sense of > and complete the following kind of vague diagram, > > combinatory (or typed or untyped > other) logic > lambda calculus >   >   >   > V V > temporal logics > ??????? > "temporal lambda calculus" > > Again, let me be the first to admit I don't really know > what I'm asking for, or even talking about. And I couldn't > dig up much help from google trying to clarify it. Thanks, Are you thinking of a realizability interpretation of temporal logic similar to the CurryHoward realizability interpretation of intuitionistic logic, where  logical formulae correspond to types,  the proof of a formula corresponds to a lambda term inhabiting the corresponding type  proof normalization corresponds to beta reduction ? If this is the case, then there is a paper by Rowan Davies: Rowan Davies. A Temporal Logic Approach to BindingTime Analysis, In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 184195, July 1996.� which gives rise to what the author calls a "temporal lambda calculus". Somewhat more na�vely, we can think of a Kripke structure which is a model of a formula F as a "realizer" of F and not care much about the prooftheoretic aspects. There is a lot of work out there in the modelchecking community on synthesizing Kripke models of temporal formulae, and much of it is based on variations of tableau techniques for modal logic. Hans

Pages: 1 Prev: "a new cosmology" Next: solutions manual 