Lambda Cálculo

Teoria da Computação
Prof. Luiz Maurílio da Silva Maciel
[Link]@[Link]

Universidade Federal de Juiz de Fora

Instituto de Ciências Exatas
Departamento de Ciência da Computação

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 1 / 20

Introdução

Proposto por Alonzo Church em 1936

Base para as linguagens de programação funcionais:
Interessante pela simplicidade sintática
Facilidade de descrição de problemas recursivos
Muitas implementações são pouco aceitas devido a ineficiência
Exemplos de linguagens funcionais: LISP, Miranda, Haskell, Orwel

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 2 / 20

Introdução

Utilidade do Lambda Cálculo em programação funcional:

Serve de ponto de partida, uma vez que as linguagens diferem somente na
sintaxe
Linguagem funcional de alto nível pode ser compilada em um código
intermediário com uma sintaxe e semântica simples, expressa em termos
de Lambda Cálculo
Lambda Cálculo é expressivo o suficiente para permitir a codificação de
uma linguagem de programação de alto nível
Algoritmos para solução de problemas usando Lambda Cálculo podem ser
facilmente implementadas de outras formas

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 3 / 20

Lambda Cálculo

Apresenta dois conceitos fundamentais: abstração e aplicação de

funções

⟨expr ⟩ ::= ⟨name⟩ | ⟨func ⟩ | ⟨app⟩

⟨func ⟩ ::= λ ⟨name⟩.⟨expr ⟩
⟨app⟩ ::= ( ⟨expr ⟩ ⟨expr ⟩ )

Um nome (⟨name⟩) pode ser qualquer sequência de caracteres não

brancos: x, 7, arg, func, +
Exemplos

x λ f .λ a.(f a)
λ x .x (λ x .x λ a.λ b.a)
λ first .λ second .first λ x .(x x )

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 4 / 20

Aplicação de Funções

Noção de Redução
Aplicação de funções se dá por meio de substituição

Exemplos
(λ x .x y )
(λ x .x λ x .x )
(λ x .x λ s.(s s))
(λ s.(s s) λ x .x )
(λ s.(s s) λ s.(s s))
((λ f .λ a.(f a) λ x .x ) λ s.(s s))

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 5 / 20

Tipos de redução

Segundo MICHAELSON (2011) temos duas estratégias de redução:

Redução de ordem aplicativa (call-by-value): a expressão do argumento é
avaliada antes de ser passada.
Redução de ordem normal (call-by-name): a expressão do argumento não
é avaliada antes de ser passada.
Sempre avaliamos a expressão mais externa e a esquerda
Exemplo:
(λ y .y (λ x .x λ z .(λ x .x z )))
Em geral, utilizaremos a redução normal (call-by-name)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 6 / 20

Funções Simples em λ -Cálculo

Função identidade:

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)
Função aplicação:

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)
Função aplicação:
λ f .λ arg .(f arg )

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)
Função aplicação:
λ f .λ arg .(f arg )
Função de seleção de argumentos (primeiro ou segundo):

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)
Função aplicação:
λ f .λ arg .(f arg )
Função de seleção de argumentos (primeiro ou segundo):
λ first .λ second .first

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)
Função aplicação:
λ f .λ arg .(f arg )
Função de seleção de argumentos (primeiro ou segundo):
λ first .λ second .first
Função sobre tuplas:

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Funções Simples em λ -Cálculo

Função identidade:
λ x .x
Função de auto-aplicação:
λ s.(s s)
Função aplicação:
λ f .λ arg .(f arg )
Função de seleção de argumentos (primeiro ou segundo):
λ first .λ second .first
Função sobre tuplas:
λ first .λ second .λ f .((f first ) second )

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 7 / 20

Açúcar Sintático

Lambda cálculo não tem constantes e as funções são anônimas

Manipular λ expressões complexas pode ser tedioso!

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 8 / 20

Açúcar Sintático

Lambda cálculo não tem constantes e as funções são anônimas

Manipular λ expressões complexas pode ser tedioso!
Vamos introduzir uma notação mais conveniente para representar
expressões λ
def ⟨name⟩ = ⟨func⟩
Exemplos:
def id = λ x .x def self = λ s.(s s) def apply = λ f .λ a.(f a)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 8 / 20

Açúcar Sintático

Lambda cálculo não tem constantes e as funções são anônimas

