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 abstration 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 formallows 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.