Given formulas A and B, A is a retraction of B if there exist proofs of A |- B and B |- A which compose to the axiom on A, up to cut-elimination and axiom-expansion. This gives a natural notion of sub-tying, and corresponds to retractions in the category of proofs: objects are formulas, and morphisms proofs up to cut-elimination and axiom-expansion. While isomorphisms for multiplicative linear logic have been characterized (Balat & Di Cosmo gave a corresponding equational theory in 1999), and there is a well-known retraction (which is not an isomorphism), there is not even a conjecture on what the set of retractions could be.

I will present a work in progress about this problem, giving properties showing the problem should not be too hard, then solving the case "an atom X is a retraction of a formula B" using proof nets. Meanwhile, I will also show difficulties for solving the general case, as well as what happens in other fragments of linear logic.