Lambda Calculus
Lambda Calculus only has
- function definitions and
- function calls
It notably doesn't have if statements, types, variables, loops and recursion.
Even though, it can compute anything that a classic language like C can.
Syntax:
x | Variable (which is any letter of the alphabet) |
λx.e | Abstraction (i. e. a nameless function where x is the argument and e is the function's body). The λ and the . always come together in pairs. |
e₁ e₂ | Application. e₁ evaluates to a function to which e₂ is applied. |
Definition of expressions
- A variable (for example
x) is a valid λ-term
- If
t is a valid λ-term and x is a variable, then λx.t is a valid λ-term
- If
t and s are both valid λ-terms, then t s is a valid λ-term
e1 e2 e3 is the same as (e1 e2) e3.
λx.x is an abstraction that represents the identity function.
λy.λx.x is a an abstraction that ignores its argument (y) and returns the identity function (λx.x)
(λx.x) y applies the y to the function λx.x.
Currying
An abstraction (function) can only have one argument (i. e. one letter between the λ and the .).
In order to create a function that takes two arguments, two functions must be defined:
- A function that takes the first argument which creates
- the function that takes the second argument.
λx. λy. ‥ x ‥ y ‥
In pseudo code, this is sometimes abbreviated with λxy. ‥
Loop
A loop can be expressed in lambda calculus like so (a function that is applied to itself):
(λx.x x) (λx.x x)
Because when the function on the right side is applied to the function on the left side, the result is again
(λx.x x) (λx.x x)
Allegedly, this form allows to define a loop in a language that doesn't have loops.
Y-Combinator
Is this the Y-Combinator?
λf.(λx.f(x x)) (λx.f(x x))
Allegedly, the Y-Combinator allows to define a recursion in a language that doesn't have recursions.