Skip to content

lambda calculus

Jump to bottom
Manoel Vilela edited this page Jan 31, 2018 · 2 revisions

Talk λ-calculus

Nessa conversa discutimos um pouco sobre a natureza do lambda calculus, a gramática e seus exemplos.

Data: 30/01/2018

Participantes:

  • André Zanella
  • Leonardo Neumann
  • Manoel Vilela
  • Christian Ferraz
  • Pedro HLC
  • Rafael Campos Nunes

Gramática formal

As entidades existentes no cálculo lambda:

  1. Funções
  2. Variáveis
  3. Aplicações

Sintaxe Formal (EBNF):

  <exp> ::= <app> | <abs> | <var>
  <app> ::= <exp> <exp>
  <abs> ::= 'λ' <var> '.' <exp>
  <var> ::= [a-z]

  <exp> = Expressão Lambda Cálculo
  <abs> = Abstração
  <var> = Variável
  <app> = Aplicação

Exemplos

Funções identidades de n-parâmetros

  1. λi.i
  2. λa.λb.a b
  3. λa.λb.λc.a b c
  
  1. Função identidade de um parâmetro
     (λi.i) (λi.i) 
  => (λi.i)

  2. Função identidade de dois parâmetros
     ((λa.λb.a b) (λi.i)) (λi.i) 
  => (λb.(λi.i) b) (λi.i)
  => (λi.i) (λi.i)
  => (λi.i)
  
  3. Função identidade de três parâmetros
     (λa.λb.λc.a b c) (λi.i) (λi.i) (λi.i) 
  => (λb.λc.(λi.i) b c) (λi.i) (λi.i)
  => (λc.(λi.i) (λi.i) c) (λi.i)
  => (λi.i) (λi.i) (λi.i) 
  => (λi.i) (λi.i)
  => (λi.i)

  Ad infinitum n-id function.

Boolean Logic

TRUE := λx.λy.x
FALSE := λx.λy.y
AND := λp.λq.p q p
OR := λp.λq.p p q
NOT := λp.λa.λb.p b a
IFTHENELSE := λp.λa.λb.p a b

Exemplo 1:

   AND TRUE FALSE
=> (λp.λq.p q p) (λx.λy.x) (λx.λy.y)
=> (λq.(λx.λy.x) q (λx.λy.x)) (λx.λy.y)
=> (λx.λy.y) (λx.λy.x) (λx.λy.y)
=> (λy.y) (λx.λy.y)
=> (λx.λy.y)
=> FALSE

Exemplo 2:

   OR TRUE FALSE
   (λp.λq.p p q) (λx.λy.x) (λx.λy.y)
=> (λq.(λx.λy.x) (λx.λy.x) q) (λx.λy.y)
=> ((λx.λy.x) (λx.λy.x)) (λx.λy.y)
=> (λy.(λx.λy.x)) (λx.λy.y)
=> (λx.λy.x)
=> TRUE

Exemplo 3:

   NOT TRUE
   (λp.λa.λb.p b a) (λx.λy.x)
=> (λa.λb.(λx.λy.x) b a)
=> (λa.λb.(λy.b) a)
=> (λa.λb.b)
=> FALSE

Exemplo 4:

   NOT FALSE
   (λp.λa.λb.p b a) (λx.λy.y)
=> (λa.λb.(λx.λy.y) b a)
=> (λa.λb.(λy.y) a)
=> (λa.λb.a)
=> TRUE

Exemplo 5:

   IFTHENELSE TRUE FALSE TRUE
   (λp.λa.λb.p a b) (λx.λy.x) (λx.λy.y) (λx.λy.x) 
=> (λa.λb.(λx.λy.x) a b) (λx.λy.y) (λx.λy.x) 
=> (λb.(λx.λy.x) (λx.λy.y) b) (λx.λy.x)
=> (λx.λy.x) (λx.λy.y) (λx.λy.x)
=> (λx.λy.x) (λa.λb.b) (λc.λd.c) ;; conversão-α, a=c=x, b=d=y
=> (λy.(λa.λb.b)) (λc.λd.c)
=> (λa.λb.b)  ;; conversão-α
=> (λx.λy.y)

Church Numerals & Arithmetics

0 := λf.λx.x
1 := λf.λx.f x
2 := λf.λx.f (f x)
3 := λf.λx.f (f (f x))

SUCC := λn.λf.λx.f (n f x)
PLUS := λm.λn.λf.λx.m f (n f x)
MULT := λm.λn.λf.m (n f)

Exemplo 1

   PLUS 0 0
   (λm.λn.λf.λx.m f (n f x)) (λf.λx.x) (λf.λx.x)
=> (λf.λx.(λf.λx.x) f ((λf.λx.x) f x)
=> (λf.λx.(λx.x) (λx.x) x)
=> (λf.λx.(λx.x) x)
=> λf.λx.x

Exemplo 2

   PLUS 0 1
   (λm.λn.λf.λx.m f (n f x)) (λx.λy.y) (λx.λy.x y)
=> (λn.λf.λx.(λx.λy.y) f (n f x)) (λx.λy.x y)
=> (λf.λx.(λx.λy.y) f ((λx.λy.x y) f x))
=> (λf.λx.(λx.λy.y) f ((λy y) f))

Exemplo 3

   PLUS 1 1
=> (λm.λn.λf.λx.m f (n f x)) (λf.λx.f x) (λf.λx.f x)
=> (λn.λf.λx.(λf.λx.f x) f (n f x)) (λf.λx.f x)
=> (λf.λx.(λf.λx.f x) f ((λf.λx.f x) f x))
=> (λf.λx.(λf.λx.f x) f ((λx.f x) x))
=> (λf.λx.(λf.λx.f x) f (f x))
=> (λf.λx.f (f x))

Exemplo 4

   MULT 0 1
=> (λm.λn.λf.m (n f)) (λx.λy.y) (λx.λy.x y)
=> (λn.λf.(λx.λy.y) (n f)) (λx.λy.x y)
=> (λf.(λx.λy.y) (λx.λy.x y) f)
=> (λf.(λx.λy.y) λy.f y)
=> (λf.(λx.λy.y) f)
=> (λx.λy.y)
=> 0

Exemplo 5

   MULT 1 1
=> (λm.λn.λf.m (n f)) (λf.λx.f x) (λf.λx.f x)
=> (λn.λf.(λf.λx.f x) (n f)) (λf.λx.f x)
=> (λf.(λf.λx.f x) ((λf.λx.f x) f))
=> (λf.(λx.((λf.λx.f x) f) x))
=> (λf.(λx.(λx.f x) x))
=> (λf.λx.f x)
=> 1

Exemplo 6

	MULT 2 2
=> (λm.λn.λf.m (n f)) (λa.λb.a (a b)) (λc.λd.c (c d)) ;; uso de α-conversão
=> (λn.λf.(λa.λb.a (a b)) (n f)) (λc.λd.c (c d))
=> (λf.(λa.λb.a (a b)) ((λc.λd.c (c d)) f))
=> (λf.λb.((λc.λd.c (c d)) f) (((λc.λd.c (c d)) f) b))
=> (λf.λb.(λd.f (f d)) (((λc.λd.c (c d)) f) b))
=> (λf.λb.f (f (((λc.λd.c (c d)) f) b)))
=> (λf.λb.f (f ((λd.f (f d)) b)))
=> (λf.λb.f (f (f (f b))))

Exemplo 7

   SUCC 0
=> (λn.λf.λx.f (n f x) (λx.λy.y))
=> (λf.λx.f (λx.λy.y f x))
=> (λf.λx.f (λy.y x))
=> λf.λx.f x
=> 1


   SUCC 1
=> (λn.λf.λx.f (n f x)) (λx.λy.x y)
=> (λf.λx.f (λx.λy.x y)f x)
=> (λf.λx.f (λy.f y) x)
=> λf.λx.f (f x)
=> 2


   SUCC 2
=> (λn.λf.λx.f (n f x)) (λx.λy.x (x y))
=> (λf.λx.f ((λx.λy.x (x y)) f x))
=> (λf.λx.f ((λy.f (f y)) x))
=> λf.λx.f (f (f x))
=> 3


   SUCC 3
=> (λn.λf.λx.f (n f x)) (λf.λx.f (f (f x)))
=> (λf.λx.f ((λf.λx.f (f (f x))) f x))
=> (λf.λx.f ((λx.f (f (f x)) x))
=> λf.λx.f (f (f (f x)))
=> 4


   SUCC 4
=> (λn.λf.λx.f (n f x)) (λf.λx.f (f (f (f x))))
=> (λf.λx.f (λf.λx.f (f (f (f x))) f x))
=> (λf.λx.f (λx.f (f (f (f (f ))) x))
=> (λf.λx.f (f (f (f (f x)))))
=> 5


   SUCC 5
=> (λn.λf.λx.f (n f x)) (λf.λx.f (f (f (f (f x)))))
=> (λf.λx.f ((λf.λx.f (f (f (f (f x))))) f x))
=> (λf.λx.f ((λx.f (f (f (f (f x))))) x)
=> (λf.λx.f (f (f (f (f (f x))))))
=> 6

// Paramos por aqui

Y-combinator (requisição do @pedrohlc)

Y := λf.(λx.f (x x)) (λx.f (x x))  

   Y SUCC
=> (λf.(λx.f (x x)) (λx.f (x x))) (λn.λf.λx.f (n f x)) 
=> (λx.(λn.λf.λx.f (n f x)) (x x)) (λx.(λn.λf.λx.f (n f x)) x x))
=> (λx.(λn.λf.λx.f (n f x)) (x x)) (λx.(λn.λf.λx.f (n f x)) x x))
=> PAUSE (TENTAR RESOLVER ISSO AQUI É LOOP INFINITO?) sim.
Clone this wiki locally