-
Normalizing the Taylor expansion of non-deterministic λ-terms, via parallel reduction of resource vectors
Authors:
Lionel Vaux
Abstract:
It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $λ$-terms that this operation commutes with normalization: the expansion of a $λ$-term is always normalizable and its normal form is the expansion of the Böhm tree of the term. We generalize this result to the non-uniform setting of the algebraic $λ$-calculus, i.e. $λ$-calculus extended with linear combinations o…
▽ More
It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $λ$-terms that this operation commutes with normalization: the expansion of a $λ$-term is always normalizable and its normal form is the expansion of the Böhm tree of the term. We generalize this result to the non-uniform setting of the algebraic $λ$-calculus, i.e. $λ$-calculus extended with linear combinations of terms. This requires us to tackle two difficulties: foremost is the fact that Ehrhard and Regnier's techniques rely heavily on the uniform, deterministic nature of the ordinary $λ$-calculus, and thus cannot be adapted; second is the absence of any satisfactory generic extension of the notion of Böhm tree in presence of quantitative non-determinism, which is reflected by the fact that the Taylor expansion of an algebraic $λ$-term is not always normalizable. Our solution is to provide a fine grained study of the dynamics of $β$-reduction under Taylor expansion, by introducing a notion of reduction on resource vectors, i.e. infinite linear combinations of resource $λ$-terms. The latter form the multilinear fragment of the differential $λ$-calculus, and resource vectors are the target of the Taylor expansion of $λ$-terms. We show the reduction of resource vectors contains the image of any $β$-reduction step, from which we deduce that Taylor expansion and normalization commute on the nose. We moreover identify a class of algebraic $λ$-terms, encompassing both normalizable algebraic $λ$-terms and arbitrary ordinary $λ$-terms: the expansion of these is always normalizable, which guides the definition of a generalization of Böhm trees to this setting.
△ Less
Submitted 30 July, 2019; v1 submitted 14 June, 2017;
originally announced June 2017.
-
Strong Normalizability as a Finiteness Structure via the Taylor Expansion of λ-terms
Authors:
Michele Pagani,
Christine Tasson,
Lionel Vaux
Abstract:
In the folklore of linear logic, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination. We make this intuition formal in the context of the non-deterministic λ-calculus by introducing a finiteness structure on resource terms, which is such that a λ-term is strongly normalizing iff the support…
▽ More
In the folklore of linear logic, a common intuition is that the structure of finiteness spaces, introduced by Ehrhard, semantically reflects the strong normalization property of cut-elimination. We make this intuition formal in the context of the non-deterministic λ-calculus by introducing a finiteness structure on resource terms, which is such that a λ-term is strongly normalizing iff the support of its Taylor expansion is finitary. An application of our result is the existence of a normal form for the Taylor expansion of any strongly normalizable non-deterministic λ-term.
△ Less
Submitted 23 March, 2016;
originally announced March 2016.
-
Transport of finiteness structures and applications
Authors:
Christine Tasson,
Lionel Vaux
Abstract:
We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: these include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the li…
▽ More
We describe a general construction of finiteness spaces which subsumes the interpretations of all positive connectors of linear logic. We then show how to apply this construction to prove the existence of least fixpoints for particular functors in the category of finiteness spaces: these include the functors involved in a relational interpretation of lazy recursive algebraic datatypes along the lines of the coherence semantics of system T.
△ Less
Submitted 14 December, 2016; v1 submitted 21 April, 2010;
originally announced April 2010.
