Skip to content
This repository has been archived by the owner on Jan 19, 2023. It is now read-only.

Latest commit

 

History

History
185 lines (148 loc) · 6.4 KB

lambda_calculus.org

File metadata and controls

185 lines (148 loc) · 6.4 KB
Raw

Lambda Calculus

Segundo a Wikipedia, o cálculo lambda (ou cálculo λ) é:

A formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing Machine.

— Lambda Calculus - Wikipedia, the free enclycopedia

Definição

É responsável por receber um input, processá-lo atráves de algo semelhante a uma “black-box” e obter seu output. Diferentemente do modelo computacional proposto por Turing, o cálculo lambda não possui nenhum estado interno, sendo assim, ela é baseada em funções matemáticas puras.

Um exemplo de uma “função lambda” seria: \begin{equation} (λ x.x + 1)(5) \end{equation}

Você pode substituir o valor de x por 5, e assim obterá o respectivo “output” gara a função.

A syntax é basicamente isto:

Expressions
<expression> := <name> / <function> / <application>
<function> := $$λ$$ <name> . <expression>
<application> := <expression><expression>

Observação: A syntax é escrita na notação de Backus-Naur form.

Reductions and others

Some ways to reduce a lambda function or write an equivalence between two of it.

Alpha equivalence

Because of non-semantic meaning of the bounded/free variables, exists a way of equivalence between lambda terms. It’s called alpha equivalence. This implies that:

\begin{aligned} λ x.x
λ d.d\ λ z.z\ \end{aligned}

All of it mean the same thing. They’re all the same function.

Beta reduction

The substitution of the input expression for all instances of bound variables[fn:1] within the body of the abstraction. You also eliminate the head of the abstraction, since its only purpose was to bind a variable. It’s called beta reduction.

Based on this function:

\begin{equation} λ x.x \end{equation}

We apply the function above to 2, substitute 2 for each bound variable in the body of the function, and eliminate the head

\begin{document} \begin{equation} (λ x.x) 2 \end{equation} \begin{equation} 2 \end{equation} \end{document}

In this case, the only bound variable is $x$, so applying this function to 2 returns 2. This function is called identity function. All it does is accept a single argument $x$ and return the same argument. All instances of $x$ within the function body must have the same value.

You can write a beta reduction like this as well:

\begin{equation} (λ x.x)2 → x[x \coloneqq 2] \end{equation}

Beta reduction is this process of applying a lambda term to an argument, replacing the bound variables with the value of the argument, and eliminating the head.

Applications in the lambda calculus are left associative. That is, unless specific parenthesis suggest otherwise, they associate, or group, to the left. So this:

\begin{equation} (λ x.x)(λ y.y)z \end{equation}

Can be rewritten as:

\begin{equation} ((λ x.x)(λ y.y))z \end{equation}

Onward with the reduction:

\begin{document} \begin{equation} ((λ x.x)(λ y.y))z \end{equation} \begin{equation} [x \coloneqq (λ y.y)] \end{equation} \begin{equation} (λ y.y)z \end{equation} \begin{equation} [y \coloneqq z] \end{equation} \begin{equation} z \end{equation} \end{document}

A computation therefore consists of an initial lambda expression (or two, if you want to separate the function and its input) plus a finite sequence of lambda terms, each deduced from the preceding term by one application of beta reduction.

Free variables

Sometimes the body expression has variables that are not named in the head. We call those variables free variables. For example, in the following expression:

\begin{equation} λ x.xy \end{equation}

The $x$ in the body is a bound variable because it is named in the head of the function, while the $y$ is a free variable because it is not. When we apply this function to an argument, nothing can be done with the $y$. It remains irreducible.

The alpha equivalence does not apply to free variables. That is, $λ x.xz$ and $λ x.xy$ are not equivalent because $z$ and $y$ might be different things. However, $λ xy.yx$ and $λ ab.ba$ are equivalent due to alpha equivalence because the free variable is left alone.

Combinators

A combinator is a lambda term with no free variables. Combinators, as the name suggest, serve only to combine the arguments they are given.

  • I ou “Identity”: é uma função que recebe um argumento e o retorna. Exemplo: λ x.x
  • K ou “Kestrel”: é uma função que recebe dois argumentos e retorna o primeiro. Exemplo: λ xy.x
  • KI ou “Kite”: é uma função que recebe dois argumentos e retorna o segundo. Exemplo: λ xy.y
  • C ou “Cardinal”: é uma função que recebe uma função com dois argumentos e os “flipa”. Exemplo: λ fxy.fyx
  • M ou “Mockingbird”: é uma função que recebe uma função e aplica nela mesmo. Exemplo: λ x.xx

References

Footnotes

[fn:1] Variáveis bounded são aquelas que tem seu escopo definido pela função, em oposição, variáveis “free” são aquelas que não possuem o escopo definido.