GoI for MELL: exponentials

From LLWiki
Jump to: navigation, search

The tensor product of Hilbert spaces

Recall that we work in the Hilbert space H=\ell^2(\mathbb{N}) endowed with its canonical hilbertian basis denoted by (e_k)_{k\in\mathbb{N}}.

The space H\tens H is the collection of sequences (x_{np})_{n,p\in\mathbb{N}} of complex numbers such that

| xnp | 2

converges. The scalar product is defined just as before:

\langle (x_{np}), (y_{np})\rangle = \sum_{n,p} x_{np}\bar y_{np}.

If x = (x_n)_{n\in\mathbb{N}} and y = (y_p)_{p\in\mathbb{N}} are vectors in H then their tensor is the sequence:

x\tens y = (x_ny_p)_{n,p\in\mathbb{N}}.

We define: e_{np} = e_n\tens e_p so that enp is the sequence (e_{npij})_{i,j\in\mathbb{N}} of complex numbers given by enpij = δniδpj. By bilinearity of tensor we have:

x\tens y = \left(\sum_n x_ne_n\right)\tens\left(\sum_p y_pe_p\right) = 
  \sum_{n,p} x_ny_p\, e_n\tens e_p = \sum_{n,p} x_ny_p\,e_{np}

Furthermore the system of vectors (enp) is a hilbertian basis of H\tens H: the sequence x=(x_{np})_{n,p\in\mathbb{N}} may be written:

x = \sum_{n,p\in\mathbb{N}}x_{np}\,e_{np}
          = \sum_{n,p\in\mathbb{N}}x_{np}\,e_n\tens e_p.

An algebra isomorphism

Being both separable Hilbert spaces, H and H\tens H 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 (n,p)\mapsto\langle n,p\rangle. For example set \langle n,p\rangle = 2^n(2p+1) - 1. Conversely, given n\in\mathbb{N} we denote by n(1) and n(2) the unique integers such that \langle n_{(1)},
n_{(2)}\rangle = n.

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 \mathbb{N}^2 into \mathbb{N} would be sufficient for our purpose.

This bijection can be extended into a Hilbert space isomorphism \Phi:H\tens H\rightarrow H by defining:

e_n\tens e_p = e_{np} \mapsto e_{\langle n,p\rangle}.

Now given an operator u on H we define the operator !u on H by:

!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p)).

Remark: The operator !u is defined by:

!u = \Phi\circ (1\tens u)\circ \Phi^{-1}

where 1\tens u denotes the operator on H\tens H defined by (1\tens u)(x\tens y) = x\tens u(y) 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 \mathcal{B}(H); 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 u = u_\varphi is a p-isometry generated by the partial permutation \varphi then we have:

!u(e_{\langle n,p\rangle}) = \Phi(e_n\tens u(e_p)) = \Phi(e_n\tens e_{\varphi(p)}) = e_{\langle n,\varphi(p)\rangle}.

Thus !u_\varphi is itself a p-isometry generated by the partial permutation !\varphi:n\mapsto \langle n_{(1)}, \varphi(n_{(2)})\rangle, which shows that the proof space is stable under the copying iso.

Given a type A we define the type !A by:

!A = \{!u, u\in A\}\biorth
Personal tools