Theoretical Computer Science 357 (2006) 215 – 229

[Link]/locate/tcs

Geometrical semantics for linear logic (multiplicative fragment)

Sergey Slavnov
Cornell University, Malott Hall, Ithaca, NY 14853-4201, USA

Abstract
Linear logic was described by Girard as a logic of dynamic interactions. On the other hand, Girard suggested an analogy between
LL and quantum theory. Following these two intuitions we give an interpretation of linear logic in the language, which is common
for both dynamical systems and quantization. Thus, we propose a denotational semantics for multiplicative linear logic using the
language of symplectic geometry.
We construct a category of coherent phase spaces and show that this category provides a model for MLL. A coherent phase space
is a pair: a symplectic manifold and a distinguished field of contact cones on this manifold. The category of coherent phase spaces is
a refinement of the symplectic “category” introduced by Weinstein. A morphism between two coherent phase spaces is a Lagrangian
submanifold of their product, which is tangent to some distinguished field of contact cones. Thus, we interpret formulas of MLL as
fields of contact cones on symplectic manifolds, and proofs as integral submanifolds of corresponding fields.
In geometric and asymptotic quantization symplectic manifolds are phase spaces of classical systems, and Lagrangian submani-
folds represent asymptotically states of quantized systems. Typically, a Lagrangian submanifold is the best possible localization of
a quantum system in the classical phase space, as follows from the Heisenberg uncertainty principle. Lagrangian submanifolds are
called sometimes “quantum points”.
From this point of view we interpret linear logic proofs as (geometric approximations to) quantum states and formulas as
specifications for these states. In particular, the interpretation of linear negation suggests that the dual formulas A and A⊥ stand
in the same relationship as the position and momentum observables. These two observables cannot simultaneously have definite
values, much like the case of two dual formulas, which cannot simultaneously have proofs.
© 2006 Published by Elsevier B.V.

Keywords: Linear logic; Denotational semantics

1. Introduction

There exists a belief that linear logic should have some significant relations with “traditional” mathematics and, may
be, with physics. Starting from the very emergence of LL a considerable amount of work has been done in order to find
its denotational models in various fields of mathematics and mathematical physics. Let us mention works of Blute and
Scott [3], Ehrhard [4] and Girard [7] himself. This work belongs to this tradition. However, the model of MLL, which
we propose below, has little to do with linear algebra or functional analysis. Our interpretation is based on geometry,
more precisely on symplectic geometry, which is the basic language for analytical mechanics and geometric aspects of
quantum theory.

E-mail address: serge@[Link].

0304-3975/$ - see front matter © 2006 Published by Elsevier B.V.

doi:10.1016/[Link].2006.03.020
216 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

Linear logic was described by Girard as a logic of dynamic interactions. On the other hand, Girard [5] suggested an
analogy between LL and quantum theory. Following these two intuitions we give an interpretation of linear logic in
the language, which is common for both dynamical systems and quantization.
The standard classical treatment of a macroscopic dynamical system is based on symplectic geometry. A dynamical
system gives rise to the phase space (symplectic manifold), evolution being described globally by flows, locally by
vector fields on the phase space. The equations of motion are Hamilton equations, whose coordinate-free formulation
needs only a symplectic structure. The transformation to Hamilton–Jacobi equation transforms the evolution of the
system to the evolution of wave fronts and has been the formulation of choice for 150 years. The relevance of this choice
was once more justified when quantum mechanics was discovered; all methods of quantization are based on symplectic
geometry and Hamilton–Jacobi formalism. Wave fronts themselves have interpretation as asymptotic approximations
to wave functions of the corresponding quantized system.
In the classical context the theory is based on a specific choice of canonical coordinates—position q and momentum
p. These give rise to a Poisson bracket between classical observables, which governs dynamic. A local expression of
the Poisson bracket is a non-degenerate skew-symmetric bilinear form on the (co)tangent bundle—a symplectic form.
The Poisson bracket or the symplectic form allow coordinate-free formulation of the equations of motion, The notion
of a symplectic manifold is the abstraction in coordinate-free form of the Hamilton–Jacobi formulation of classical
mechanics.
Solutions of the Hamilton–Jacobi equations, describing the evolution of wave fronts, (which have, in particular,
the meaning of approximate wave functions of the quantized system) are, geometrically, certain submanifolds of the
phase space—Lagrangian submanifolds. Lagrangian submanifolds should satisfy some specifications determined by
corresponding problems. One may take as an example of such a specification a field of contact cones on the phase
space, that is a subset of the tangent bundle, closed under scalar multiplication. Then given a field of contact cones A
on the phase space MA , one looks for Lagrangian submanifolds of MA tangent to A.
This is the key point in our interpretation of multiplicative linear logic. Thinking of formulas as specifications we
interpret them as fields of contact cones on corresponding symplectic manifolds, whereas proofs become Lagrangian
submanifolds tangent to these fields. More specifically, we construct a category whose objects are symplectic manifolds
(carrying some additional structure, namely a field of contact cones) and whose morphisms are Lagrangian subman-
ifolds. This seems to us to be very much in spirit of symplectic geometry whose slogan was expressed by Weinstein
[10]

EVERYTHING IS A LAGRANGIAN SUBMANIFOLD.

Typically a morphism between manifolds M and N in our category is a Lagrangian submanifold of M− × N where
M− stands for the manifold M equipped with the minus symplectic structure of M. This submanifold is required to be
tangent to a certain field of contact cones. In fact, we think of these fields of contact cones as “infinitesimal versions”
of coherence relations of the standard coherent spaces semantics of linear logic, and Lagrangian submanifolds are
“infinitesimal analogues” of cliques.
Looking at our interpretation from a point of view of geometric quantization, we come to an interesting intuition. Let
us recall the meaning of associating Lagrangian submanifolds with wave functions. Due to the Heisenberg uncertainty
principle the position and the momentum of a particle cannot be measured simultaneously. Therefore, the localization
of a quantum particle in the (classical) phase space may be given either by its position or by its momentum. The level
sets of position and momentum are Lagrangian submanifolds of the phase space. More generally, one may speak about a
localization of the particle not at a point of the phase space, but at a Lagrangian submanifold. Lagrangian submanifolds
of the phase space are sometimes called “quantum points”. In geometric quantization a choice between the position
and momentum representation amounts to a choice between two transversal foliations of the phase space—the foliation
into the level sets of position and a foliation into the level sets of momentum. In particular, two “quantum points”,
localized, respectively, in the momentum and the position spaces, are represented by transversal submanifolds. Now,
in our interpretation of MLL dual formulas A and A⊥ are interpreted as complementary fields of contact cones, hence
a Lagrangian submanifold tangent to the field A (a semantical “proof” of A) is transversal to a Lagrangian submanifold
tangent to the field A⊥ (semantical “counterproof” of A). Thus, intuitively, proofs and counterproofs correspond to
“quantum points” in position and momentum representation, respectively. That is, proofs and counterproofs seem to
be in the same relationship as position and momentum observables.
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 217

