Will Troiani

1. Linear logic and the Hilbert scheme

Multiplicative exponential linear logic has the multiplicative connectives tensor (\(\otimes\)) and par (\(\parr\)), with the exponential modality \(!\). The connectives have meanings familiar from tensor algebra: \(\otimes\) is the tensor product, and the linear implication \(A \multimap B = A^\perp \parr B\) is the space of linear maps. The exception is the exponential, which has the semantics of a cofree cocommutative coalgebra. Linear logic is in this way a formal language for constructions in a canonical nonlinear extension of tensor algebra. While the connectives are familiar to mathematicians, the fact that the structural maps associated to their universal properties can be used to encode algorithms is less familiar.

In Elimination and cut-elimination in multiplicative linear logic (with Murfet), each proof net \(\pi\) determines a polynomial ideal \(I(\pi)\). Cut-elimination then becomes variable elimination in commutative algebra.

In Linear Logic and the Hilbert Scheme (with Murfet), this picture is extended to shallow MELL by interpreting the exponential modality using the Hilbert scheme. Writing \(\mathbb{S}(X)\) for the scheme attached to a formula \(X\),

\[ \mathbb{S}(!X) \;=\; \operatorname{Hilb}\bigl(\mathbb{S}(X)\bigr), \]

where \(\operatorname{Hilb}(Y)\) parameterises closed subschemes of \(Y\). To each shallow proof net \(\pi\) we associate a closed immersion \(\iota_\pi : \mathbb{X}(\pi) \hookrightarrow \mathbb{S}(\pi)\) of locally projective schemes, and the main theorem of the paper says that for any cut-reduction \(\gamma : \pi \to \pi'\) between shallow proof nets there is an explicit isomorphism \(\mathbb{X}(\pi) \cong \mathbb{X}(\pi')\).

Geometrically, the multiplicative part of a proof net is a system of linear equations between atomic degrees of freedom, such as \(x - y, \; y - z\). The exponential introduces additional parameters \(\theta, \phi, \psi, \kappa, \ldots\) that parametrise a space of such equations,

\[ x - \theta y - \phi z, \quad y - \psi w - \kappa t, \quad \ldots, \]

and structural rules like contraction impose equations between these parameters, such as \(\theta = \phi\). In this way the exponential modality has the geometric content of equations between equations.

2. Matrix factorisations and quantum error correction

A second line studies cut-elimination inside the bicategory \(\mathrm{LG}\) of Landau–Ginzburg models. A matrix factorisation of a polynomial \(W \in k[x_1, \ldots, x_n]\) is a \(\mathbb{Z}/2\)-graded free module \(M\) with an odd endomorphism \(d\) satisfying \(d^2 = W \cdot \mathrm{id}\); these encode the singularity theory of the hypersurface \(\{W = 0\}\). Each proof net determines a matrix factorisation of a sum of potentials, and cut-elimination is bicategorical composition followed by the splitting of an idempotent \(e = e^2\), computed concretely by the Falling Roofs algorithm of Elimination and cut-elimination in multiplicative linear logic.

The central observation of Linear Logic and Quantum Error Correcting Codes (with Murfet) is that this idempotent splitting is the recovery map of a quantum error-correcting code. The image of \(e\) is the code space \(\mathcal{C}\); the components of the composed factorisation lying in \(\ker(e)\) are the errors; the idempotent itself is the recovery map \(\mathcal{R}\); and the correction condition \(\mathcal{R} \circ \mathcal{E}|_{\mathcal{C}} = \mathrm{Id}_{\mathcal{C}}\) holds because \(e\) is idempotent. No error-correction structure was imposed on the construction: the code space, error model, and recovery map are all determined by the proof theory.

The bicategorical setting is essential. The coherence and functoriality data of composition in \(\mathrm{LG}\) are absent from one-categorical models, and they are precisely what produces the idempotent and its splitting.

3. Singular learning theory

A more recent line applies algebraic-geometric methods to statistical learning, in collaboration with the singular learning theory programme at Timaeus.

A noisy Turing-machine code is a point \(w\) in a product of probability simplices, parameterising a smooth statistical model \(p(y \mid x, w)\). The smooth family arises from the differential treatment of copying and reuse in linear logic, in particular from the Sweedler semantics of the exponential modality. The Bayesian evidence integral

\[ Z_n \;=\; \int_W e^{-n L_n(w)} \, \varphi(w)\, dw \]

is the partition function of the synthesis problem. The model is typically singular: the solution set of exact codes is not a smooth manifold, and the relevant asymptotic theory is Watanabe’s singular learning theory.

In Programs as Singularities (with Murfet), the Taylor coefficients of a polynomial surrogate of the loss are controlled by error-syndrome combinatorics, and the real log canonical threshold (the learning coefficient) is computable from the multiplicities of the monomials produced by the Sweedler semantics. The exponential modality of linear logic produces precisely the singular geometry that controls Bayesian learning.

A second recent development, joint with Salazar, Snikkers, and Murfet, is Susceptibilities for Turing Machines. There the susceptibility to upweighting an input \(x\) is the covariance \(\chi_x(A) = -\operatorname{Cov}_\beta(A, \ell_x - L)\), a Bayesian form of the fluctuation-dissipation principle. Control-flow decompositions of a program produce rank-one off-diagonal blocks in the centred susceptibility matrix, and symmetries of subroutines appear as equivariances.

The susceptibility framework should extend from noisy Turing machines to neural networks, giving a mathematically grounded approach to interpretability: detecting when a learned computation is robust or brittle, identifying when two networks computing the same function differ in their internal structure, and quantifying the Bayesian complexity of the algorithms a model has actually learned. Singular learning theory is the right asymptotic framework for the model-selection, structural-inference, and interpretability problems that govern whether a learned system can be understood and controlled.