Manipular λ expressões complexas pode ser tedioso!
Vamos introduzir uma notação mais conveniente para representar
expressões λ
def ⟨name⟩ = ⟨func⟩
Exemplos:
def id = λ x .x def self = λ s.(s s) def apply = λ f .λ a.(f a)
Uso dos nomes definidos na aplicação de funções
(id id) (self id) ((apply self) id)
A substituição dos nomes pelas respectivas definições resulta no λ -termo
original
A substituição de um nome pela sua definição associada será denotada
por ==
Exemplo: (id y) == (λ x .x y)
Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 8 / 20
β -redução

Formalmente, a substituição de uma variável por um argumento no corpo

da função é chamada β -redução (beta-redução) e será denotada por ⇒
(ou ⇒β )
Exemplos:
(id self) == (λ x .x λ s.(s s)) ⇒ λ s.(s s)
((apply id) self) == ((λ f .λ a.(f a) id) self) ⇒ (λ a.(id a) self) ⇒ (id self) ==
(λ x .x λ s.(s s)) ⇒ λ s.(s s)
Uma expressão que possui uma aplicação de função que pode ser
reduzida é chamada redex
Uma expressão se encontra na forma normal quando não apresenta
redexes

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 9 / 20

Variáveis livres e ligadas

Como deve ser realizada a substituição no seguinte λ -termo?

(λ f .(f λ f .f ) λ s.(s s))

Para uma função arbitrária:

λ ⟨name⟩.⟨body ⟩

O escopo da variável ⟨name⟩ é ⟨body ⟩

Uma variável é ligada a ocorrências no corpo de uma função para a qual
está associada, desde que nenhuma outra função dentro do corpo
introduza a mesma variável. Caso contrário, ela é livre na expressão.

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 10 / 20

Variáveis livres e ligadas (Exemplos)

A variável x é ligada na expressão λ x .x e livre na expressão x

Na expressão λ f .(f λ x .x ), a variável f é ligada, mas na expressão
(f λ x .x ) a variável f é livre
Na expressão (λ f .(f λ f .f ) λ s.(s s)) quais são as variáveis livres e
ligadas em cada subexpressão?
E na expressão λ g .((g λ h.(h (g λ h.(h λ g .(h g ))))) g )?

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 11 / 20

Ordem normal de aplicação

Em geral a ordem normal para a β -redução em uma aplicação:

(λ ⟨name⟩.⟨body ⟩ ⟨argument ⟩)

nós substituímos todas as ocorrências livres de ⟨name⟩ em ⟨body ⟩ por

⟨argument ⟩.
Dessa forma, como ficará a β -redução na expressão:

(λ f .(f λ f .f ) λ s.(s s))

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 12 / 20

Conflito de nomes

Em alguns casos o uso de uma mesma variável pode criar problemas

para a redução de expressões
Considerando a função def apply = λ func .λ arg .(func arg )
Observe a λ -expressão a seguir:

((apply arg ) boing )

Se fizermos a β -redução como:

((apply arg ) boing ) == ((λ func .λ arg .(func arg ) arg ) boing )

⇒ (λ arg .(arg arg ) boing ) ⇒ (boing boing )

Observe que criou-se uma nova ocorrência da variável arg na função!

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 13 / 20

α -conversão

Para evitar criar inconsistências causadas por conflitos de nomes,

podemos realizar substituições consistentes de variáveis, chamada
α -conversão (alfa-conversão)
Para uma função:
λ ⟨name1⟩.⟨body ⟩
o nome name1 e todas as ocorrências livres de name1 em ⟨body ⟩ podem
ser substituídas por um novo nome name2 desde que name2 não seja o
nome de uma variável livre em λ ⟨name1⟩.⟨body ⟩
Como ficaria uma α -conversão na expressão (λ f .(f λ f .f ) λ s.(s s))
substituindo f por g na primeira função?

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 14 / 20

η -redução
A aplicação de uma função da forma:

λ ⟨name⟩.(⟨expression⟩ ⟨name⟩)

a um argumento genérico ⟨argument ⟩ é equivalente a:

(λ ⟨name⟩.(⟨expression⟩ ⟨name⟩) ⟨argument ⟩)

⇒ (⟨expression⟩ ⟨argument ⟩)
O que é equivalente a aplicação direta de ⟨expression⟩ sobre o
argumento
Podemos realizar uma simplificação de

λ ⟨name⟩.(⟨expression⟩ ⟨name⟩)

para ⟨expression⟩ chamada η -redução (eta-redução)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 15 / 20
Representando Valores Lógicos

Escolher λ -termos para representar valores lógicos true e false

Motivação: expressão condicional
def cond = λ e1 .λ e2 .λ c .((c e1 ) e2 )
Expressão tal que quando c for true o resultado é e1 . Se c for false,
resulta em e2

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 16 / 20

Representando Valores Lógicos

Escolher λ -termos para representar valores lógicos true e false

Motivação: expressão condicional
def cond = λ e1 .λ e2 .λ c .((c e1 ) e2 )
Expressão tal que quando c for true o resultado é e1 . Se c for false,
resulta em e2
Funções de seleção:
def true = λ t .λ f .t
def false = λ t .λ f .f

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 16 / 20

Representando Valores Lógicos

Escolher λ -termos para representar valores lógicos true e false

Motivação: expressão condicional
def cond = λ e1 .λ e2 .λ c .((c e1 ) e2 )
Expressão tal que quando c for true o resultado é e1 . Se c for false,
resulta em e2
Funções de seleção:
def true = λ t .λ f .t
def false = λ t .λ f .f
Avalie as expressões:
(((cond ⟨expr 1⟩) ⟨expr 2⟩) true)
(((cond ⟨expr 1⟩) ⟨expr 2⟩) false)
Note que o valor lógico é o último argumento de cond

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 16 / 20

Funções Lógicas

Negação (not):

Entrada Saída
λ t .λ f .t true λ t .λ f .f
λ t .λ f .f false λ t .λ f .t

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 17 / 20

Funções Lógicas

Negação (not):

Entrada Saída
def not = λ p.(((cond false) true) p)
λ t .λ f .t true λ t .λ f .f
= ...
λ t .λ f .f false λ t .λ f .t

Teste a função:
1. (not true)
2. (not false)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 17 / 20

Funções Lógicas

Conjunção (and):

Entrada Saída
λ t .λ f .t λ t .λ f .t λ t .λ f .t
λ t .λ f .t λ t .λ f .f λ t .λ f .f
λ t .λ f .f λ t .λ f .t λ t .λ f .f
λ t .λ f .f λ t .λ f .f λ t .λ f .f

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 17 / 20

Funções Lógicas

Conjunção (and):

Entrada Saída
λ t .λ f .t λ t .λ f .t λ t .λ f .t
def and = λ e1 .λ e2 .(((cond e2 ) false) e1 )
λ t .λ f .t λ t .λ f .f λ t .λ f .f
= ...
λ t .λ f .f λ t .λ f .t λ t .λ f .f
λ t .λ f .f λ t .λ f .f λ t .λ f .f

Teste a função:
1. ((and true) false)
2. ((and false) true)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 17 / 20

Funções Lógicas

Disjunção (or):

Entrada Saída
λ t .λ f .t λ t .λ f .t λ t .λ f .t
λ t .λ f .t λ t .λ f .f λ t .λ f .t
λ t .λ f .f λ t .λ f .t λ t .λ f .t
λ t .λ f .f λ t .λ f .f λ t .λ f .f

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 17 / 20

Funções Lógicas

Disjunção (or):

Entrada Saída
λ t .λ f .t λ t .λ f .t λ t .λ f .t
def or = λ e1 .λ e2 .(((cond true) e2 ) e1 )
λ t .λ f .t λ t .λ f .f λ t .λ f .t
= ...
λ t .λ f .f λ t .λ f .t λ t .λ f .t
λ t .λ f .f λ t .λ f .f λ t .λ f .f

Teste a função:
1. ((or true) true)
2. ((or false) false)

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 17 / 20

Operações aritméticas

Também existem definições em Lambda Cálculo para a representação de

valores numéricos e operações aritméticas
Algumas dessas definições são apresentadas na lista de exercícios
Assumindo essas definições, podemos calcular expressões aritméticas
da forma:
(+ 9 4) ⇒ 13
Observe que utilizamos notação pré-fixada
Vejamos mais um exemplo:

(+ (∗ 5 6) (∗ 8 3)) ⇒ (+ 30 (∗ 8 3)) ⇒ (+ 30 24) ⇒ 54

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 18 / 20

Lambda Cálculo em linguagens de programação

Algumas linguagens de programação não funcionais suportam o uso de

funções lambda (anômimas)
É o caso da linguagem Python. Vamos ver alguns exemplos:

No seguinte arquivo do Colab se encontram mais exemplos.

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 19 / 20
Referências

MICHAELSON, G. An introduction to functional programming through

lambda calculus, 2011.

Luiz Maurílio Maciel (DCC/UFJF) Lambda Cálculo 20 / 20