The idea of considering Lagrangian submanifolds as morphisms has some history. It has been present in literature
since 1970s. In 1981 it was spelled out [10] and the symplectic “category” with symplectic manifolds as objects and
Lagrangian submanifolds as morphisms was constructed. However, it was not a true category, since the composition of
Lagrangian submanifolds given by symplectic reduction was not always defined. Roughly speaking, in order for two
Lagrangian submanifolds to compose, they should intersect transversally, which condition fails in general. It turns out,
though, that the extra structure of a field of contact cones, which allows us to take as morphisms between M and N
only those submanifolds of M− × N, which are tangent to a certain field, is exactly what is needed in order to exclude
non-composable pairs of morphisms. Recalling Girard’s [6] slogan
FORMULAS = PLUGGING INSTRUCTIONS
we may see our fields of contact cones as these instructions; they require that the “plugging” of submanifolds should
be transversal.
We would like to note also that our construction was motivated and inspired only by investigations of linear logic.
Only later it was understood that our category was a natural refinement of the “category”, which had already existed
on its own right. We would like to consider it as a modest manifestation of an actual interaction of linear logic with
“traditional” mathematics.
We assume that the reader is familiar with elementary notions of differential geometry. For general references on
symplectic geometry we use [9].

2. Linear logic and denotational semantics

In this section we review briefly the circle of ideas tied with linear logic and denotational semantics.
The concept of denotational semantics was derived apparently from Brower–Heyting–Kolmogorov (BHK) interpre-
tation of the intuitionistic logic. The key idea of BHK interpretation is that constructive proofs should be interpreted as
programs or algorithms. The crucial part is how the implication is understood: a proof of A → B should be a program
(function, algorithm), which transforms any proof of A to a proof of B. A more modern, abstract nonsense version of
this idea may be formulated like the following: in a constructive logic, the class of formulas forms a category, whose
morphisms are proofs. Typically a morphism between A and B is a proof of the implication A → B.
This idea is justified by the cornerstone property of Cut-elimination.
Any reasonable logical calculus contains a rule of Cut, which in the simplest case takes the form:
A ⇒ BB ⇒ C
. (1)
A⇒C
This rule, which says, basically, that proofs of two lemmas can be combined to yield together a proof of a theorem, is
of course absolutely essential for any kind of rational reasoning. However, it is well-known that this rule is redundant
in the following sense: in all known reasonable logical systems the rule of Cut is derivable (it can be eliminated). This
is the starting point of any proof theory, and the property of Cut-elimination is often understood as the criterion for
a calculus to be called a logic. (What the property of Cut-elimination actually says in real life is that all lemmas and
definitions can be spelled out.) In proofs-as-programs interpretations, the process of Cut-elimination corresponds to
the computation of the outcome of a program.
We chose notations to write the rule of Cut in (1) above so that it is very likely to recognize a composition of
morphisms in it. Thus, if one would like to think of formulas as objects in a category then natural candidates for
morphisms are cut-free proofs. Given two cut-free proofs
and  of A ⇒ B and B ⇒ C, respectively, one combines
them by means of the Cut to yield a proof of A ⇒ C and then, applying a Cut-elimination procedure to this new
proof, computes the composition  ◦
. In order for this construction to work appropriately, it is necessary for a cut-free
form of a proof to be (essentially) unique. This does not hold, for example, in the case of classical logic. Therefore,
classical proofs do not form a category. This is the precise meaning of a well-known statement that classical logic
is not constructive. Classical proofs are not programs since the result of a computation is not defined uniquely. In a
constructive calculus proofs form a category with cut-elimination being composition, and proofs are programs with
cut-elimination being computation.
Now, given a constructive logical system S, the problem of denotational semantics for S consists in finding a
representation of the category of proofs of S. In more down-to-earth terms, in denotational semantics one tries to
218 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

interpret formulas and connectives of S as some objects and operations (multifunctors), and proofs as morphisms
between these objects in such a way that the interpretation be invariant under Cut-elimination. An important difference
with the traditional (“Tarski-style”) semantics is that denotational semantics is not in general concerned with any kind
of “truth” or “falsity” of formulas. What is being modeled is the functional behavior of proofs.
Linear logic was introduced by Girard [5]. A remarkable discovery of Girard was the phenomenon of linearity of
some proofs. Typically a proof of the implication A ⇒ B is linear if it uses the hypothesis A only and exactly once,
and otherwise it is nonlinear. This discovery allowed him to investigate the functional structure of proofs in a great
detail. In particular, he was able to decompose intuitionistic implication into linear and nonlinear parts. Linear logic is
a result of this decomposition.
Linear logic is usually described as a resource sensitive calculus; the hypotheses in an implication are considered
as resources: in general they cannot be used unlimitedly. This system has several “layers”: multiplicative, additive
and exponential. The multiplicative fragment is the simplest and consequently the weakest one. However, it is also in
some sense the basic fragment, and our understanding of linear logic depends considerably on our understanding of
the multiplicative part.
The simplest illustration to the phenomenon of linearity is provided by the following example. In the intuitionistic,
as well as in the classical logic one may prove the implication

A, (A → B) ⇒ A&B. (2)

From the functional point of view this implication is nonlinear: the hypothesis (resource) A is used twice: at first proofs
of A and A → B yield together a proof of B, but then one needs to add to this proof of B the proof of A, which has
already been used. In multiplicative linear logic implication
and conjunction ⊗ (usually called times or tensor) are
linear, and one may prove

A, A
B⵫B

or

A ⊗ A, A
B⵫A ⊗ B

but nothing like (2).

A complex structure of proofs revealed by linear logic motivated the interest in its denotational semantics; one
needed new methods to model (and understand) this complex structure. In particular, it was soon understood that
various structures of “traditional” mathematics (topological vector spaces, operator algebras, Hopf algebras, games)
might be appropriate for this purpose. (We mentioned in the introduction just a couple of works, which were inspired
by this idea.) The interest in mathematical methods was accompanied by a strong interest in physics, especially in the
quantum theory. Indeed, in linear logic a hypothesis can be used only once in general; one may say that in some sense
the “truth-value” of a formula is changed in the course of the proof or, even better, sometimes it simply gets lost, stops
making sense. This resembles to some extent the situation in quantum mechanic. Typically, the assumption about the
wave structure (particle structure) of the matter cannot be used unlimitedly since in the course of some experiments it
becomes wrong (better to say inconsistent). A position of a particle gets lost after a measurement of momentum and
vice versa. Although, to the author’s knowledge, only few attempts to put intuitive analogies between LL and quantum
theory in some tangible form have been made (let us mention [2]), these analogies are discussed a lot by researchers
in the field.
These short remarks may perhaps give some motivation for modeling linear logic with the use of symplectic geometry,
which is one of the basic tools in mathematical physics. In the next two sections we recall some basic results from this
field.

3. Symplectic spaces and symplectic manifolds

Material of the following two sections is standard. We refer the reader to [9] for a more detailed discussion.

Definition 1. A symplectic space V ,  consists of a finite-dimensional vector space V and a skew-symmetric non-
degenerate bilinear form  on V.
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 219

Given a symplectic space V , , we shall always write V for V , , and given u, v ∈ V , we shall write u, v for
(u, v) unless this leads to a confusion.
A map  : V1 → V2 where Vi = Vi , i , i = 1, 2, are symplectic vector spaces is a symplectomorphism, if  is an
isomorphism of vector spaces and  transforms 1 to 2 . In this paper, the notation V1 V2 is always to be understood
as meaning that V1 and V2 are isomorphic (but not necessarily symplectomorphic).
It follows from the non-degeneracy of symplectic form that a symplectic vector space is necessarily even-dimensional.
A canonical example is U × U ∗ , , where U is a vector space and  is given by
((v1 , u1 ), (v2 , u2 )) = v1 , u2  − v2 , u1 .
Like the familiar case of Euclidean spaces one may define the orthogonal “complement” with respect to a symplectic
form. Given a subspace U with dim U = k of a symplectic space V with dim V = 2n, the space orth(U ) is defined by
orth(U ) := {v ∈ V |u, v = 0 ∀u ∈ U }. (3)
It is easy to see that dim orth(U ) = 2n − k.

Definition 2. A subspace U of V = V ,  is called isotropic if U ⊆ orth(U ), coisotropic if orth(U ) ⊆ U and

Lagrangian if it is both isotropic and coisotropic. It is called a symplectic subspace of V if it is a symplectic space under
the restriction of  to U.

The following elementary observations may hopefully give some feeling of the properties of orthogonal “comple-
ments”:

Note 1. An isotropic subspace of the symplectic space V is Lagrangian iff dim L = 1

2 dim V .
Let U, W be subspaces of a symplectic space V. Then
orth(orth(U )) = U ;
orth(U + W ) = orth(U ) ∩ orth(W );
orth(U ∩ W ) = orth(U ) + orth(W ).
If U is isotropic (coisotropic) then orth(U ) is coisotropic (isotropic);
If U is symplectic then orth(U ) is symplectic and V is symplectomorphic to U ⊕ orth(U ).
If U = V then orth(U ) = {0}.
For any Lagrangian subspace L of V there exists a complementary to L Lagrangian subspace L of V s.t. L is
canonically isomorphic to L∗ and V is canonically symplectomorphic to L ⊕ L .

For (straightforward) proofs see for example [9], 1.5–1.9. (The last assertion of the note above explains why the
space U ⊕ U ∗ is indeed the canonical example of a symplectic space.)
Given symplectic spaces V , , Vi , i , i = 1, 2, one can construct new symplectic spaces V− := V , −, and
V1 ⊕ V2 , 1 + 2 . The following note will be used in the sequel:

Note 2. Let V , , Vi , i , i = 1, 2, be symplectic spaces and L, L1 , L2 be Lagrangian subspaces of V, V1 and V2 ,
respectively. Then L and L1 ⊕ L2 are Lagrangian subspaces of V− and V1 ⊕ V2 , 1 + 2 , respectively.

Proof. Is straightforward. 

4. Symplectic manifolds

A natural generalization of the notion of a symplectic vector space is that of a symplectic manifold.

Definition 3. A symplectic manifold M,  consists of a smooth manifold and a closed non-degenerate 2-form 
on M.
220 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

If this does not lead to a confusion we shall use the notation vx , ux  := (x)(vx , ux ) for vx , ux ∈ Tx M, where
M,  is a symplectic manifold.
Again, the prototypical example of a symplectic manifold is cotangent bundle. We follow the presentation in [8].
Let M be a manifold, T ∗ M be its cotangent bundle.
At any point (q, q ) ∈ T ∗ M the tangent space T(q,q ) T ∗ M to T ∗ M is isomorphic to Tq M × (Tq M)∗ , hence is a
symplectic vector space. The above isomorphism depends, however, on the choice of local coordinates. The invariant
description is as follows.
The space T(q,q ) T ∗ M is equipped with an invariantly defined 1-form M (q, q ) (Liouville form) given by

M (q, q )(v) = q , T(q,q ) (v), (4)

or in local coordinates by
M (q, q )(u, ) = q , u where u ∈ Tq M,  ∈ (Tq M)∗ , (5)
and with the 2-form M = dM (q, q ) (canonical symplectic form) given locally by
dM (q, q )((u1 , 1 ), (u2 , 2 )) = 1 , u2  − 2 , u1 . (6)
These forms are invariantly defined on the whole T ∗ M.
If U is a sufficiently small neighborhood of M and q = (q 1 , . . . , q n ) are local coordinates on U then T ∗ U is
diffeomorphic to U × Rn , where n = dim M, and any covector u ∈ T ∗ U has a unique representation
u = (q 1 , . . . , q n , p1 1 dq 1 + · · · + pn dq n )
Coordinates
(q, p) = (q 1 , . . . , q n , p1 , . . . , pn )
are called canonical coordinates on the cotangent bundle. Canonical symplectic form in this coordinates reads simply


M = dq i ∧ dpi (7)
and Liouville form reads


M = pi dq i . (8)
In fact any symplectic manifold locally looks like a cotangent bundle.
More precisely, the classical Darboux theorem states that for any symplectic manifold P and point x ∈ P there exists
a neighborhood U of x and a system (q, p) of local coordinates on U s.t. in these coordinates  is of the form (7).
Since the tangent space to a symplectic manifold is itself a symplectic vector space, the notions developed for
symplectic spaces may be lifted to the setting of symplectic manifolds. In particular, a submanifold C of a symplectic
manifold M is isotropic, coisotropic, Lagrangian or symplectic, if for any x ∈ C the tangent space Tx C is an isotropic,
coisotropic, Lagrangian or symplectic subspace of Tx M. Two symplectic manifolds M1 , 1 , M2 , 2  are said to be
symplectomorphic if they are diffeomorphic and this diffeomorphism transforms 1 to 2 .
Let us state the following immediate corollary of Note 1

Note 3. An isotropic submanifold
of a symplectic manifold M is Lagrangian iff dim
= 1

2 dim M.

Also the analogue of the Note (2) holds

Note 4. Let M, , Mi , i , i = 1, 2, be symplectic manifolds and
,
1 , L
2 be Lagrangian submanifolds of M,
M1 and M2 , respectively. Then the manifolds M− = M, − and M1 × M2 = M1 × M2 , 1 + 2  are symplectic,
and
and
1 ×
2 are Lagrangian submanifolds of M− and M1 × M2 , respectively.

In the next section, we recall the fundamental concept of symplectic reduction, which, as we shall see, corresponds
in a natural way to the Cut rule (or composition of morphisms).
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 221

5. Symplectic reduction

We proceed to a fundamental in symplectic geometry operation of symplectic reduction.

Let M,
be manifolds and i :
→ M be a smooth map. Recall that (
, i) (or just
, for short) is an immersed
submanifold of M or an immersion in M, if for any point x ∈
there exists a neighborhood U of x s.t. i takes U
diffeomorphically onto a submanifold of M. If M is symplectic and for each x ∈
there exists a neighborhood U of x
s.t. i(U ) is a Lagrangian submanifold of M then the immersion (
, i) is called Lagrangian. Two immersions (
1 , i1 )
and (
2 , i2 ) are said to be equal if there exists a diffeomorphism f :
1 →
2 such that i1 = f ∗ i2 . In this paper, we
shall understand notation
⊂ M as “
is immersed in M”.
Two immersions (
1 , i1 ) and (
2 , i2 ) in a manifold M are said to be transversal, if for any xi ∈
i , i = 1, 2, s.t.
i1 (x1 ) = i2 (x2 ) = x,
it holds that Tx1 i1 (Tx1
1 ) and Tx2 i2 (Tx2
2 ) span the whole Tx M. In this case one may form their fiber product (
1 ∩

2 , i1 ×M i2 ) (or
1 ∩
2 , for short) where

1 ∩
2 = {(x1 , x2 )|xi ∈
i , i = 1, 2, i1 (x1 ) = i2 (x2 )},
and
i1 ×M i2 (x1 , x2 ) = i1 (x1 ).
Given a manifold M, a subset D of TM is called a distribution, if for any x ∈ M the set D ∩ Tx M is a linear space and
dim(D ∩ Tx M) = k for some fixed k independent of x. (Often one uses a more general definition, where the second
condition is dropped.) A distribution D is said to be smooth, if the assignment x → D ∩ Tx M is smooth.
A submanifold
of M is said to be an integral submanifold of D if T
⊆ D. A distribution D is said to be completely
integrable, if for any x ∈ M there exists an integral submanifold
of D passing through x.
It is well known that, unlike integral curves, integral submanifolds (of dimension greater than 1) are by no means a
common thing. More precisely, the classical Frobenius theorem states:

Theorem 1 (Frobenius theorem). Let M be a manifold, D a smooth distribution on M. Then D is completely integrable
iff for any two vector fields t, s lying in D their commutator [t, s] lies in D (such distributions are called involutive).

For the proof see any textbook on differential geometry, for example [8].
Given a completely integrable smooth distribution D on a manifold M, a connected integrable submanifold
of D
is called maximal, if
is not contained in any connected integral submanifold of D other than itself. A partition of M
into maximal integral submanifolds is called the foliation of M generated by D, and maximal integral submanifolds of
D are called leaves of this foliation (leaves of D, for short). Finally, the foliation generated by D is simple if the set
M/D of leaves of D has a manifold structure, such that the natural projection  : M → M/D is smooth.
Now let M be a symplectic manifold and C be a coisotropic submanifold of M. Assume also that for each x ∈ X the
dimension k of orth(Tx C) is independent of x. Since for each x ∈ C the space Tx C is coisotropic, i.e. orth(Tx C) ⊆ Tx C,
we have that the distribution

orth(T C) := orth(Tx C)
x∈C

(called the null distribution) lies in TC.

Let us denote orth(T C) by C ⊥ . Suppose that C ⊥ is a smooth distribution on C. Then the following theorem holds:

Lemma 1. With notations as above the distribution C ⊥ is integrable. Suppose that the foliation generated by C ⊥ is
simple. Let C be the set of leaves of C ⊥ ,  : C → C the natural projection. Then the manifold C is symplectic under
the well-defined symplectic form  given by
((x))(T (vx ), T (ux )) = (x)(vx , ux ),
where x ∈ C, ux , vx ∈ Tx C.
222 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

Furthermore, if L is an immersed Lagrangian submanifold of M transversal to C then (L ∩ C) is an immersed

Lagrangian submanifold of C, and  restricted to L ∩ C is an immersion.

For a proof see for example [9], 3.14.3 and 3.14.19.

With notations as above we shall call the projection C → C symplectic reduction and the manifold C the reduced
space.
In the next section, we describe the symplectic “category” as defined by Weinstein [10] and explain how symplectic
reduction is related to the composition of morphisms.

6. The symplectic “category”

