[Prev][Next][Index][Thread]
On fixed points in (full classical) linear logic
Proposition [Least and greatest fixed point in LL]
For any formula A(x) \in LL where x occurs positively, then
/\ x.(!(A(x) -0 x) -0 x)
is the least fixed point in (full classical) LL ordered by |- of
the mapping x |-> A(x).
Greatest fixed point is (indeed) dual.
My questions are then~:
1. Is that already known ? (or (nobody is perfect) false ??)
(I can post the proof if this is new...)
2. Is there any (non trivial) statement of unicity of such
least (and greatest) fixed points ?
3. I have already made some (draft) works towards the
specification of processes within LL (quite straigforwardly
encoding (syntactic) CCS like processes as formulae in LL
with phase semantics seen as a testing semantics) and such
fixed point constructors enable me to describe as LL
formulae specification of infinite (regular) behaviours.
Is there any recent work in that direction ?
Thanks for any comments,
David Janin
-----------------------------------------------------------
LaBRI - Universite' de Bordeaux | janin@labri.u-bordeaux.fr
351, cours de la Liberation | Tel : (33) 56 84 69 12
33 405 Talence FRANCE | Fax : (33) 56 84 66 69
-----------------------------------------------------------