Hostname: page-component-8448b6f56d-qsmjn Total loading time: 0 Render date: 2024-04-23T12:38:28.984Z Has data issue: false hasContentIssue false
  • English
  • Français

The Impact of the Lambda Calculus in Logic and Computer Science

Published online by Cambridge University Press:  15 January 2014

Henk Barendregt
Henk Barendregt*
Affiliation:
Computing Science Institute, Nijmegen University, The Netherlands.E-mail: henk@cs.kun.nl
Get access Rights & Permissions [Opens in a new window]

Abstract

One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the representation of computations and the resulting functional programming languages on the one hand and the representation of reasoning and the resulting systems of computer mathematics on the other hand.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 3 , Issue 2 , June 1997 , pp. 181 - 215
Copyright
Copyright © Association for Symbolic Logic 1997

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E. (editors), Handbook of logic in computer science, Volume 2: Background: Computational structures, Oxford University Press, 1992.Google Scholar
[2] Ackermann, W., Zum Hilbertschen Aufbau der reellen Zahlen, Mathematische Annalen, vol. 99 (1928), pp. 118–133.CrossRefGoogle Scholar
[3] Appel, A. W., Compiling with continuations, Cambridge University Press, 1992.Google Scholar
[4] Aspinall, D. and Compagnoni, A., Subtyping dependent types, Proceedings of the 11th annual symposium on logic in computer science (New Brunswick, New Jersey) (Clarke, E., editor), IEEE Computer Society Press, 07 1996, pp. 86–97.CrossRefGoogle Scholar
[5] Backus, J. W., Can programming be liberatedfrom the von Neuman style?, Comm. ACM, vol. 21 (1978), pp. 613–641.CrossRefGoogle Scholar
[6] Barendregt, H. P., The lambda calculus: its syntax and semantics, revised ed., North-Holland, Amsterdam, 1984.Google Scholar
[7] Barendregt, H. P., Theoretical pearls: Self-interpretation in lambda calculus, Journal of Functional Programming, vol. 1 (1991), no. 2, pp. 229–233.CrossRefGoogle Scholar
[8] Barendregt, H. P., Lambda calculi with types, 1992, in [1], pp. 117–309.Google Scholar
[9] Barendregt, H. P., Discriminating coded lambda terms, From universal morphisms to megabytes: A Baayen space-odyssey (Apt, K. R., Schrijver, A. A., and Temme, N. M., editors), CWI, Kruislaan 413, 1098 SJ Amsterdam, 1994, pp. 141–151.Google Scholar
[10] Barendregt, H. P., Enumerators of lambda terms are reducing constructively, Annals of Pure and Applied Logic, vol. 73 (1995), pp. 3–9.CrossRefGoogle Scholar
[11] Barendregt, H. P., The quest for correctness, Images of SMC research, Stichting Mathematisch Centrum, P.O. Box 94079, 1090 GB Amsterdam, 1996, pp. 39–58.Google Scholar
[12] Barendregt, H. P. and Barendsen, E., Efficient computations in formal proofs, to appear, 1997.Google Scholar
[13] Barendregt, H. P., Bunder, M., and Dekkers, W., Systems of illative combinatory logic complete for first order propositional and predicate calculus, Journal of Symbolic Logic, vol. 58 (1993), no. 3, pp. 89–108.CrossRefGoogle Scholar
[14] Barendsen, E. and Smetsers, J. E. W., Conventional and uniqueness typing in graph rewrite systems (extended abstract), 1993, in [105], pp. 41–51.CrossRefGoogle Scholar
[15] Barendsen, E. and Smetsers, J. E. W., Uniqueness typing for functional languages with graph rewriting semantics, to appear in Mathematical Structures in Computer Science, 1997.Google Scholar
[16] Beeson, M. J., Foundations of constructive mathematics, Springer-Verlag, Berlin, 1980.Google Scholar
[17] van Benthem, J. F. A. K., Language in action: Categories, lambdas and dynamic logic, Studies in Logic and the Foundations of Mathematics, vol. 130, North-Holland, Amsterdam, 1991.Google Scholar
[18] Jutting, L. S. van Benthem, Checking Landau's “Grundlagen” in the AUTOMATH system, Ph.D. thesis , Eindhoven University of Technology, 1977.Google Scholar
[19] Berarducci, A. and Böhm, C., A self-interpreter of lambda calculus having a normal form, Lecture Notes in Computer Science, vol. 702 (1993), pp. 85–99.CrossRefGoogle Scholar
[20] Bezem, M. and Groote, J. F. (editors), Typed lambda calculi and applications, TLCA'93, Lecture Notes in Computer Science, vol. 664, Berlin and New York, Springer-Verlag, 1993.CrossRefGoogle Scholar
[21] Böhm, C., The CUCH as a formal and description language, Annual review in automatic programming (Goodman, Richard, editor), vol. 3, Pergamon Press, Oxford, 1963, pp. 179–197.Google Scholar
[22] Böhm, C. and Berarducci, A., Automatic synthesis of typed λ-programs on term algebras, Theoretical Computer Science, vol. 39 (1985), pp. 135–154.CrossRefGoogle Scholar
[23] Böhm, C. and Gross, W., Introduction to the CUCH, Automata theory (Caianiello, E. R., editor), Academic Press, New York, 1966, pp. 35–65.Google Scholar
[24] Böhm, C., Piperno, A., and Guerrini, S., Lambda-definition of function(al)s by normal forms, Esop'94 (Berlin) (Sanella, D., editor), vol. 788, Springer-Verlag, 1994, pp. 135–154.Google Scholar
[25] Braithwaite, R. B. (editor), F. P. Ramsay: The foundations of mathematics and other logical essays, Routledge & Kegan Paul, London, 1960.Google Scholar
[26] de Bruijn, N. G., The mathematical language AUTOMATH, its usage and some of its extensions, Symposium on automatic demonstration (Berlin and New York) (Laudet, M., Lacombe, D., and Schuetzenberger, M., editors), Lecture Notes in Mathematics, vol. 125, Springer-Verlag, 1970, pp. 29–61, also in [88], pp. 73–100.CrossRefGoogle Scholar
[27] de Bruijn, N. G., Reflections on Automath, Eindhoven University of Technology, 1990, also in [88], pp. 201–228.CrossRefGoogle Scholar
[28] Church, A., An unsolvable problem of elementary number theory, American Journal of Mathematics, vol. 58 (1936), pp. 354–363.CrossRefGoogle Scholar
[29] Church, A., A formulation of the simple theory of types, Journal of Symbolic Logic, vol. 5 (1940), pp. 56–68.CrossRefGoogle Scholar
[30] Church, A., The calculi of lambda conversion, Princeton University Press, 1941.Google Scholar
[31] Church, A. and Rosser, J. B., Some properties of conversion, Transactions of the American Mathematical Society, vol. 39 (1936), pp. 472–482.CrossRefGoogle Scholar
[32] Clinger, W. and Rees, J. (editors), Revised report on the algorithmic language Scheme, vol. IV, LISP Pointers, no. 3, 1991.Google Scholar
[33] Coquand, T. and Huet, G., The calculus of constructions, Information and Computation, vol. 76 (1988), no. 2/3, pp. 95–120.CrossRefGoogle Scholar
[34] Cousineau, G., Curien, P.-L., and Mauny, M., The categorical abstract machine, Science of Computer Programming, vol. 8 (1987), no. 2, pp. 173–202.CrossRefGoogle Scholar
[35] Curien, P.-L., Categorical combinators, sequential algorithms, and functional programming, Research Notes in Theoretical Computer Science, Pitman, London, 1986.Google Scholar
[36] Curry, H. B., Grundlagen der kombinatorischen Logik, American Journal of Mathematics, vol. 52 (1930), pp. 509–536, 789–834, in German.Google Scholar
[37] Curry, H. B., Functionality in combinatory logic, Proceedings of the National Academy of Science of the USA, vol. 20 (1934), pp. 584–590.CrossRefGoogle ScholarPubMed
[38] Curry, H. B., Modified basic functionality in combinatory logic, Dialectica, vol. 23 (1969), pp. 83–92.CrossRefGoogle Scholar
[39] Dekkers, W., Bunder, M., and Barendregt, H. P., Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic, Journal of Symbolic Logic (1997), to appear.Google Scholar
[40] van Eekelen, M. C. J. D. and Plasmeijer, M. J., Functional programming and parallel graph rewriting, Addison-Wesley, Reading, Massachusetts, 1993.Google Scholar
[41] Elbers, H., Personal communication, 1996.Google Scholar
[42] Euclid, , The elements, 325 B.C. English translation in [55], 1956.Google Scholar
[43] Feferman, S., A language and axioms for explicit mathematics, Proof theory symposium (Berlin) (Diller, J. H. and Müller, G. H., editors), Lecture Notes in Mathematics, vol. 500, Springer-Verlag, 1975, pp. 87–139.Google Scholar
[44] Feferman, S., Definedness, Erkentniss, vol. 43 (1995), pp. 295–320.CrossRefGoogle Scholar
[45] Gamut, L. T. F., Logic, language and meaning, Chicago University Press, Chicago, 1992.Google Scholar
[46] Gandy, R. O., Church's Thesis and principles for mechanisms, The Kleene symposium, North-Holland Publishing Company, Amsterdam, 1980, pp. 123–148.CrossRefGoogle Scholar
[47] Gentzen, G., Investigations into logical deduction, in [111], 1969.Google Scholar
[48] Gentzen, G., Untersuchungen über das logische Schliessen, Mathematische Zeitschrift, vol. 39 (1935), pp. 176–210, 405–431, also available in [111], pp 68–131.CrossRefGoogle Scholar
[49] Girard, J.-Y., Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur, Ph.D. thesis , Universite Paris VII, 1972.Google Scholar
[50] Girard, J.-Y., Linear logic: its syntax and semantics, Advances in linear logic ( Girard, J.-Y., Lafont, Y., and Regnier, L., editors), London Mathematical Society Lecture Note Series, Cambridge University Press, 1995, available by anonymous ftp from lmd.univ-mrs.fr as /pub/girard/Synsem.ps.Z.Google Scholar
[51] Girard, J-Y., Lafont, Y. G. A., and Taylor, P., Proofs and types, Cambridge Tracts in Theoretical Computer Science, vol. 7, Cambridge University Press, 1989.Google Scholar
[52] Gordon, A. D., Functional programming and Input/Output, Distinguished Dissertations in Computer Science, Cambridge University Press, 1994.Google Scholar
[53] Grue, K., Map theory, Theoretical Computer Science (1992), pp. 1–133.Google Scholar
[54] Gunter, C. A. and Scott, D. S., Semantic domains, Handbook of theoretical computer science, vol. B, in [78], 1990, pp. 633–674.Google Scholar
[55] Heath, T. L., The thirteen books of Euclid's elements, Dover Publications, Inc., New York, 1956.Google Scholar
[56] van Heijenoort, J. (editor), From Frege to Gödel: A source book in mathematical logic, 1879–1931, Harvard University Press, Cambridge, Massachusetts, 1967.Google Scholar
[57] Henderson, P., Functional programming: Application and implementation, Prentice-Hall, Englewood Cliffs, New Jersey, 1980.Google Scholar
[58] Hilbert, D. and Ackermann, W., Grundzüge der theoretischen logik, first ed., Die Grundlehren der Mathematischen Wissenschaften in Einzeldars tellungen, Band XXVII, Springer-Verlag, Berlin and New York, 1928.Google Scholar
[59] Hindley, R., The principal type-scheme of an object in combinatory logic, Transactions of the American Mathematical Society, vol. 146 (1969), pp. 29–60.Google Scholar
[60] Hodges, A., The enigma of intelligence, Unwin paperbacks, London, 1983.Google Scholar
[61] Hofmann, M., A simple model for quotient types, Typed lambda calculi and applications (Berlin and New York), Lecture Notes in Computer Science, Springer-Verlag, 1977, pp. 216–234.Google Scholar
[62] Hudak, P. et al., Report on the programming language Haskell: A non-strict, purely functional language (Version 1.2), ACM SIGPLAN Notices, vol. 27 (1992), no. 5, pp. Ri–Rx, R1–R163.Google Scholar
[63] Hughes, R. J. M., The design and implementation of programming languages, Ph.D. thesis , University of Oxford, 1984.Google Scholar
[64] Hughes, R. J. M., Why functional programming matters, The Computer Journal, vol. 32 (1989), no. 2, pp. 98–107.CrossRefGoogle Scholar
[65] Iverson, K. E., A programming language, Wiley, New York, 1962.CrossRefGoogle Scholar
[66] Johnsson, T., Efficient compilation of lazy evaluation, SIGPLAN Notices, vol. 19 (1984), no. 6, pp. 58–69.CrossRefGoogle Scholar
[67] Kleene, S. C., Lambda-definability and recursiveness, Duke Mathematical Journal, vol. 2 (1936), pp. 340–353.CrossRefGoogle Scholar
[68] Kleene, S. C., Introduction to metamathematics, The University Series in Higher Mathematics, D. Van Nostrand Comp., New York, Toronto, 1952.Google Scholar
[69] Kleene, S. C., Reminiscences of logicians, Algebra and logic (Fourteenth summer res. inst., Austral. Math. Soc., Monash Univ., Clayton, 1974) (Crossley, J. N., editor), Lecture Notes in Mathematics, vol. 450, Springer-Verlag, Berlin and New York, 1975, pp. 1–62.Google Scholar
[70] Kleene, S. C., Origins of recursive function theory, Annals of the History of Computing, vol. 3 (1981), no. 1, pp. 52–67.CrossRefGoogle Scholar
[71] Kleene, S. C. and Rosser, J. B., The inconsistency of certain formal logics, Annals of Mathematics, vol. 36 (1935), pp. 630–636.CrossRefGoogle Scholar
[72] Koymans, C. P. J., Models of the lambda calculus, Information and Control, vol. 52 (1982), no. 3, pp. 306–323.Google Scholar
[73] Kreisel, G., Church's thesis: A kind of reducibility axiom for constructive mathematics, in [86], pp. 121–150.Google Scholar
[74] Kreisel, G., The formalist-positivist doctrine of mathematical precision in the light of experience, L'age de la Science, vol. 3 (1970), pp. 17–46.Google Scholar
[75] Kuper, J., An axiomatic theory for partial functions, Information and Computation (1993), pp. 104–150.Google Scholar
[76] Landau, E., Grundlagen der analysis, third ed., Chelsea Publishing Company, 1960.Google Scholar
[77] Landin, P. J., The mechanical evaluation of expressions, The Computer Journal, vol. 6 (1964), no. 4, pp. 308–320.CrossRefGoogle Scholar
[78] van Leeuwen, J. (editor), Handbook of theoretical computer science, vol. A, B, North-Holland, MIT-Press, 1990.Google Scholar
[79] Leivant, D., Reasoning about functional programs and complexity classes associated with type disciplines, 24th annual symposium on foundations of computer science, IEEE, 1983, pp. 460–469.Google Scholar
[80] Luo, Z. and Pollack, R., The LEGO proof development system: A user's manual, Technical Report ECS-LFCS-92-211, University of Edinburgh, 05 1992.Google Scholar
[81] Martin-Löf, P., Intuitionistic type theory, Studies in Proof Theory, Bibliopolis, Napoli, 1984.Google Scholar
[82] Matijasevič, Yu.V., On recursive unsolvability of hilbert's tenth problem, Fourth international congress for logic, methodology and philosophy of science, Studies in Logic and the Foundations of Mathematics, vol. 74, North-Holland, Amsterdam, 1971, pp. 89–110.Google Scholar
[83] McCarthy, J. et al., Lisp 1.5 programmer's manual, MIT Press, Cambridge, Massachusetts, 1962.Google Scholar
[84] Milner, R., A theory of type polymorphism in programming, Journal of Computer and System Sciences, vol. 17 (1978), pp. 348–375.CrossRefGoogle Scholar
[85] Mogensen, T.Æ., Theoretical pearls: Efficient self-interpretation in lambda calculus, Journal of Functional Programming, vol. 2 (1992), no. 3, pp. 345–364.Google Scholar
[86] Myhill, J., Vesley, R. E., and Kino, A. (editors), Intuitionism and proof theory, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1970.Google Scholar
[87] Nadathur, G. and Miller, D., An overview of λProlog, Logic programming: Proceedings of the fifth international conference and symposium, Volume 1 (Cambridge, Massachusetts) (Kowalski, Robert A. and Bowen, Kenneth A., editors), MIT Press, 08 1988, pp. 810–827.Google Scholar
[88] Nederpelt, R. P., Geuvers, J. H., and de Vrijer, R. C. (editors), Selected papers on automath, Studies in Logic and the Foundations of Mathematics, vol. 133, North-Holland, Amsterdam, 1994.Google Scholar
[89] von Neumann, J., Eine axiomatisierung der mengenlehre, Journal für die Reine und Angewandte Mathematik, vol. 154 (1925), pp. 219–240.CrossRefGoogle Scholar
[90] Oostdijk, M., Proof by calculation, Master's thesis, 385 , Universitaire School voor Informatica, Catholic University Nijmegen, 1996.Google Scholar
[91] Paulin-Mohring, C., Inductive definitions in the system Coq; rules and properties, 1993, in [20], pp. 328–345.CrossRefGoogle Scholar
[92] Jones, S. L. Peyton and Wadler, P., Imperative functional programming, Conference record ofthe twentieth annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, Charleston, South Carolina, January 10-13, 1992, ACM Press, 1993, pp. 71–84 (English).Google Scholar
[93] Plotkin, G. D., Call-by-name, call-by-value and the λ-calculus, Theoretical Computer Science, vol. 1 (1975), pp. 125–159.CrossRefGoogle Scholar
[94] Poincaré, H., La science et l'hypothèse, Flammarion, Paris, 1902.Google Scholar
[95] Ramsey, F. P., The foundations of mathematics, Proceedings of the London Mathematical Society, Series 2, vol. 25 (1925), pp. 338–384, translated in [25].Google Scholar
[96] Reynolds, J. C., Definitional interpreters for higher-order programming languages, Proceedings of 25th ACM national conference (Boston, Massachusetts), 1972, pp. 717–740.Google Scholar
[97] Reynolds, J. C., The discoveries of continuations, LISP and Symbolic Computation, vol. 6 (1993), no. 3/4, pp. 233–247.CrossRefGoogle Scholar
[98] Robinson, R. M., The theory of classes—a modification of von Neumann's system, Journal of Symbolic Logic, vol. 2 (1937), pp. 29–36.CrossRefGoogle Scholar
[99] Rosser, J. B., Highlights of the history of lambda-calculus, ACM symposium on Lisp and functional programming (Pennysylvania), ACM Press, 08 1982, pp. 216–225.Google Scholar
[100] Russell, B. A. W. and Whitehead, A. N., Principia mathematica, vol. 1 and 2, Cambridge University Press, 1910–1913.Google Scholar
[101] Schwichtenberg, H., Definierbare Funktionen im λ-Kalkül mit Typen, Archief für Mathematische Logik, vol. 25 (1976), pp. 113–114.Google Scholar
[102] Scott, D. S., Constructive validity, Symposium on automated demonstration (Lacombe, D., Laudet, M. and Schuetzenberger, M., editors), Lecture Notes in Mathematics, vol. 125, Springer-Verlag, Berlin, 1970, pp. 237–275.CrossRefGoogle Scholar
[103] Scott, D. S., Continuous lattices, Toposes, algebraic geometry, and logic (Lawvere, F. W., editor), Lecture Notes in Mathematics, vol. 274, Springer-Verlag, Berlin and New York, 1972, pp. 97–136.CrossRefGoogle Scholar
[104] Severi, P. and Poll, E., Pure type systems with definitions, Proceedings of LFCS'94 (Berlin and New York) (Nerode, A. and Matijasevič, Yu.V., editors), Lecture Notes in Computer Science, vol. 813, LFCS'94, St. Petersburg, Springer-Verlag, 1994, pp. 316–328.Google Scholar
[105] Shyamasundar, R. K. (editor), Proceedings of the 13th conference on foundations of software technology and theoretical computer science, Lecture Notes in Computer Science, vol. 761, Berlin and New York, Bombay, India, Springer-Verlag, 1993.CrossRefGoogle Scholar
[106] Skolem, T., Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Verënderlichen mit unendlichem Ausdehnungsbereich, Videnskapsselskapets skrifter, I. Matematisk-naturvidenskabelig klasse, vol. 6 (1923), English translation in [56], pp. 302–333.Google Scholar
[107] Smyth, M. B. and Plotkin, G. D., The category-theoretic solution of recursive domain equations, SIAM Journal on Computing, vol. 11 (1982), no. 4, pp. 761–783.CrossRefGoogle Scholar
[108] Statman, R., The typed lambda calculus is not elementary recursive, Theoretical Computer Science, vol. 9 (1979), pp. 73–81.CrossRefGoogle Scholar
[109] Steele, Guy L. Jr., Rabbit: A compiler for Scheme, Technical Report AI-TR-474, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, 05 1978.Google Scholar
[110] Steele, Guy L. Jr., Common Lisp: The language, Digital Press, 1984.Google Scholar
[111] Szabo, M. E. (editor), The collected papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969.Google Scholar
[112] Troelstra, A. S. (editor), Metamathematical investigation of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin and New York, 1973.CrossRefGoogle Scholar
[113] Turing, A. M., On computable numbers with an application to the Entscheidungsproblem, Proceeding of the London Mathematical Society. Second Series., vol. 42 (1936), pp. 230–265.Google Scholar
[114] Turing, A. M., Computability and lambda definability, Journal of Symbolic Logic, vol. 2 (1937), pp. 153–163.CrossRefGoogle Scholar
[115] Turner, D. A., The SASL language manual, 1976.Google Scholar
[116] Turner, D. A., A new implementation technique for applicative languages, Software—Practice andExperience, vol. 9 (1979), pp. 31–49.CrossRefGoogle Scholar
[117] Turner, D. A., The semantic elegance of functional languages, Proceedings of the ACM/MIT conference on functional languages and computer architecture, ACM Press, Pennsylvania, 1981, pp. 85–92.Google Scholar
[118] Turner, D. A., Miranda—a non-strict functional language with polymorphic types, Functional programming languages and computer architectures (Berlin and New York) (Jouannaud, J. P., editor), Lecture Notes in Computer Science, vol. 201, Springer-Verlag, 1985, pp. 1–16.CrossRefGoogle Scholar
[119] Wadswortt, C., Semantics and pragmatics of the lambda-calculus, D. Phil thesis , University of Oxford, Programming Research Group, Oxford, U.K., 1971.Google Scholar