Delia Kesner (PPS)

A Nonstandard Standardization Theorem

This talk focuses on standardization for the linear substitution calculus, a calculus with explicit substitutions being able to mimick reduction in lambda-calculus and linear logic proof-nets. For the latter, proof-nets can be formalized by means of a simple equational theory over the linear substitution calculus.

Our system can be equipped with a residual theory in the sense of Lévy, which is used to prove a left-to-right standardization theorem for the calculus with explicit substitutions but without the equational theory. Such a theorem, however, does not lift from the calculus with explicit substitutions to proof-nets, because the notion of left-to-right derivation is not preserved by the equational theory. We then relax the notion of left-to-right standard derivation, based on a total order on redexes, to a more liberal notion of standard derivation based on partial orders.

Our proofs rely on Melliès' axiomatic theory for standardization but we revisit some of its key concepts. In particular, we obtain uniqueness (modulo) of standard derivations in a different way and we provide a coinductive characterization of the key abstract notion of external redex. This last point is then used to give a simple proof that linear head reduction – a strategy having a central role in the theory of linear logic – is standard.

This is joint work with Beniamino Accattoli, Eduardo Bonelli and Carlos Lombardi.