GoI for MELL: the *-autonomous structure
Recall that when u and v are p-isometries we say they are dual when uv is nilpotent, and that denotes the set of nilpotent operators. A type is a subset of that is equal to its bidual. In particular is a type for any . We say that X generates the type .
The tensor and the linear application
If u and v are two p-isometries summing them doesn't in general produces a p-isometry. However as pup * and qvq * have disjoint domains and disjoint codomains it is true that pup * + qvq * is a p-isometry. Given two types A and B, we thus define their tensor by:
Note the closure by bidual to make sure that we obtain a type.
From what precedes we see that is generated by the internalizations of operators on of the form:
Remark: This so-called tensor resembles a sum rather than a product. We will stick to this terminology though because it defines the interpretation of the tensor connective of linear logic.
The linear implication is derived from the tensor by duality: given two types A and B the type is defined by:
Unfolding this definition we get:
Given a type A we are to find an operator ι in type , thus satisfying:
An easy solution is to take ι = pq * + qp * . In this way we get ι(pup * + qvq * ) = qup * + pvq * . Therefore (ι(pup * + qvq * ))2 = quvq * + pvup * , from which one deduces that this operator is nilpotent iff uv is nilpotent. It is the case since u is in A and v in .
It is interesting to note that the ι thus defined is actually the internalization of the operator on given by the matrix:
We will see once the composition is defined that the ι operator is the interpretation of the identity proof, as expected.
The execution formula, version 1: application
Note that the hypothesis that u11v is nilpotent entails that the sum
is actually finite. It would be enough to assume that this sum converges. For simplicity we stick to the nilpotency condition, but we should mention that weak nilpotency would do as well.
As an example if we compute the application of the interpretation of the identity ι in type to the operator then we have:
Now recall that ι = pq * + qp * so that ι11 = ι22 = 0 and ι12 = ι21 = 1 and we thus get:
- App(ι,v) = v
The tensor rule
Let now A,A',B and B' be types and consider two operators u and u' respectively in and . We define an operator by:
Once again the notation is motivated by linear logic syntax and is contradictory with linear algebra practice since what we denote by actually is the internalization of the direct sum .
Indeed if we think of u and u' as the internalizations of the matrices:
then we may write:
Thus the components of are given by:
and we see that is actually the internalization of the matrix:
We are now to show that if we suppose uand u' are in types and , then is in . For this we consider v and v' respectively in A and A', so that pvp * + qv'q * is in , and we show that .
Since u and u' are in and we have that u11v and u'11v' are nilpotent and that App(u,v) and App(u',v') are respectively in B and B', thus:
But we have:
Therefore is nilpotent. So we can compute :
thus lives in .
Other monoidal constructions
Let A and B be some types; we have:
Indeed, means that for any v and w in respectively A and we have which is exactly the definition of .
We will denote the operator:
where uij is given by externalization. Therefore the externalization of is:
- where is defined by .
From this we deduce that and that .
Let σ be the operator:
- σ = ppq * q * + pqp * q * + qpq * p * + qqp * p * .
One can check that σ is the internalization of the operator S on defined by: . In particular the components of σ are:
- σ11 = σ22 = 0;
- σ12 = σ21 = pq * + qp * .
Let A and B be types and u and v be operators in A and B. Then pup * + qvq * is in and as σ11.(pup * + qvq * ) = 0 we may compute:
But , thus we have shown that:
We get distributivity by considering the operator:
- δ = ppp * p * q * + pqpq * p * q * + pqqq * q * + qppp * p * + qpqp * q * p * + qqq * q * p *
that is similarly shown to be in type for any types A, B and C.
Similarly we get weak distributivity thanks to the operators:
- δ1 = pppp * q * + ppqp * q * q * + pqq * q * q * + qpp * p * p * + qqpq * p * p * + qqqq * p * and
- δ2 = ppp * p * q * + pqpq * p * q * + pqqq * q * + qppp * p * + qpqp * q * p * + qqq * q * p * .
Given three types A, B and C then one can show that:
- δ1 has type and
- δ2 has type .
Execution formula, version 2: composition
Let A, B and C be types and u and v be operators respectively in types and .
As usual we will denote uij and vij the operators obtained by externalization of u and v, eg, u11 = p * up, ...
As u is in we have that ; similarly as , thus , we have . Thus u22v11 is nilpotent.
We define the operator Comp(u,v) by:
This is well defined since u11v22 is nilpotent. As an example let us compute the composition of u and ι in type ; recall that ιij = δij, so we get:
- Comp(u,ι) = pu11p * + pu12q * + qu21p * + qu22q * = u
Similar computation would show that Comp(ι,v) = v (we use pp * + qq * = 1 here).
Coming back to the general case we claim that Comp(u,v) is in : let a be an operator in A. By computation we can check that:
- App(Comp(u,v),a) = App(v,App(u,a)).
Now since u is in , App(u,a) is in B and since v is in , App(v,App(u,a)) is in C.
If we now consider a type D and an operator w in then we have:
- Comp(Comp(u,v),w) = Comp(u,Comp(v,w)).
Putting together the results of this section we finally have: