Document Open Access Logo

A Lambda Calculus Satellite (Invited Talk)

Author Giulio Manzonetto

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.3.pdf
  • Filesize: 0.78 MB
  • 14 pages

Document Identifiers

Author Details

Giulio Manzonetto
  • Université Sorbonne Paris Nord, LIPN, UMR 7030, CNRS, F-93430 Villetaneuse, France

Acknowledgements

I want to thank Henk Barendregt for accepting to embark with me in the ambitious project of writing a "sequel" of his yellow book The Lambda Calculus, for all the pleasant gatherings and interesting discussions about λ-calculus, consciousness and life. Both Henk and I are grateful to Stefano Guerrini and Vincent Padovani for their contributions to the Satellite.

Cite As Get BibTex

Giulio Manzonetto. A Lambda Calculus Satellite (Invited Talk). In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 3:1-3:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.3

Abstract

We shortly summarize the contents of the book "A Lambda Calculus Satellite", presented at the 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023).

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • λ-calculus
  • rewriting
  • denotational models
  • equational theories

Metrics

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

References

  1. Andrea Asperti and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998. Google Scholar
  2. Andrea Asperti and Giuseppe Longo. Categories, types and structures: an introduction to category theory for the working computer scientist. MIT Press, Cambridge, MA, 1991. Google Scholar
  3. Henk P. Barendregt. RTA list, Problem #97: Is the word problem for the S-combinator decidable?, 1975. See URL: https://www.win.tue.nl/rtaloop/problems/97.html.
  4. Henk P. Barendregt. The type free lambda calculus. In J. Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 1091-1132. North-Holland, Amsterdam, 1977. Google Scholar
  5. Henk P. Barendregt. The lambda-calculus, its syntax and semantics. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984. Google Scholar
  6. Henk P. Barendregt. Constructive proofs of the range property in lambda calculus. Theoretical Computer Science, 121(1-2):59-69, 1993. A collection of contributions in honour of Corrado Böhm on the occasion of his 70th birthday. Google Scholar
  7. Henk P. Barendregt, Jan A. Bergstra, Jan Willem Klop, and Henri Volken. Degrees of sensible lambda theories. J. Symb. Log., 43(1):45-55, 1978. Google Scholar
  8. Henk P. Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. J. Symb. Log., 48(4):931-940, 1983. URL: https://doi.org/10.2307/2273659.
  9. Henk P. Barendregt and Giulio Manzonetto. A Lambda Calculus Satellite. College Publications, 2022. URL: https://www.collegepublications.co.uk/logic/mlf/?00035.
  10. Alessandro Berarducci. Infinite λ-calculus and non-sensible models. In Marcel Dekker, editor, Logic and Algebra (Pontignano, 1994), volume 180, pages 339-377, New York, 1996. Google Scholar
  11. Corrado Böhm. Alcune proprietà delle forme β-η-normali nel λ-K-calcolo. Pubblicazioni dell'istituto per le applicazioni del calcolo, 696:1-19, 1968. Lavoro eseguito all'INAC. Google Scholar
  12. Corrado Böhm and Mariangiola Dezani-Ciancaglini. Combinatorial problems, combinator equations and normal forms. In Jacques Loeckx, editor, Automata, Languages and Programming, 2nd Colloquium, University of Saarbrücken, Germany, July 29 - August 2, 1974, Proceedings, volume 14 of Lecture Notes in Computer Science, pages 185-199. Springer, 1974. Google Scholar
  13. Corrado Böhm and Wolf Gross. Introduction to the CUCH. Automata theory, pages 35-65, 1966. Reprinted in Pubblicazioni dell'Istituto Nazionale per le Applicazioni del Calcolo, ser. 11 no. 669, Rome 1966. Google Scholar
  14. Flavien Breuvart, Giulio Manzonetto, Andrew Polonsky, and Domenico Ruoppolo. New results on Morris’s observational theory: The benefits of separating the inseparable. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 15:1-15:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.15.
  15. Antonio Bucciarelli and Thomas Ehrhard. Sequentiality and strong stability. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 138-145. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151638.
  16. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In Jacques Duparc and Thomas A. Henzinger, editors, Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings, volume 4646 of Lecture Notes in Computer Science, pages 298-312. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74915-8_24.
  17. Felice Cardone and J. Roger Hindley. Lambda-calculus and combinators in the 20th century. In Dov M. Gabbay and John Woods, editors, Logic from Russell to Church, volume 5 of Handbook of the History of Logic, pages 723-817. Elsevier, 2009. URL: https://doi.org/10.1016/S1874-5857(09)70018-4.
  18. Alonzo Church. A set of postulates for the foundation of logic. Annals of Mathematics, 33(2):346-366, 1932. Google Scholar
  19. Alonzo Church. A set of postulates for the foundation of logic (second paper). Annals of Mathematics, 34:839-864, 1933. Google Scholar
  20. Alonzo Church and J. B. Rosser. Some properties of conversion. Transactions of the American Mathematical Society, 39(3):472-482, 1936. Google Scholar
  21. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, 1980. Google Scholar
  22. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms and 𝒟_∞-lambda-models. Inf. Comput., 72(2):85-116, 1987. URL: https://doi.org/10.1016/0890-5401(87)90042-3.
  23. Haskell B. Curry and Robert Feys. Combinatory logic. Volume I. Number 1 in Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1958. Google Scholar
  24. Lukasz Czajka. A new coinductive confluence proof for infinitary lambda calculus. Log. Methods Comput. Sci., 16(1), 2020. URL: https://doi.org/10.23638/LMCS-16(1:31)2020.
  25. David Edward. The Church-Rosser Theorem. Ph.D. thesis, Cornell Univ., 1965. Informally circulated 1963. 673 pp. Obtainable from University Microfilms Inc., Ann Arbor, Michigan, U.S.A., Publication No. 66-41. Google Scholar
  26. Jörg Endrullis and Roel de Vrijer. Reduction under substitution. In Andrei Voronkov, editor, Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings, volume 5117 of Lecture Notes in Computer Science, pages 425-440. Springer, 2008. Google Scholar
  27. Jörg Endrullis, Dimitri Hendriks, Jan Willem Klop, and Andrew Polonsky. Clocked lambda calculus. Math. Struct. Comput. Sci., 27(5):782-806, 2017. URL: https://doi.org/10.1017/S0960129515000389.
  28. Jörg Endrullis, Jan Willem Klop, and Andrew Polonsky. Reduction Cycles in Lambda Calculus and Combinatory Logic. In Jan van Eijck, Rosalie Iemhoff, and Joost J. Joosten, editors, Liber Amicorum Alberti - A Tribute to Albert Visser. College Publications, 2016. Google Scholar
  29. Enno Folkerts. Kongruenz von unlösbaren Lambda-Termen. Ph.D. thesis, University WWU-Münster, 1995. In German. Google Scholar
  30. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  31. J. Roger Hindley and Giuseppe Longo. Lambda calculus models and extensionality. Z. Math. Logik Grundlag. Math, 26:289-310, 1980. Google Scholar
  32. R. Hindley. Reductions of residuals are finite. Transactions of the American Mathematical Society, 240:345-361, 1978. Google Scholar
  33. J. Martin E. Hyland. A syntactic characterization of the equality in some models for the λ-calculus. Journal London Mathematical Society (2), 12(3):361-370, 1975. Google Scholar
  34. Martin Hyland. A simple proof of the Church-Rosser Theorem. Technical report, Oxford University, 1973. 7 pp. Google Scholar
  35. Benedetto Intrigila. Non-existent Statman’s double fixedpoint combinator does not exist, indeed. Inf. Comput., 137(1):35-40, 1997. URL: https://doi.org/10.1006/inco.1997.2633.
  36. Benedetto Intrigila. TLCA list, Problem #25: How many fixed points can a combinator have?, 2000. See http://tlca.di.unito.it/opltlca/. First raised in [Benedetto Intrigila and E. Biasone, 2000].
  37. Benedetto Intrigila and E. Biasone. On the number of fixed points of a combinator in lambda calculus. Mathematical Structures in Computer Science, 10(5):595-615, 2000. Google Scholar
  38. Benedetto Intrigila, Giulio Manzonetto, and Andrew Polonsky. Refutation of Sallé’s longstanding conjecture. In Dale Miller, editor, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, volume 84 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.FSCD.2017.20.
  39. Benedetto Intrigila and Richard Statman. Solution of a problem of Barendregt on sensible λ-theories. Log. Methods Comput. Sci., 2(4), 2006. URL: https://doi.org/10.2168/LMCS-2(4:5)2006.
  40. Richard Kennaway, Jan Willem Klop, M. Ronan Sleep, and Fer-Jan de Vries. Infinitary lambda calculus. Theor. Comput. Sci., 175(1):93-125, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00171-5.
  41. Jan Willem Klop. Reduction cycles in Combinatory Logic. In Hindley and Seldin, editors, Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pages 193-214. Academic Press, San Diego, 1980. Google Scholar
  42. Christiaan Peter Jozef Koymans. Models of the lambda calculus. Inf. Control., 52(3):306-332, 1982. URL: https://doi.org/10.1016/S0019-9958(82)90796-3.
  43. Dexter Kozen and Alexandra Silva. Practical coinduction. Math. Struct. Comput. Sci., 27(7):1132-1152, 2017. Google Scholar
  44. Jean-Jacques Lévy. An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus. Theor. Comput. Sci., 2(1):97-114, 1976. URL: https://doi.org/10.1016/0304-3975(76)90009-8.
  45. Jean-Jacques Lévy. Réductions correctes et optimales dans le λ-calcul. Thèse d'état, Université Paris-Diderot (Paris 7), 1978. In French. Google Scholar
  46. Stefania Lusin and Antonino Salibra. The lattice of lambda theories. J. Log. Comput., 14(3):373-394, 2004. Google Scholar
  47. Giulio Manzonetto, Andrew Polonsky, Alexis Saurin, and Jakob Grue Simonsen. The fixed point property and a technique to harness double fixed point combinators. Journal of Logic and Computation, 2019. URL: https://doi.org/10.1093/logcom/exz013.
  48. Giulio Manzonetto and Antonino Salibra. From lambda-calculus to universal algebra and back. In Edward Ochmanski and Jerzy Tyszkiewicz, editors, Mathematical Foundations of Computer Science 2008, 33rd International Symposium, MFCS 2008, Torun, Poland, August 25-29, 2008, Proceedings, volume 5162 of Lecture Notes in Computer Science, pages 479-490. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85238-4_39.
  49. James Hiram Morris. Lambda calculus models of programming languages. Ph.D. thesis, Massachusetts Institute of Technology (MIT), 1968. Google Scholar
  50. Hans Mulder. On a conjecture by J.W. Klop. Unpublished, 1986. Google Scholar
  51. Rob P. Nederpelt, J. Herman Geuvers, and Roel C. de Vrijer, editors. Selected Papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1994. Google Scholar
  52. Gordon D. Plotkin. A set-theoretical definition of application. Technical Report MIP-R-95, School of artificial intelligence, 1971. Google Scholar
  53. Gordon D. Plotkin. The lambda-calculus is ω-incomplete. Journal of Symbolic Logic, 39(2):313-317, 1974. Google Scholar
  54. Andrew Polonsky. Proofs, Types and Lambda Calculus. Ph.D. thesis, University of Bergen, Norway, 2011. Google Scholar
  55. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus: A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin Heidelberg, 2004. Google Scholar
  56. Dana S. Scott. Continuous lattices. In Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lecture Notes in Mathematics, pages 97-136. Springer, 1972. Google Scholar
  57. Dana S. Scott. The language LAMBDA (abstract). J. Symb. Log., 39:425-427, 1974. Google Scholar
  58. Shoji Sekimoto and Sachio Hirokawa. One-step recurrent terms in lambda-beta-calculus. Theor. Comput. Sci., 56:223-231, 1988. URL: https://doi.org/10.1016/0304-3975(88)90079-5.
  59. Raymond Smullyan. To Mock A Mockingbird. Alfred A. Knopf, New York, 1985. Google Scholar
  60. Richard Statman. There is no hyper-recurrent S,K combinator. Technical Report 91-133, Department of Mathematics, Carnegie Mellon University, Pittsburgh, PA, 1991. Google Scholar
  61. Richard Statman. RTA list, Problem #52: Is there a fixed point combinator Y for which Y ↔^* Y(SI)?, 1993. See https://www.win.tue.nl/rtaloop/. First raised in [Richard Statman, 1993].
  62. Richard Statman. RTA list, Problem #53: Are there hyper-recurrent combinators?, 1993. See https://www.win.tue.nl/rtaloop/. First raised in [Richard Statman, 1993].
  63. Richard Statman. Some examples of non-existent combinators. Theor. Comput. Sci., 121(1&2):441-448, 1993. Google Scholar
  64. Richard Statman and Henk P. Barendregt. Applications of Plotkin-terms: partitions and morphisms for closed terms. Journal of Functional Programming, 9(5):565-575, 1999. Google Scholar
  65. Diederik van Daalen. The Language Theory of Automath. Ph.D. thesis, Technical University Eindhoven, 1980. Large parts of this thesis, including the treatment of RuS, have been reproduced in [51]. Google Scholar
  66. Albert Visser. Numerations, λ-calculus, and arithmetic. In Hindley and Seldin, editors, Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pages 259-284. Academic Press, San Diego, 1980. Google Scholar
  67. Christopher P. Wadsworth. The relation between computational and denotational properties for Scott’s 𝒟_∞-models of the lambda-calculus. SIAM J. Comput., 5(3):488-521, 1976. URL: https://doi.org/10.1137/0205036.
  68. Johannes Waldmann. The Combinator S. Ph.D. thesis, Friedrich-Schiller-Universität Jena, 1998. 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 About DROPS Imprint Privacy Contact