Document Open Access Logo

Taylor Expansion, lambda-Reduction and Normalization

Author Lionel Vaux

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2017.39.pdf
  • Filesize: 0.58 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • lambda-calculus
  • non-determinism
  • normalization
  • denotational semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

We introduce a notion of reduction on resource vectors, i.e. infinite linear combinations of resource lambda-terms. The latter form the multilinear fragment of the differential lambda-calculus introduced by Ehrhard and Regnier, and resource vectors are the target of the Taylor expansion of lambda-terms.

We show that the reduction of resource vectors contains the image, through Taylor expansion, of beta-reduction in the algebraic lambda-calculus, i.e. lambda-calculus extended with weighted sums: in particular, Taylor expansion and normalization commute.

We moreover exhibit a class of algebraic lambda-terms, having a normalizable Taylor expansion, subsuming both arbitrary pure lambda-terms, and normalizable algebraic lambda-terms. For these, we prove the commutation of Taylor expansion and normalization in a more denotational sense, mimicking the Böhm tree construction.

Cite As Get BibTex

Lionel Vaux. Taylor Expansion, lambda-Reduction and Normalization. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 39:1-39:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.CSL.2017.39

Author Details

Lionel Vaux

References

  1. M. Alberti. On operational properties of quantitative extensions of λ-calculus. PhD thesis, Aix Marseille Université and Università di Bologna, 2014. URL: https://hal.inria.fr/tel-01096067.
  2. P. Arrighi and G. Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In RTA 2008, volume 5117 of LNCS. Springer, 2008. URL: http://dx.doi.org/10.1007/978-3-540-70590-1_2,
  3. A. Bucciarelli, T. Ehrhard, and G. Manzonetto. Not enough points is enough. In CSL 2007, volume 4646 of LNCS. Springer Berlin, 2007. Google Scholar
  4. V. Danos and T. Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 2011. URL: http://dx.doi.org/10.1016/j.ic.2011.02.001.
  5. D. de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. Math. Struct. in Comp. Sci., 2017. Google Scholar
  6. U. de' Liguoro and A. Piperno. Nondeterministic extensions of untyped λ-calculus. Information and Computation, 1995. Google Scholar
  7. A. Díaz-Caro. Du typage vectoriel. PhD thesis, Université de Grenoble, France, 2011. Google Scholar
  8. T. Ehrhard. On Köthe sequence spaces and linear logic. Math. Struct. in Comp. Sci., 2001. Google Scholar
  9. T. Ehrhard. Finiteness spaces. Math. Struct. in Comp. Sci., 15(4):615-646, 2005. Google Scholar
  10. T. Ehrhard. A finiteness structure on resource terms. In LICS 2010. IEEE Computer Society, 2010. URL: http://dx.doi.org/10.1109/LICS.2010.38.
  11. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theor. Comp. Sci., 2003. Google Scholar
  12. T. Ehrhard and L. Regnier. Böhm trees, Krivine’s machine and the Taylor expansion of λ-terms. In CiE 2006, volume 3988 of LNCS. Springer, 2006. URL: http://dx.doi.org/10.1007/11780342_20.
  13. T. Ehrhard and L. Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comp. Sci., 2008. URL: http://dx.doi.org/10.1016/j.tcs.2008.06.001.
  14. J.-Y. Girard. The system F of variable types, fifteen years later. Theor. Comp. Sci., 1986. URL: http://dx.doi.org/10.1016/0304-3975(86)90044-7.
  15. J.-Y. Girard. Normal functors, power series and lambda-calculus. Annals of Pure and Applied Logic, 1988. Google Scholar
  16. R. Hasegawa. The generating functions of lambda terms. In First Conference of the Centre for Discrete Mathematics and Theoretical Computer Science, Auckland, New Zealand, December, 9-13, 1996. Springer-Verlag, Singapore, 1996. Google Scholar
  17. A. Joyal. Foncteurs analytiques et espèces de structures. In Proceedings of the "Colloque de combinatoire énumérative", Montréal, May 28 - June 1, 1985. Springer, 1986. URL: http://dx.doi.org/10.1007/BFb0072514.
  18. J. R. Kennaway, J. W. Klop, M. R. Sleep, and F. J. de Vries. Infinitary lambda calculus. Theor. Comp. Sci., 1997. Google Scholar
  19. J. Laird. Fixed points in quantitative semantics. In LICS 2016. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2934569.
  20. J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. Weighted relational models of typed lambda-calculi. In LICS 2013. IEEE Computer Society, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.36.
  21. T. Leventis. Probabilistic λ-theories. PhD thesis, Aix-Marseille Université, 2016. Google Scholar
  22. M. Pagani, C. Tasson, and L. Vaux. Strong normalizability as a finiteness structure via the taylor expansion of λ-terms. In FOSSACS 2016, volume 9634 of LNCS. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_24.
  23. Takeshi Tsukada, Kazuyuki Asada, and Luke Ong. Generalised species of rigid resource terms. In Joel Ouaknine, editor, Proceedings of the 32nd Annual IEEE Symposium on Logic in Computer Science, LICS 2017, June 2017. To appear. Google Scholar
  24. L. Vaux. The algebraic lambda calculus. Math. Struct. in Comp. Sci., 2009. URL: http://dx.doi.org/10.1017/S0960129509990089.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact