Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of Graph Search.
Concept
Deductive lambda calculus
Summary
Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression. The expression would equal the reduction of the expression.
Alonzo Church invented the lambda calculus in the 1930s, originally to provide a new and simpler basis for mathematics. However soon after inventing it major logic problems were identified with the definition of the lambda abstraction: The Kleene–Rosser paradox is an implementation of Richard's paradox in the lambda calculus. Haskell Curry found that the key step in this paradox could be used to implement the simpler Curry's paradox. The existence of these paradoxes meant that the lambda calculus could not be both consistent and complete as a deductive system.
Haskell Curry studied of illative (deductive) combinatory logic in 1941. Combinatory logic is closely related to lambda calculus, and the same paradoxes exist in each.
Later the lambda calculus was resurrected as a definition of a programming language.
Lambda calculus is the model and inspiration for the development of functional programming languages. These languages implement the lambda abstraction, and use it in conjunction with application of functions, and types.
The use of lambda abstractions, which are then embedded into other mathematical systems, and used as a deductive system, leads to a number of problems, such as Curry's paradox. The problems are related to the definition of the lambda abstraction and the definition and use of functions as the basic type in lambda calculus. This article describes these problems and how they arise.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.