───✱*.。:。✱*.:。✧*.。✰*.:。✧*.。:。*.。✱ ───
Introduction
Lambda calculus is a system for expressing computations based on function abstraction & application. It’s the basis of functional programming and provides a simple way to represent computations.
It was introduced by Alonzo Church in the 1930s as part of his research into the foundations of mathematics.
λ Terms
Lambda calculus is comprised of constructing lambda terms and doing reduction operations on those terms.
Abstraction is the process of creating a function. The syntax of these functions are: λx. M, where x is the parameter of the function, and M is the lambda expression (also known as the body of the function). For instance, a function that doubles some x would look like: λx. x * 2
Application is the process of applying an argument to a function. The syntax of this is (M N), where M and N are lambda expressions. For instance, (λx. x * 2) 2 applies the double function from before to the argument 2, resulting in 2 * 2 = 4.
Expressions
Lambda calculus consists of a few expression rules, such as alpha conversion, beta reduction, and eta conversion:
- Alpha conversion renames variables
λx. xis equivalent toλy. y
- Beta reduction applies arguments to functions
(λx. x + 1) 2reduces to2 + 1 = 3
- Eta conversions simplify functions
λx. (f x)is equivalent tofiffdoesn’t usexin the lambda expression.
───✱*.。:。✱*.:。✧*.。✰*.:。✧*.。:。*.。✱ ───