Skip to Main content Skip to Navigation
Conference papers

Taylor expansion, β-reduction and normalization

Abstract : We introduce 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 introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of λ-terms. We show that the reduction of resource vectors contains the image, through Taylor expansion, of β-reduction in the algebraic λ-calculus, i.e. λ-calculus extended with weighted sums: in particular , Taylor expansion and normalization commute. We moreover exhibit a class of algebraic λ-terms, having a normalizable Taylor expansion, subsuming both arbitrary pure λ-terms, and normalizable algebraic λ-terms. For these, we prove the commutation of Taylor expansion and normalization in a more denotational sense, mimicking the Böhm tree construction.
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal-amu.archives-ouvertes.fr/hal-01834329
Contributor : Lionel Vaux Auclair <>
Submitted on : Tuesday, July 10, 2018 - 2:39:13 PM
Last modification on : Thursday, January 23, 2020 - 6:22:13 PM
Long-term archiving on: : Tuesday, October 2, 2018 - 8:41:13 AM

File

taylornf-csl.pdf
Publisher files allowed on an open archive

Identifiers

Collections

Citation

Lionel Vaux. Taylor expansion, β-reduction and normalization. 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. pp.39:1--39:16, ⟨10.4230/LIPIcs.CSL.2017.39⟩. ⟨hal-01834329⟩

Share

Metrics

Record views

80

Files downloads

104