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 pi-calculus 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 mu-calculus, but it is
completely different since its expressions are formulae,
not terms (as are the pi-calculus or the lambda-calculus
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 Curry-Howard 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 Binding-Time Analysis, In E.
Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in
Computer Science, pages 184-195, 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
proof-theoretic aspects. There is a lot of work out there in the
model-checking 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