GoI for MELL: exponentials
The tensor product of Hilbert spaces
Recall that we work in the Hilbert space endowed with its canonical hilbertian basis denoted by
.
The space is the collection of sequences
of complex numbers such that
∑ | | xnp | 2 |
n,p |
converges. The scalar product is defined just as before:
-
.
If and
are vectors in H then their tensor is the sequence:
-
.
We define: so that enp is the sequence
of complex numbers given by enpij = δniδpj. By bilinearity of tensor we have:
Furthermore the system of vectors (enp) is a hilbertian basis of : the sequence
may be written:
-
.
An algebra isomorphism
Being both separable Hilbert spaces, H and are isomorphic. We will now define explicitely an iso based on partial permutations.
We fix, once for all, a bijection from couples of natural numbers to natural
numbers that we will denote by . For
example set
. Conversely, given
we denote by n(1) and
n(2) the unique integers such that
.
Remark:
just as it was convenient but actually not necessary to choose p and q so that pp * + qq * = 1 it is actually not necessary to have a bijection, a one-to-one mapping from into
would be sufficient for our purpose.
This bijection can be extended into a Hilbert space isomorphism by defining:
-
.
Now given an operator u on H we define the operator !u on H by:
-
.
Remark: The operator !u is defined by:
where denotes the operator on
defined by
for any x,y in H. However this notation must not be confused with the tensor of operators that was defined in the previous section in order to interpret the tensor rule of linear logic; we therefore will not use it.
One can check that given two operators u and v we have:
- !u!v = !(uv);
- !(u * ) = (!u) * .
Due to the fact that Φ is an isomorphism onto we also have !1 = 1; this however will not be used.
We therefore have that ! is a morphism on ; it is easily seen to be an iso (not onto though). As this is the crucial ingredient for interpreting the structural rules of linear logic, we will call it the copying iso.
Interpretation of exponentials
If we suppose that is a p-isometry generated by the partial permutation
then we have:
-
.
Thus is itself a p-isometry generated by the
partial permutation
, which shows that the proof space is stable under the copying iso.
Given a type A we define the type !A by: