# Lambda calculus#

Bruijn is based on de Bruijn indexed lambda calculus.

## Traditional lambda calculus#

Lambda calculus basically has three types of terms:

*Variable*:`x`

binds the named variable`x`

to an abstraction.*Abstraction*:`λx.E`

accepts an argument`x`

and binds it to term`E`

respectively. It's helpful to think of abstractions as anonymous functions.*Application*:`(f x)`

applies`f`

to`x`

-- the standard convention allows repeated left-associative application:`f x y z`

is`(((f x) y) z)`

.

Combining these terms and removing redundant parentheses can result in
terms like `λx.λy.x y`

, basically representing a function with two
parameters that uses its second parameter as an argument for its first.

Evaluating terms is called *reduction*. There's only one rule you need
to know: `(λx.E A)`

becomes `E[x := A]`

-- that is, calling an
abstraction with an argument substitutes the argument inside the body of
the abstraction ("β-reduction"). There are many different kinds of
reduction techniques, but they basically all come back to this simple
rule -- mainly because of the "Church-Rosser theorem" that states that
the order of reduction doesn't change the eventual result.

When we talk about reduction in bruijn, we typically mean "reduction
until normal form" -- we reduce until the term can't be reduced any
further (there does not exist any `(λx.E A)`

).

```
(λx.x λx.x) ⤳ λx.x
(λx.x λx.λy.x) ⤳ λx.λy.x
(λx.λy.x (λx.x) ⤳ λy.λx.x
```

## De Bruijn indices#

Programs written in lambda calculus often have many abstractions and therefore at least as many variables. I hate naming variables, especially if you need hundreds of them for small programs. With that many variables it's also really complicated to compare two expressions, since you first need to resolve shadowed and conflicting variables ("α-conversion").

De Bruijn indices replace the concept of variables by using numeric
references to the abstraction layer. Let me explain using an example:
The expression `λx.x`

becomes `λ0`

-- the `0`

refers to the first
parameter of the abstraction. Subsequently, the expression `λx.λy.x y`

becomes `λλ1 0`

. Basically, if you're reading from left to right
starting at the abstraction you want to bind, you increment on every
occurring `λ`

until you arrive at the index.

While confusing at first, programs written with de Bruijn indices can actually be way easier to understand than the equivalent program with named variables.

## Bruijn's bracketing#

Bruijn's final syntactic variation from lambda calculus is the use of square brackets instead of lambda symbols. By putting the entire abstracted term in brackets, it's much clearer where indices and the respective terms are bound to.

Representing `λλ1 0`

in bruijn's syntax then becomes `[[1 0]]`

.
The application of `λ0`

and `λλ1 0`

becomes `[0] [[1 0]]`

.

Random example reductions:

```
a [0] [[1]] ⤳ [[1]]
b [[0]] [[1]] ⤳ [0]
c [[1]] [[1]] ⤳ [[[1]]]
d [[0]] [0] [[1]] ⤳ [[1]]
e [[0 1]] [0] ⤳ [0 [0]]
f [[1 0]] [0] ⤳ [0]
```