In the symplectic “category” one takes symplectic manifolds as objects and Lagrangian submanifolds of A− × B
(so-called canonical relations) as morphisms between symplectic manifolds A and B. The idea to consider Lagrangian
submanifolds as morphisms originated apparently in the context of WKB quantization. We refer the reader to [1] for a
discussion of related methods with the emphasis on the symplectic “category”.
One may wonder what is the natural notion of a morphism between symplectic manifolds. If we attempt to define a
morphism between symplectic manifolds in the obvious way as a smooth map, which preserves symplectic structure,
then we soon find that such morphisms are quite few. Basically the only smooth maps, which may preserve symplectic
structure, are immersions. On the other hand, there are plenty of canonical relations between two symplectic manifolds.
In particular, let us mention two examples:
If M and N are symplectic manifolds and f : M → N a symplectomorphism then it is immediate that graph(f ) is
a Lagrangian submanifold of M− × N .
The second example is more interesting. Let M and N be two general (not symplectic) manifolds and f : M → N a
smooth map. Recall that the cotangent bundles T ∗ M and T ∗ N are symplectic manifolds. Now let F ⊆ M × N be the
graph of f and
T F 0 = { ∈ T ∗ (M × N ) T ∗ M × T ∗ N : , v = 0 for all v ∈ T F }
be the annihilator of TF. Then, as follows from the definition of the canonical symplectic structure, T F 0 is a Lagrangian
submanifold of T ∗ M × T ∗ N , and after the transformation

: T ∗ M × T ∗ N → (T ∗ M)− × T ∗ N,

: (u, v) → (−u, v),
its image
(T F 0 ), which we will denote by T ∗ f , becomes a canonical relation on T ∗ M × T ∗ N . Thus a smooth map
f between M and N lifts to a canonical relation on the corresponding cotangent bundles called the cotangent lift of f.
Note that in general f does not lift to any map between cotangent bundles. One may say that there exists a functor from
the category of smooth manifolds to the symplectic “category”.
These were a few words of motivation for definition of symplectic “category”. Now let us discuss how to compose
canonical relations. Given two canonical relations
⊂ M− × N and  ⊂ N− × P , one attempts to define their
composition set theoretically, i.e.
 ◦
:= {(x, z) ∈ M × P |∃y ∈ N s.t. (x, y) ∈
and (y, z) ∈ }. (9)
The problem with this composition is that ◦
is not in general a submanifold of M ×P . However if
×, a Lagrangian
submanifold of M− × N × N− × P , is transversal to the coisotropic manifold
C = {(x, y1 , y2 , z) ∈ M− × N × N− × P : y1 = y2 }, (10)
then Lemma 1 applies, and
◦  is easily seen to be a canonical relation on M− × P .
Indeed the null distribution C ⊥ consists of vectors of the form (0, v, v, 0) ∈ T M × T N × T N × T P , and leaves of
⊥
C are nothing but the manifolds of the form {x} × N × {z} where x ∈ M, z ∈ P , and N = {(y, y)|y ∈ N } is the
diagonal submanifold of N × N . Hence the reduced space C is just M− × P , and the symplectic reduction  : C → C
is the natural projection on the first and the fourth factors. Since  ◦
was defined exactly as the image of
×  ∩ C
under , we conclude that  ◦
is indeed a Lagrangian submanifold of M− × P .
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 223

But in general the composition of canonical relations is not always defined and the symplectic “category” is not a
true category.
Now consider the subcategory of the symplectic “category” consisting of cotangent bundles and cotangent lifts of
smooth maps. This is indeed a category and is in fact isomorphic to the category of manifolds and smooth maps. Let
us find out what guarantees the composition of cotangent lifts to be always defined.
So let M, N be smooth manifolds and f : M → N be a smooth map. Let T ∗ f be the cotangent lift of f. It is easy to
see that
T ∗ f = {(x, Tf∗(x) f , f (x), )|x ∈ M,  ∈ Tf∗(x) N }.

Let p = (x, Tf∗(x) , f (x), ) ∈ f˜, where x ∈ M,  ∈ Tf∗(x) N . Choose local coordinates on T ∗ M × T ∗ N near p s.t.
in these coordinates
Tp (T ∗ M × T ∗ N ) = Tx M × Tx∗ M × Tf (x) N × Tf∗(x) N.

Vectors tangent to T F 0 at p take in these coordinates the form

(v, Tf∗(x) f  + Tx (Tf∗(x) f )v, Tx f (v), ), v ∈ Tx M,  ∈ Tf∗(x) N. (11)
Let M : T ∗ M → MN : T ∗ N → N be canonical projections. Then for a vector 0 = u = (uM , uN ) of the form (11),
uM ∈ M, vN ∈ N it holds that
T M (uM ) = 0 implies T N (uN ) = Tx f (uM ) = 0 and uN  = 0. (12)
Now recall that if  : E → M is a vector bundle then a vector v ∈ T E is vertical if T (v) = 0. Hence, condition
(12) reads: if a vector 0  = u = (uM , uN ) ∈ T ∗ M × T ∗ N is tangent to T ∗ f then
uM is vertical implies 0  = uN is vertical. (13)
We claim that it is exactly the condition (13) which makes the composition of cotangent lifts be always defined. More
explicitly if P is a third manifold and
1 ⊂ (T ∗ M)− × T ∗ N ,
2 ⊂ (T ∗ N )− × T ∗ P are canonical relations satisfying
(13) then the composition
2 ◦
1 given by (9) is well defined.
If C = T ∗ M × T ∗ N × T ∗ P then C ⊥ consists of vectors of the form (0, v, v, 0) where v ∈ T T ∗ N . It follows
from (13) that T (
1 ∩
2 ) has only zero intersection with C ⊥ and this in turn implies that
1 ×
2 is transversal to C
(this reasoning will be rigorously justified below). Thus, Lemma 1 applies and
1 ◦
2 is a Lagrangian submanifold of
(T ∗ M)− × T ∗ P .
Let us summarize our analysis. Each object M of the subcategory of cotangent bundles and cotangent lift comes with
a singled out distribution V (M) on M—namely the distribution consisting of vertical vectors. For two objects M1 and
M2 of this subcategory only those canonical relations
⊂ M− × N count, which satisfy:
0  = v = (v1 , v2 ) ∈ T
, vi ∈ T Mi , i = 1, 2 implies
v1 ∈ V (M1 ) implies 0  = v2 ∈ V (M2 ).
As we have seen above this is sufficient to guarantee the composition of canonical relations to be defined.
Now we want to make the symplectic “category” into a true category, suitable for interpretation of MLL. The idea is
clear from the remarks above. We have seen that if one equips our symplectic manifolds with some extra structure, for
example a distribution, and take only those canonical relations as morphisms, which satisfy some natural conditions
expressed in terms of this extra structure then problems with composition may be resolved.
However, in order to have a model of MLL such a simple additional structure as distribution turns out to be not
sufficient. The correct object to work with is a generalization of the notion of distribution—a field of contact cones.

7. Contact cones and coherent phase spaces

Let V = V ,  be a symplectic vector space.

Definition 4. A nonempty subset A of V is a contact cone if for any v ∈ A the whole line {tv|t ∈ R} lies in A.
224 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

It is easy to see that adding the zero vector to the complement of a contact cone we obtain a contact cone again
hence each contact cone determines a partition of V − {0} (or of the projectivization PV if the reader prefers) into two
disjoint subsets. To keep with the syntax of linear logic we shall denote the complement of a contact cone A by A⊥ .
Further, it is immediate that the following operations are well defined:
Let Vi , i , i = 1, 2 be symplectic spaces, Ai ⊂ Vi —contact cones. Let V = V1 ⊕ V2 , 1 + 2 .
Then the sets

A1 ⊗ A2 := {(v1 , v2 )|vi ∈ Ai , i = 1, 2},

A1 ℘A2 = (A⊥ ⊥ ⊥
1 ⊗ A2 ) = {(v1 , v2 )|0  = v1 ∈ A1 or 0  = v2 ∈ A2 } ∪ {0},

and

A1
A2 = A⊥
1 ℘A2 = {(v1 , v2 )|v1 ∈ A1 implies 0  = v2 ∈ A2 }

are contact cones in V , .

Now we lift our definitions to the setting of manifolds.

Definition 5. Let M be a symplectic manifold. A subset A of the tangent bundle TM of M is a field of contact cones if
for any x ∈ M the set A(x) := Tx M ∩ A is a contact cone in Tx M.

Obviously a field A of contact cones on a symplectic manifold M determines a partition of the tangent bundle TM
of M into two complementary subsets—just like the case of vector spaces (more precisely into two subsets whose
intersection is the zero section).

Definition 6. A coherent phase space is a pair M, A where M is a symplectic manifold and A is a field of contact
cones on M.

Unless it leads to a confusion we shall denote a coherent phase space M, A simply by A.

Definition 7. A state of a coherent phase space A = M, A is an immersed Lagrangian submanifold of M tangent to
A at every point.

Now we lift the operations defined on contact cones to coherent phase spaces.

Definition 8. Given two coherent phase spaces M1 , A1  and M2 , A2  their tensor product A1 ⊗A2 and cotensor prod-
uct A1 ℘A2 as well as negation A⊥
i and linear implication A1
A2 are given by pointwise operations on corresponding
contact cones.
More precisely, tensor and cotensor products of A1 and A2 are fields of contact cones on M1 × M2 given by

A1 ⊗ A2 = {v ∈ Tx1 M1 × Tx2 M2 |v ∈ A1 (x1 ) ⊗ A2 (x2 ), xi ∈ Mi , i = 1, 2},

A1 ℘A2 = {v ∈ Tx1 M1 × Tx2 M2 |v ∈ A1 (x1 )℘A2 (x2 ), xi ∈ Mi , i = 1, 2},

where T (M1 × M2 ) is identified with T M1 × T M2 .

Negation of A1 is the field of contact cones on (M1 )− given by

A⊥ ⊥
1 = {v ∈ Tx (M1 )|v ∈ A1 (x) },

and linear implication A1
A2 is the field

A1
A2 = {v ∈ Tx1 M1 × Tx2 M2 |v ∈ A1 (x1 )
A2 (x2 ), xi ∈ Mi , i = 1, 2}.

Note that under negation the sign of the symplectic form is changed.
Now we define the domain of our interpretation of multiplicative linear logic.
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 225

Definition 9. The category P of coherent phase spaces consists of:

the class of coherent phase spaces as objects,
for each pair of coherent phase spaces A and B the states of A⊥ ℘B = A
B as morphisms between A and B.
For each object A = MA , A the identity morphism id A is defined as the diagonal submanifold of (MA )− × MA .
For two morphisms
: MX , X → MY , Y  and  : MY , Y  → MZ , Z their composition is defined by

 ◦
= {(x, z)|∃y ∈ MY s.t. (x, y) ∈
and (y, z) ∈ }. (14)

It follows from a discussion in the previous section that the category of cotangent bundles and cotangent lifts embeds
in P. A cotangent bundle T ∗ M corresponds to the coherent phase space T ∗ M, V (M), where V (M) is the vertical
distribution on M.
One has to show that all objects and operations above are well defined. This will be done below in parallel with the
description of the interpretation of MLL.
At first however we will make a few remarks on the analogies between coherent phase spaces and (ordinary) coherent
spaces.

8. Infinitesimal coherent spaces

Recall that coherent spaces is a standard interpretation of linear logic (see [6]). We assume that the reader is familiar
with this model.
A coherent space A consists of a set |A| (called the web of A) and a reflexive symmetric coherence relation on |A|.
One writes

x y (mod A)

for “x is coherent to y”

x  y (mod A)

for “x  = y and x 
 y (mod A)” and

x y (mod A)

for “x is not coherent to y”.
Given a coherent space A, its negation A⊥ has the same web |A|, whereas the coherence (mod A⊥ ) is defined by
 
x y (mod , A⊥ ) if x y (mod A) or x = y. (15)
 
If A and B are two coherent spaces then their tensor and cotensor products A ⊗ B and A℘B are defined to have web
|A| × |B| and coherence relations:
  
(x, x  ) (y, y  ) (mod A ⊗ B) if x y (mod A) and x  y  (mod B), (16)
  
(x, x  )(y, y  ) (mod A℘B) if xy (mod A) or x  y  (mod B). (17)

Finally, a clique in the coherent space A is a subset of pairwise coherent elements of A.

We would like to give a justification of the idea mentioned in the Introduction that fields of contact cones are
“infinitesimal” coherence relations.
Let M be a manifold. Recall that a neighborhood of the zero-section of the tangent bundle TM is diffeomorphic to a
neighborhood of the diagonal M in M × M.
Assume that there is a connection chosen on TM i.e. the class of geodesic curves on M is specified. Then the
diffeomorphism in question is given by the following correspondence:
(x1 , x2 ) ∈ M × M corresponds to vx ∈ T M, if x is the middle point of the unique affinely parameterized geodesic
 : [0, 1] → M joining x1 , and x2 and vx = d/dt( 21 ).
226 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

Note that if vx corresponds to (x1 , x2 ) then −vx corresponds to (x2 , x1 ) also 0x corresponds to (x, x) for all x ∈ M.
Now let A ⊆ T M be a field of contact cones on M. Then under the diffeomorphism above A is mapped to a subset
of M × M, i.e. a relation on M. This relation is symmetric, since vx ∈ A implies −vx ∈ A, and reflexive, since 0x ∈ A
for all x ∈ M. Thus, a field of contact cones on M becomes a coherence relation on M. If the field A is sufficiently
smooth (in any reasonable sense) then this relation reads

x y (mod A) if x and y may be joined by a geodesic tangent to A.

Moreover, if our diffeomorphism is onto then the image of the field of contact cones A⊥ is exactly the complementary
relation on M.
Now let Mi , Ai , i = 1, 2, be two coherent phase spaces and diffeomorphisms T Mi → Mi × Mi , i = 1, 2, be
specified. Assume that these diffeomorphisms are of the form described above. Then comparing the definitions (16)
and (17) of tensor and cotensor product of coherent spaces with the Definition 8 of tensor and cotensor product of
coherent phase spaces, we see that the correspondence between fields of contact cones and coherence relations agrees
with these operations.
Thus, it seems perfectly justified to speak about fields of contact cones as infinitesimal coherence relations.
In the next section we proceed at last to the interpretation of MLL in the category of coherent phase spaces.

9. Interpretation of formulas of MLL

We are going to give an interpretation of formulas (and sequents) of linear logic as coherent phase spaces. We note
that in order to interpret the multiplicative fragment no smoothness assumptions are needed. This is not a surprise in
view of the very weak expressive power of multiplicative fragment.
Recall that formulas of multiplicative linear logic are built from literals p0 , p0⊥ , p1 , p1⊥ , . . . , pn , pn⊥ , . . . by means
of binary connectives ⊗ (times) and ℘ (par). Linear negation A⊥ of a formula A is defined inductively:
(p⊥ )⊥ := p;
(A ⊗ B)⊥ := A⊥ ℘B ⊥ ; (A℘B)⊥ := A⊥ ⊗ B ⊥ .
Linear implication is defined by
A
B = A⊥ ℘B.

Definition 10. Multiplicative linear logic contains the following rules:

⵫A, A⊥ (Identity),
⵫ , A⵫A⊥ , 
(Cut),
⵫ ,
⵫A1 , . . . , An
, ∈ Sn (Exchange),
⵫A (1) , . . . , A (n)
⵫ , A, B ⵫ , A⵫B, 
(Par) (Times).
⵫ , A℘B ⵫ , A ⊗ B, 

Interpretation of formulas is an assignment p :  → [[]] of coherent phase spaces to MLL formulas satisfying
obvious conventions:
[[A ⊗ B]] = [[A]] ⊗ [[B]]; [[A]]℘[[B]] = [[A℘B]];
⊥ ⊥
[[A ]] = [[A]] ; [[A
B]] = [[A]]⊥ ℘[[B]].
In the following, however, we shall write  instead of [[]] in order to avoid cumbersome notations. In view of the
conventions above this shall not lead to confusion.
As usual we interpret the sequent ⵫A1 , . . . , An as the formula A1 ℘ . . . ℘An .
Next we are going to give an interpretation of proofs.
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 227

10. Interpretation of (cut-free) proofs

Further to the interpretation of formulas we are going to give an interpretation of proofs. Given the interpretation of
provable formula A, we assign to each proof s of A a state
of the corresponding coherent phase space A.
The first step is the interpretation of the identity axiom. This is of course just the identity morphism.

Lemma 2. Let M be a symplectic manifold. The diagonal submanifold

M = {(x, x) ∈ M × M|x ∈ M}

is a Lagrangian submanifold of M × M− . Furthermore, for any field of contact cones A on M the manifold M is a
state of A℘A⊥ .

Proof. It is immediate that M is a Lagrangian submanifold of M × M− .

Indeed for any y ∈ M , where y = (x, x), x ∈ M and two vectors v1 , v2 ∈ Ty M , it holds that vi = (ui , ui ),
ui ∈ Tx M, i = 1, 2. Hence, v1 , v2  = u1 , u2  − u1 , u2  = 0. Also, dim M = dim M = 21 dim M × M− . So M is
Lagrangian (by Note 3).
The second part of Lemma follows from the definition of cotensor product. 

Now, given a proof s of the sequent ⵫A (1) , . . . , A (n) , ∈ Sn , obtained from a proof s  of ⵫A1 , . . . , An by means
of the Exchange rule and s  being interpreted as a state
 of A1 ⊗ · · · ⊗ An , where Ai = Mi , Ai , the immersion

induced from
under the diffeomorphism A1 × · · · × An A (1) × · · · × A (n) is obviously a Lagrangian immersion
satisfying required specification.
If a proof s of ⵫ is obtained from s  by means of the Par rule, s  being interpreted as a manifold
 , it is a tautology
that the same
 works as an interpretation of s.
Finally, let a proof s of ⵫ , A ⊗ B,  be obtained by means of the Times rule from proofs s1 and s2 of ⵫ , A and
⵫B, , respectively. Let s1 , s2 be interpreted as states
1 and
2 of ⊗ A and B ⊗ , respectively, where = M , ,
A = MA , A, B = MB , B,  = M , . Obviously, we take as the interpretation of s the manifold
=
1 ×
2 ⊂
M × MA × MB × M .
We have to verify that
is a state of ℘ (A ⊗ B)℘.
Assume that this is not the case. Let v ∈ T
be such that 0  = v ∈ ⊥ ⊗(A⊥ ℘B ⊥ )⊗⊥ . We have v = (v1 , v2 , v3 , v4 ),
v1 ∈ T M , v2 ∈ T MA , v3 ∈ T MB , v4 ∈ T M , where v1 ∈ ⊥ , v4 ∈ ⊥ , (v2 , v3 ) ∈ A⊥ ℘B ⊥ .
Since (v1 , v2 ) ∈ T
1 , it follows that v2 ∈ / A⊥ —otherwise (v1 , v2 ) ∈ ⊥ ⊗ A⊥ , which contradicts the specification
of
1 unless v1 , v2 = 0.
In the same fashion v3 ∈ / B ⊥ or v3 , v4 = 0.
It follows that (v1 , v2 , v3 , v4 ) = 0 i.e. v = 0. So
is tangent to ℘ (A ⊗ B)℘. On the other hand,
is Lagrangian
as the product of two Lagrangian submanifolds (Note 4).

