Document Open Access Logo

Head reduction and normalization in a call-by-value lambda-calculus

Author Giulio Guerrieri

PDF
Thumbnail PDF

File

OASIcs.WPTE.2015.3.pdf
  • Filesize: 0.54 MB
  • 15 pages

Document Identifiers

Author Details

Giulio Guerrieri

Cite AsGet BibTex

Giulio Guerrieri. Head reduction and normalization in a call-by-value lambda-calculus. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 3-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/OASIcs.WPTE.2015.3

Abstract

Recently, a standardization theorem has been proven for a variant of Plotkin's call-by-value lambda-calculus extended by means of two commutation rules (sigma-reductions): this result was based on a partitioning between head and internal reductions. We study the head normalization for this call-by-value calculus with sigma-reductions and we relate it to the weak evaluation of original Plotkin's call-by-value lambda-calculus. We give also a (non-deterministic) normalization strategy for the call-by-value lambda-calculus with sigma-reductions.
Keywords
  • sequentialization
  • lambda-calculus
  • sigma-reduction
  • call-by-value
  • head reduction
  • internal reduction
  • (strong) normalization
  • evaluation
  • confluence

Metrics

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

References

  1. Beniamino Accattoli. Proof nets and the call-by-value lambda-calculus. In Delia Kesner and Petrucio Viana, editors, Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2012, volume 113 of EPTCS, pages 11-26, 2012. Google Scholar
  2. Beniamino Accattoli and Luca Paolini. Call-by-Value Solvability, Revisited. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming, volume 7294 of Lecture Notes in Computer Science, pages 4-16. Springer-Verlag, 2012. Google Scholar
  3. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North Holland, 1984. Google Scholar
  4. Alberto Carraro and Giulio Guerrieri. A Semantical and Operational Account of Call-by-Value Solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures, volume 8412 of Lecture Notes in Computer Science, pages 103-118. Springer-Verlag, 2014. Google Scholar
  5. Karl Crary. A Simple Proof of Call-by-Value Standardization. Technical Report CMU-CS-09-137, Carnegie Mellon University, 2009. Google Scholar
  6. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-102, 1987. Google Scholar
  7. Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. Standardization of a call-by-value lambda-calculus. In To appear in the Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA'15), 2015. Available at URL: http://www.pps.univ-paris-diderot.fr/~giuliog/standard.pdf.
  8. Hugo Herbelin and Stéphane Zimmermann. An Operational Account of Call-by-Value Minimal and Classical lambda-Calculus in "Natural Deduction" Form. In Pierre-Louis Curien, editor, Typed Lambda Calculi and Applications, volume 5608 of Lecture Notes in Computer Science, pages 142-156. Springer-Verlag, 2009. Google Scholar
  9. Peter J. Landin. A correspondence between ALGOL 60 and Church's lambda notation. Communications of the ACM, 8:89-101; 158-165, 1965. Google Scholar
  10. John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theoretical Computer Science, 228(1-2):175-210, 1999. Google Scholar
  11. Eugenio Moggi. Computational Lambda-Calculus and Monads. In Logic in Computer Science, pages 14-23. IEEE Computer Society, 1989. Google Scholar
  12. Luca Paolini. Call-by-Value Separability and Computability. In Antonio Restivo, Simona Ronchi Della Rocca, and Luca Roversi, editors, Italian Conference in Theoretical Computer Science, volume 2202 of Lecture Notes in Computer Science, pages 74-89. Springer-Verlag, 2002. Google Scholar
  13. Luca Paolini and Simona Ronchi Della Rocca. Call-by-value Solvability. Theoretical Informatics and Applications, 33(6):507-534, 1999. RAIRO Series, EDP-Sciences. Google Scholar
  14. Luca Paolini and Simona Ronchi Della Rocca. The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer-Verlag, 2004. Google Scholar
  15. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science, 1(2):125-159, 1975. Google Scholar
  16. Laurent Regnier. Lambda calcul et réseaux. PhD thesis, Université Paris 7, 1992. Google Scholar
  17. Laurent Regnier. Une équivalence sur les lambda-termes. Theoretical Computer Science, 126(2):281-292, April 1994. Google Scholar
  18. Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. Lisp and symbolic computation, 6(3-4):289-360, 1993. Google Scholar
  19. Masako Takahashi. Parallel reductions in lambda-calculus. Information and Computation, 118(1):120-127, 1995. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact