Lambda Calculus com JavaScript

Uma abordagem introdutória às raízes da programação funcional

(English)

O problema de decisão e a computabilidade

Existe um método efetivo que receba e valide qualquer proposição em uma linguagem formal?

Em termos gerais, essa é uma importante questão matemática posta em 1928 e que ficou conhecida como Entscheidungsproblem (termo alemão para “problema de decisão”). Anos mais tarde, em 1936, Alonzo Church e Alan Turing provaram que um algoritmo geral para o problema de decisão era impossível.

Para isso, eles elaboraram, de forma independente, dois modelos computacionais: Church criou o Lambda Calculus (λ-calculus) e Turing usou a sua teórica máquina (depois conhecida como Máquina de Turing).

A arquitetura de Von-Neumann implementou a teórica máquina de Turing e é utilizada nos computadores atuais. Já o modelo de Church, igualmente poderoso ao de Turing, por razões históricas, tomou um caminho mais acadêmico e menos comercial.

O objetivo deste artigo é apresentar os principais conceitos do Lambda Calculus com o auxílio da sintaxe JavaScript (ES2015), evidenciando sua influência nas linguagens modernas e a sua importância para o futuro da programação.

Lambda Calculus

O λ-calculus é um sistema formal para expressar e computar funções com regras de redução e sintaxe própria. O sistema é baseado em expressões (ou λ-terms; fórmulas).

Uma expressão pode corresponder a uma variável, uma abstração ou uma aplicação de função.

expression = variable || abstraction || application

As classes de expressões são definidas indutivamente como:

• A variável x é uma expressão por si só.

variable = expression

• Se x é uma variável e E é uma expressão, então λx.E é uma abstração.

abstraction = λ(variable).(expression)

• Se E é uma expressão e A é uma expressão, então EA é uma aplicação.

application = (expression)(expression)

Abstração de função

Em λ-calculus, as funções são definidas usando a λ (lambda) e não são nomeadas. Uma função anônima tem como única identidade a sua própria abstração. A expressão abaixo representa a definição de uma função (também chamada de abstração lambda):

λx.x

O nome depois de λ é o identificador do argumento e a expressão depois do ponto (.) representa o corpo da função. Em JavaScript, temos:

function (x) { 
    return x 
}

Agora com Arrow Function:

x => x

Para definir a abstração que recebe uma variável y como argumento e a retorna elevada ao quadrado, podemos escrever:

λy.y²

const Square = y => (y ** 2)

Aplicação de função

As funções podem ser aplicadas às expressões. Na expressão EA, o termo E é uma função aplicada à expressão A. Em outras palavras, a expressão A é um input na expressão E para produzir um output E(A).

Substituindo o termo E pela abstração λy.y², temos:

EA = E(A)

EA = (λy.y²)(A)

const E = y => (y ** 2)      // Abstração.
E(A)                         // Aplicação.

Essa aplicação é computada substituindo o valor do argumento y pelo input no corpo da função. Considere a expressão A como uma codificação do número inteiro 5:

EA = (λy.y²)(A) = y[y := A] = A² = 5² = 25

A notação y[y := A] indica que na expressão y (corpo), todas as ocorrências da variável y (argumento) devem ser substituídas pela expressão A.

const E = y => (y ** 2)
const A = 5
// A expressão "A" substitui a variável "y" na aplicação.
// Assim, a função pode ser simplificada como "A²".
E(A) == (A ** 2)              // true
A ** 2                        // 25
E(A)                          // 25

Sabendo disso é fácil entender que a aplicação EE simula uma recursão, onde a função E é passada como argumento para ela mesma.

EE = (λx.x)(λx.x) = x[x := (λx.x)] = λx.x

const E = x => x
E(E) // x => x

Em aplicações de λ-calculus, as funções podem receber outras funções como argumento e também retornar funções como resultado. Em linguagem de programação, as funções com essas características são conhecidas como First-class functions. Veja um exemplo trivial:

const SquareArea = side => (side ** 2)
const GetFormula = formula => formula
GetFormula(SquareArea) // side => (side ** 2)

A função anônima associada à variável GetFormula pode receber uma outra função como argumento e retorná-la como valor.

Funções com múltiplos argumentos

As abstrações em λ-calculus devem receber apenas um argumento. A técnica para obter múltiplos argumentos consiste na iteração de aplicações. Considere a função matemática:

f(x, y) = x + y

Estamos habituados a definir e aplicá-la da seguinte maneira:

const F = (x, y) => (x + y)
F(5, 10)

Diferente disso, podemos formular uma sequência de funções cuja primeira recebe o valor de x e retorna uma nova função que recebe o valor de y:

λx.(λy.x+y)

const F = x => (y => (x + y))

Aplicando a função com duas variáveis em dois passos:

(λx.(λy.x+y))(5) = x[x := 5] = λy.5+y

(λy.5+y)(10) = y[y := 10] = 5+10 = 15

const F = x => (y => (x + y))
F(5)(10)
// "x => (y => 5 + y)"
// "x => (y => 5 + 10)"
// 15

Essa estratégia foi introduzida por Haskell Curry e é chamada de Currying.

Para ficar mais claro, imagine uma abstração para calcular a área de um retângulo (A = base * altura):

λb.(λh.b*h)

const RectangleArea = base => (height => (base * height))
RectangleArea(2)(4)

Aplicamos a primeira função para receber o valor do argumento base e uma nova função, que cuidará do restante da operação, é retornada. Essa segunda função, quando aplicada, recebe o valor da altura (height) e retorna o resultado final do calculo de área do retângulo.

Codificação de tipos de dados

A função é o único tipo de dado primitivo no (untyped) Lambda Calculus. Para utilizar estruturas como Booleanos, numerais e operações aritméticas, por exemplo, é necessário definir abstrações que representem-as. Aqui, vamos abordar apenas as mais simples: Booleanos e seus operadores and e or.

Recomendo a leitura de The untyped Lambda Calculus para aprofundar-se no assunto.

Alonzo Church codifica os Booleanos como:

true = λa.(λb.a)

false = λa.(λb.b)

const True = a => b => a
const False = a => b => b

A lógica booleana é encarada como uma ação de escolha. Ambas as funções têm dois parâmetros e retornam um; a diferença é que True escolhe o primeiro para retornar e False escolhe o segundo.

Com base nisso, a estrutura If-then-else é representada como:

if = λp.(λa.(λb. p a b))

const If = Condition => Then => Else => Condition(Then)(Else)

Se Condition receber True , a função Then é retornada, pois True retorna o primeiro parâmetro recebido. Senão, se Condition receber False, a função Else é retornada, já que False retorna o seu segundo parâmetro.

Definindo rapidamente funções para auxiliar nos logs:

const isTrue = () => "it's true!"
const isFalse = () => "it's false!" 

Agora vamos aplicar a função If com os Booleanos:

const First = If(True)(isTrue)(isFalse)
const Second = If(False)(isTrue)(isFalse)
First() // "it's true!"
Second() // "it's false!"

Realizando as reduções fica fácil explicar o resultado; perceba que a, no código, é representado pela função Then e b é representado pela função Else:

if true = λp.(λa.(λb. p a b)) true = p[p := true] = true a b = λa.(λb.a) a b = a

if false = λp.(λa.(λb. p a b)) false = p[p := false] = false a b = λa.(λb.b) a b = b

Podemos ir além do If e definir os operadores and e or:

and = λp.(λq. p q p)

or = λp.(λq. p p q)

const And = Exp1 => Exp2 => Exp1(Exp2)(Exp1)
const Or = Exp1 => Exp2 => Exp1(Exp1)(Exp2)

Em lógica matemática, o operador and só retorna verdadeiro quando as duas expressões analisadas são verdadeiras. Por outro lado, o operador or só retorna falso quando ambas as expressões são falsas. Dessa maneira, a função And retornará False sempre que as expressões aplicadas forem diferentes de And(True)(True). A função Or retornará True toda vez que as expressões aplicadas não forem Or(False)(False).

Basta realizar as substituições nas aplicações dos operadores para verificar qualquer resultado. Por exemplo:

and true false = λp.(λq. p q p) true false = p[p := true] = q[q := false] = true false true = λa.(λb. a) false true = false

or true false = λp.(λq. p p q) true false = p[p := true] = q[q := false] = true true false = λa.(λb. a) true false = true

Segue uma tabela com todas as reduções:

| Operação          | Redução             | Resultado |
|-------------------|---------------------|-----------|
| And(True)(True)   | True(True)(True)    | True      |
| And(True)(False)  | True(False)(True)   | False     |
| And(False)(True)  | False(True)(False)  | False     |
| And(False)(False) | False(False)(False) | False     |
| Or(True)(True)    | True(True)(True)    | True      |
| Or(True)(False)   | True(True)(False)   | True      |
| Or(False)(True)   | False(False)(True)  | True      |
| Or(False)(False)  | False(False)(False) | False     |

Neste ponto, estamos prontos para testar todas as nossas estruturas de forma simples e intuitiva:

const Result1 = If(And(True)(True))(isTrue)(isFalse)
const Result2 = If(And(True)(False))(isTrue)(isFalse)
const Result3 = If(Or(False)(True))(isTrue)(isFalse)
const Result4 = If(Or(False)(False))(isTrue)(isFalse)
Result1() // "it's true"
Result2() // "it's false"
Result3() // "it's true"
Result4() // "it's false"

Por fim, vale ressaltar que a codificação em Lambda Calculus não visa uma implementação prática dos tipos de dados mas sim uma demonstração formal de que estes não são necessários para representar qualquer cálculo, já que, usando apenas funções, é possível simulá-los.

Lambda Calculus e a programação funcional

“Computability via Turing machines gave rise to imperative programming. Computability described via λ-calculus gave rise to functional programming.” — Cooper & Leeuwen (2013)

Alonzo Church criou o λ-calculus antes dos computadores eletrônicos, no entanto, sua notação tem grande impacto em linguagens de programação atuais. Lisp é conhecida como a segunda linguagem de programação de alto nível da história e foi inspirada (assim como toda sua família) pelo λ-calculus. Qualquer linguagem com suporte a anonymous function (Haskell, JavaScript, Python, Ruby, entre outras), por exemplo, tem um pouco do formalismo de Church.

O uso de padrões funcionais encorajam códigos expressivos pois estes correspondem mais diretamente a objetos matemáticos e, portanto, são mais razoáveis. Assim, como na matemática, um código funcional tem transparência referencial (produz o mesmo resultado dados os mesmos parâmetros) e isso facilita a sua paralelização em múltiplos processadores.

A influência do Lambda Calculus sobre as diversas linguagens de programação modernas não se deve apenas ao fato do formalismo ser Turing-completo, mas principalmente por sua simplicidade e expressividade, sendo esses aspectos decisivos para o futuro da programação.

Referências

1. Henk Barendregt, Erik Barendsen (2000). Introduction to Lambda Calculus.
2. Raúl Rojas (1998). A Tutorial Introduction to the Lambda Calculus.
3. Manuel Eberl (2011). The untyped Lambda Calculus.
4. Barry Cooper, J. van Leeuwen (2013). Alan Turing: His Work and Impact.