11. Interpretation of Cut. Composition of morphisms

It remains to give interpretation of the Cut rule, or rather to show that the composition of morphisms in the category
of coherent phase spaces is well defined.
This will follow from the following

Lemma 3. Let MX , X, MY , Y  and MZ , Z be coherent phase spaces. Let
and  be states of X
Y and Y
Z,
respectively.
Then the set  ◦
defined by (14) is a state of X
Z.

Proof. We will assume for simplicity that MY is connected. If this is not the case one has to repeat the argument below
for each connected component Mi of MY such that
×  meets MX × Mi × Mi × MZ .
Consider the manifold M = (MX )− × MY × (MY )− × MZ with the natural symplectic structure of the Cartesian
product. The manifold
=
1 ×
2 ⊂ M is a Lagrangian immersion in M.
228 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229

Consider the constraint submanifold

C = {(x, y1 , y2 , z) ∈ M|y1 = y2 }.
The manifold C is coisotropic. Indeed for any point c = (x, y, y, z) ∈ C the tangent space
Tc C = {(u, v1 , v2 , w) ∈ Tc M Tx MX × Ty MY × Ty MY × Tz MZ |v1 = v2 }
and after a straightforward calculation one sees that
orth(Tc C) = {(0, v, v, 0) ∈ Tc C|v ∈ Ty Y }.
Thus the null distribution C ⊥ is nothing else than

C⊥ = T ({x} × y × {z}) ⊆ T C. 
x∈MX ,z∈MZ

Hence, we deduce

Note 5. Each submanifold of M of the form {x} × Y × {z}, where x ∈ MX , z ∈ MZ , is a leaf of the foliation generated
by C ⊥ . Conversely each leaf of C ⊥ is of this form.

Proof. Routine. 

It follows that the set of leaves of C ⊥ equals MX × MZ and this foliation is simple,
C = C/C ⊥ MX × M Z . (18)
So by Lemma 1 the manifold C has a natural symplectic structure induced by natural projection and straightforward
computation shows that diffeomorphism (18) is actually a symplectomorphism.
Applying the same argument as the one used for the Times rule in previous section, we see that the spaces C ⊥ ∩ Tx C
and Tx
are of intersection zero for each point x ∈ C ∩
. It follows from an easy lemma below that C and
are
transversal.

Lemma 4. Let V be a symplectic vector space. Let W ⊆ V be a coisotropic subspace and L ⊆ V be Lagrangian.
Assume that L ∩ orth(W ) = {0}. Then W and L are transversal.

Proof. By Note (1) orth(L + W ) = orth(L) ∩ orth(W ) = L ∩ orth(W ) = {0}, hence L + W = orth({0})
= V. 

Thus by Lemma 1, we have that
:= (
1 ×
2 ) is a Lagrangian immersion in C MX × MZ .

Finally, it is easy to see that
is a state of X
Z.
Indeed, let u ∈
and u ∈
∩ C be such that (u) = u and u ∈ X ⊗ Z ⊥ . Then u = (u1 , ũ, ũ, u4 ), (u1 , ũ) ∈ T
1 ,
(ũ, u4 ) ∈ T
2 , and u = (u1 , u4 ). It follows that u1 ∈ X, u4 ∈ Z ⊥ . But either ũ ∈ Y ⊥ or ũ ∈ Y . The first possibility
contradicts to the specification of
1 , the second one contradicts to the specification of
2 .
Thus, the composition of morphisms is well defined. It is associative because the composition of relations is asso-
ciative.
Returning to the interpretation of linear logic it remains to show that this interpretation is invariant under Cut-
elimination. This is again completely routine.

Acknowledgments

I would like to thank Sergei Artemov for turning my attention to linear logic and Anil Nerode for his interest in this
work, many useful discussions and invaluable help with the organization of this paper. This work was presented on
FLOC02 in Copenhagen in July of 2002. I am grateful to the organizers of the conference for this possibility and to
many participants for their interest.
 S. Slavnov / Theoretical Computer Science 357 (2006) 215 – 229 229

References

[1] S. Bates, A. Weinstein, Lectures on the geometry of quantization, American Mathematical Society, Berkeley Center for Pure and Applied
Mathematics, 1997.
[2] R. Blute, I.T. Ivanov, Prakash Panangaden, Discrete quantum casual dynamics, available as gr-qc/0109053 at [Link], 2001.
[3] R.F. Blute, P.J. Scott, Linear Lauchli semantics, Ann. Pure Appl. Logic 77 (1996) 101–142.
[4] T. Ehrhard, On Koethe sequence spaces and linear logic, Math. Structures Comput. Sci., 2000, to appear.
[5] J.-Y. Girard, Linear logic, Theoret. Comput. Sci. 50 (1987) 1–102.
[6] J.-Y. Girard, Linear logic: its syntax and semantics, in: J.-Y. Girard, Y. Lafont, L. Regnier (Eds.), Advances in Linear Logic, Cambridge
University Press, Cambridge, 1995, Proc. Workshop on Linear Logic, Ithaca, NY, June 1993, pp. 1–42.
[7] J.-Y. Girard, Coherent Banach spaces: a continuous denotational semantics, Theoret. Comput. Sci. 227 (1–2) (1999) 275–297.
[8] S. Lang, Differential Manifolds, Addison Wesley, Reading, MA, 1972.
[9] P. Libermann, C.M. Marle, Symplectic geometry and analytical mechanics (translated from the French by Bertram Eugene Schwarzbach),
Mathematics and its Applications, Vol. 35, D. Reidel Publishing Co., Dordrecht, 1987.
[10] A. Weinstein, Symplectic geometry, Bull. Amer. Math. Soc. (N.S.) 5 (1981) 1–13.