O Cálculo como
Linguagem de Programação
Rafael Dueire Lins
Departamento de Informática
Universidade Federal de Pernambuco - Recife - Brasil
O -Cálculo: Sintaxe
< expr :: <variável
| <expr<expr
| <variável.<expr
| <constante
aplicação
abstração
abc = (ab)c aplicação é associativa à
esquerda
O -Cálculo:
Semântica Operacional
 Conversão-a:
 Conversão-:
Substituição de parâmetros reais por
parâmetros formais
(x.t ) s  [ s / x ] t
A
Conversão-:
Extensionalidade do sistema
(x.x )  
O -Cálculo
Teoremas de Church-Rosser
1. Formas normais são únicas.
(módulo conversão-a)
2. -reduzir a expressão mais externa e mais
à esquerda a cada ponto numa sequência
de reduções leva a forma normal, se ela
existir.
Operações Booleanas

Valores Lógicos
true = a. b.a
 
false =
(K )
a.b.b
((true)P)Q
((false)P)Q

 

 
(( KI ))
P
Q
Comando If-Then-Else
if C then P else Q

 C P Q
Assim:
if true then P else Q

 
if false then P else Q

 
P
Q
Operadores Booleanos
Not = b. if b then false else true
Or =
And =
 b. c.if b then true else c
b. c.if b then c else false
Lemas









not true = false
not false = true
or true true = false
or true false = true
or false false = false
and true true = true
and true false = false
and false true = false
and false false = false
Numerais de Church
Representação dos Números
Naturais em Lambda Calculus
 Definições:

• 0 =  f. x.x
• succ =  n.  f.  x.f ( n f x )
• repita n vezes f em x = n f x
Sucessor de um Número
 n.  f. x.f( n f x ) 0
   f.  x.f( 0 f x )

 f.  x.f((  f.  x.x) f x )
=
  
 
f. x.f((  x.x) x )
  
 
f. x.fx
Assim, se (  f.  x.fx) recebe o valor
succ 0 =

de 1:
3 = succ(succ(succ(0)))
Numerais de Church
0 = f. x.x
1 = f. x.fx
2 = f. x.f x
...
2
n = f.  x.f x
n+1
n+1 =  f.  x.f x
Numerais de Church: Adição
A adição entre dois Numerais de
Church m e n pode ser feita
computando-se o sucessor de n m
vezes, o combinador da adição seria
representado por:
add =  m. n. repita m vezes succ sobre n
Adição
add a b = (  m.  n.m succ n) a b

a succ b
 

succ a b
 
= succ(succ(...(succ b)...))

 
...
a vezes
succ(succ(...(succ b+1)...))
(a - 1) vezes

 

 
succ(b + a - 1)
b+a
Numerais de Church: Multiplicação
A multiplicação entre dois números
m e n pode ser definida como sendo
a adição de n a 0, um número m de
vezes.
mult =  m.
n. repita m vezes add n sobre 0
Multiplicação
mult a b = (  m.  n.m(add n) 0 ) a b
a

a (add b) 0
 
=
(add b) 0
= add b(add b(...(add b 0)...)

...
a vezes
 
add b(add b(...(add b + b)...)

(a - 1) vezes
 

 
add b( b + b + b ... + b + b)
(a - 1) vezes
b + b + b ... + b + b = a * b
a vezes
Numerais de Church: Exponenciação
n
A exponenciação de m pode ser
definida como a multiplicação de m a
1, um número n de vezes.
exp =  m. n. repita n vezes mult m sobre 1
Exponenciação
exp a b = (  m. n.n(mult m) 1) a b

  b (mult a) 1

  (mult a) 1
= mult a(mult a(...(mult a 1)..)

...
b vezes
 
mult a(a * a * ... * a * a)

(b - 1) vezes
 
b
a
Pares Ordenados
Um Par Ordenado é uma estrutura
algébrica para a manipulação de
elementos aos pares. De modo que
uma operação realizada sobre um
dado elemento não afete o
comportamento do outro.
<a,b> -> x.x a b
Pares Ordenados
Para obtermos cada elemento de um par
ordenado, devemos definir os
combinadores fst e snd:
fst =  p.p true
snd =  p.p false
Representação:
<fst, snd>
Pares Ordenados
Função Predecessor
predecessor x = x - 1, se x > 0
0 , se x <= 0
Combinador PRED :

pred =  n.snd (repita n vezes F sobre <0 . 0>
Onde:
F =  p. <(fst p) + 1, fst p>
Numerais de Church: Subtração
Especificada como:
minus a b = a - b, se a >= b
= 0, se a < b
Combinador:
minus =
m.n.(repita m vezes pred sobre n)
Fatorial
O combinador que computa o fatorial
de um numeral de Church pode ser
definido como:
fat =
 n.fst ( repita n vezes F sobre <1,1>)
Onde F é:
F=
 p.<(fst p)*(snd p),(snd p) + 1>
Operadores Relacionais
Primeiramente, definamos um
operador chamado IsZero
especificado como:
IsZero n = true, se n = 0
false, se n > 0
Correspondente a :
IsZero =  n.n(K false)(true)
Operadores Relacionais
Analogamente, temos :
NoZero n = true, se n > 0
false, se n = 0
Definido como :
NoZero =  n.n(K true)(false)
Operadores Relacionais
Maior Que
gt = n. m.(NoZero (minus n m))
Maior ou Igual A
ge = n.  m.(IsZero(minus m n))
Operadores Relacionais
Menor Que
lt = n. m.(NoZero(minus m n))
Menor ou Igual A
le =  n. m.(IsZero(minus n m))
Operadores Relacionais
Igual A
Um número n é igual a outro número
m quando m - n e n - m são iguais a
zero:
eq = n.m.(and(IsZero(minus n m))
(IsZero(minus m n)))
Amanhã:

Recursividade no -Cálculo.

Introdução a Lógica Combinatorial.

Máquina de Turner.