Church’s formal system of lambda-calculus Duccio Pianigiani University of Siena, Italy This is a section of Lectures in Proof Theory and Complexity(DOI: 10.36253/979-12-215-0778-2) by Duccio Pianigiani Firenze University Press, USiena Press Florence 2025 https://doi.org/10.36253/979-12-215-0778-2.06

Available for academic research purposes

Open Access

Copyright Author(s)

Content licence CC BY-SA 4.0

Metadata licence CC0 1.0

This is original content, published for academic research purposes

 Digital edition XML powered by Booksflow

A. Church in 1936 introduced a formal system based on the operations of function abstraction and application, called the lambda calculus and defined the notion of computable function in this system. Church’s original goal was to construct a formal system for the foundations of mathematics based on functions together with a set of logical notions. When this system was discovered to be inconsistent, Church then separated out the consistent subsystem that is now called lambda calculus and concentrated on it. We we will discuss the three-way isomorphism between typed lambda calculus, intuitionistic Proof Theory and Cartesian Closed Categories of category theory, widely used in Computer Science, sometimes referred as the “computational trinitarianism”.

 Lambda calculus Type Theory Cartesian Closed Categories normalization

It is available online at https://doi.org/10.36253/979-12-215-0778-2.06

References Abramsky, Samson and Tzevelekos, Nikos. 2011. Introduction to Categories and Categorical Logic. Oxford University Computing Laboratory. ArXiv : 1102.1313. Amadio, Roberto and Curien, Pierre-Louis. 1996. Domains and Lambda-Calculi. Cambridge: Cambridge University Press. Asperti, Andrea. 1998. “Light affine logic” . In Proc. 13th IEEE Annual Symp. on Logic in Computer Science 300-308. Washington: IEEE Computer Society. Asperti, Andrea and Roversi, Luca. 2002. “Intuitionistic Light Affine Logic” . ACM Trans. Comput. Logic 3 (1): 137-175. 10.1145/504077.504081 Awodey, Steve. 1996. “Structure in mathematics and logic: A categorical perspective” . Philosophia Mathematica 4 (3): 209-237. 10.1093/philmat/4.3.209 Awodey, Steve. 2008. Category Theory (II edition). Oxford: Oxford University Press. Baillot, Patrick. 2004. “Type inference for light affine logic via constraints on words” . Theoretical Computer Science 328 (3): 289-323. 10.1016/j.tcs.2004.08.014 Baillot, Patrick and Mogbil, Virgile. 2004. “Soft lambda-Calculus: A Language for Polynomial Time Computation” . In I. Walukiewicz (editors) Foundations of Software Science and Computation Structures 27-41. FoSSaCS 2004. Lecture Notes in Computer Science 2987. Berlin: Springer. 10.1007/978-3-540-24727-2_4 Barendregt, Henk P. 1984. The Lambda Calculus: Its Syntax and Semantics, second, revised edition. Amsterdam: North-Holland. Bellantoni, Stephen and Cook, Stephen. 1992. “A new recursion-theoretic characterization of the polytime functions”. Computational Complexity 2: 97-110. 10.1007/BF01201998 Bishop, Erret. 1970. “Mathematics as a numerical language” In A. Kino, J. Myhill and R. E. Vesley (editors) Intuitionism and Proof Theory 53-71. Amsterdam: North-Holland. 10.1007/978-1-4020-8926-8_13 Barendregt, Henk P. 1992. “Representing undefined in Lambda calculus” . Journal of Func- tional Programming 2 (3): 367-374. 10.1017/S0956796800000447 Church, Alonso. 1936. “An unsolvable Problem of Elementary Number Theory”. American Journal of Mathematics 58 (2): 345-363. 10.2307/2371045 Crole, Roy. 1994. Categories for Types. Cambridge: Cambridge University Press. 10.1017/CBO9781139172707 Girard, Jean-Yves and Lafont, Yves and Taylor, Paul. 1989. Proofs and types. Cambridge: Cambridge University Press. Gödel, Kurt. 1958. “Über eine bisher noch nicht benützte Erweiterung des finiten Standpunk- tes” . Dialectica 12 (3): 280. Gödel, Kurt. 1972. “On an Extension of Finitary Mathematics Which Has Not Yet Been Used” . Revised and expanded English version of 1958, first published in Gödel’s Collected Works (1986-2005) II: 271-280. Harper, Robert. 2011. “Existential Type” . https://existentialtype.wordpress.com/2011/03/27/the- Holy-trinity/ Lafont, Yves. 2004. “Soft linear logic and polynomial time” . Theoretical Computer Science, 318 (1-2): 163-180. 10.1016/j.tcs.2003.10.018 Lambek, Joachim and Scott, Philip J. 1986. Introduction to Higher-Order Categorical Logic. Cambridge: Cambridge University Press. Leivant, Daniel and Marion, Jean-Yves. 1993. “Lambda-calculus characterisations of polytime”. Fundamenta Informaticae 19: 167-184. 10.3233/FI-1993-191-207 Krivine, Jean Louis. 1993. Lambda-calculus, Types and Models. London: Ellis Horwood. Nerode, Anil and Odifreddi, Piergiorgio. 1990. Lambda Calculi and Constructive Logics. Mathematical Sciences Institute, Cornell University. Schwichtenberg, Helmut. 1976. “Definierbare Funktionen im Lambda-Kalkul mit Typen”. Archiv Logik Grundlagenforsch. 17: 113-114. Sørensen, Morten Heine and Urzyczyin, Pavel. 2006. Lectures on the Curry-Howard Isomor- phism. Amsterdam: Elsevier. 10.1016/S0049-237X(06)80005-4 Statman, Richard. 1979. “The typed λ-calculus is not elementary recursive.”Theoretical Com- puter Science 9(1): 73-81. 10.1016/0304-3975(79)90007-0 Statman, Richard. 1979“ . Intuitionistic propositional logic is polynomial-space complete”. Theoretical Computer Science 9 : 67-72. 10.1016/0304-3975(79)90006-9 Takahashi, Masako. 1995. “Parallel Reductions in λ-Calculus ”. Information and Computation 118 (1): 120-127. 10.1006/inco.1995.1057 Troelstra, Anne S. and Schwichtenberg, Helmut. 2000. Basic proof theory. Cambridge: Cam- bridge University Press. 10.1017/cbo9781139168717 Wadsworth, Christopher P. 1971. Semantics and Pragmatics of the Lambda-Calculus. Disser- tation. Oxford University.