Codificação de Church

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Broom icon.svg
As referências deste artigo necessitam de formatação (desde outubro de 2011).
Por favor, utilize fontes apropriadas contendo referência ao título, autor, data e fonte de publicação do trabalho para que o artigo permaneça verificável no futuro.
Ambox rewrite.svg
Esta página precisa ser reciclada de acordo com o livro de estilo (desde outubro de 2011).
Sinta-se livre para editá-la para que esta possa atingir um nível de qualidade superior.

CODIFICAÇÃO DE CHURCH[editar | editar código-fonte]

Em matemática, a codificação de Church é uma forma de incorporar dados e operadores ao cálculo lambda, a forma mais conhecida dos numerais de Church, uma representação dos números naturais usando a notação lambda. O método é conhecido como Alonzo Church, que foi o primeiro a codificar os dados no cálculo lambda desta forma. Termos que são geralmente considerados primitivos em outras notações (com inteiros, booleanos e pares, por exemplo) são mapeados para funções de ordem superior na codificação de Church. A tese de Church-Turing afirma que qualquer operador computável (e seus operandos) pode ser representado sob a codificação de Church. Muitos estudantes de matemática estão familiarizados com a numeração de Gödel de elementos de um conjunto. A codificação de Church é uma operação equivalente, definida sob lambda-abstrações, o invés de números naurais.

Os Numerais de Church[editar | editar código-fonte]

Os numerais de Church são as representações dos números naturais através da codificação de Church. A função de ordem mais alta, que representa o número natural n é uma função que mapeia qualquer função f à sua composição n-fecho. Em termos mais simples, o valor de um numeral é equivalente ao número de vezes de que a função encapsula seu argumento.

f^n = f \circ f \circ \cdots \circ f.\,

Definição[editar | editar código-fonte]

Todos os numerais de Church são funções que tomam dois parâmetros. Aqui f é a função sucessor e x representa . Os numerais de Church 0,1,2,… são definidos a seguir, no cálculo lambda:

0λf.λx. x
1λf.λx. f x
2λf.λx. f (f x)
3λf.λx. f (f (f x))
...
nλf.λx. fn x
...

Isto é, o número natural n é representado pelo numeral de Church n, que tem a propriedade que, para quaisquer lambda termos F e X, F e X

n F X =β Fn X

Cálculo com os numerais de Church[editar | editar código-fonte]

No cálculo lambda, as funções numéricas são representáveis por funções correspondentes nos numerais de Church. Estas funções podem ser implementadas na maioria das linguagens de programação funcional (sujeitas à restrição de tipo) pela translação direta de lambda termos.

A função adição plus(m,n)=m+n usa a identidade f^{(m+n)}(x)=f^m(f^n(x)).

plusλm.λn.λf.λx. m f (n f x)

A função sucessor succ(n)=n+1 é β-equivalente a (plus 1).

succλn.λf.λx. f (n f x).

A função multiplicação mult(m,n)=m*n usa a identidade ff^{(m*n)} = (f^n)^m.

multλm.λn.λf.λx. m (n f) x.

A função exponencial exp(m,n)=m^n segue-se a partir do uso da função multiplicação definida acima.

expλm.λn. n (mult m) 1.

A função predecessor

\operatorname{pred}(n) = \begin{cases} 0 & \mbox{se }n=0, \\ n-1 & \mbox{caso contrário}\end{cases}.

A função predecessor gera uma composição n-fecho de funções em que cada uma aplica seu argumento g para f; o caso base descarta sua cópia de f e retorna x.

predλn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

A função subtração pode ser escrita baseada na função predecessor:

subλm.λn. (n pred) m

O predicado zero pode ser escrito como:

zero?λn. n (λx.F) T

Agora:

zero? n =β T if n =β 0.
zero? n =β F if nβ 0, desde que n é um numeral de Church onde ≠β é a negação de =β restrita aos lambda termos redutíveis.

T e F podem ser termos arbitrários, como por exemplo, termos Booleanos.

Translação com outras representações[editar | editar código-fonte]

A maioria das linguagens do mundo real tem suporte para máquinas nativas de inteiros; as funções de Church e as 

não-Church (dadas aqui em Haskell) convertem inteiros não-negativos em seus correspondentes numerais de Church. As implementações destas conversões em outras linguagens são similares.


type Church a = (a -> a) -> (a -> a)

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch n = n (\x -> x + 1) 0

Em Haskell, a \ corresponde ao λ do lambda cálculo.

Booleanos de Church[editar | editar código-fonte]

Os booleanos de Church são os codificadores dos valores booleanos verdadeiro ou falso. Algumas linguagens de programação usam estes como um modelo de implementação para aritmética booleana; como exemplos, Smalltalk e Pico. Os valores booleanos são representados como funções de dois valores que são avaliadas como um ou outro de seus argumentos.

A seguir, a definição formal em cálculo lambda:

trueλa.λb. a
falseλa.λb. b

Note que esta função permite predicados (isto é, funções retornando valores lógicos) para atuar diretamente como cláusulas se, como por exemplo, se predicado é um predicado unário,

predicado x cláusula então cláusula senão

avalia a cláusula então se predicado x assume verdadeiro, e para cláusula senão se predicado x assume falso.

As funções da aritmética booleana podem ser derivadas dos booleanos de Church:

andλm.λn. m n m
orλm.λn. m m n
notλm.λa.λb. m b a
xorλm.λn.λa.λb. m (n b a) (n a b)

Alguns exemplos:

e verdadeiro falso(λm.λn. m n m) (λa.λb. a) (λa.λb. b) ≡ (λa.λb. a) (λa.λb. b) (λa.λb. a)(λa.λb. b)falso
ou verdadeiro falso(λm.λn. m m n) (λa.λb. a) (λa.λb. b)(λa.λb. a) (λa.λb. a) (λa.λb. b)(λa.λb. a)verdadeiro
não verdadeiro(λm.λa.λb. m b a) (λa.λb. a)(λa.λb. (λa.λb. a) b a)(λa.λb. b)falso

Pares de Church[editar | editar código-fonte]

Os pares de Church são os codificadores de Church para os pares (duplas). O par é representado como uma função que recebe um argumento de função. Quando seu argumento é dado, ela o aplicará aos dois componentes do par.

Definição formal em cálculo lambda:

pairλx.λy.λz.z x y
fstλp.p (λx.λy.x)
sndλp.p (λx.λy.y)

Exemplo:

fst (pair a b) ≡ λp.p (λx.λy.x) ((λx.λy.λz.z x y) a b) ≡ λp.p (λx.λy.x) (λz.z a b) ≡ (λz.z a b) (λx.λy.x) ≡ (λx.λy.x) a b ≡ a

Lista de codificadores[editar | editar código-fonte]

Um codificador de listas (imutáveis) de comprimento variável deve definir um construtor para criar uma lista vazia (nil), uma operação que testa quando ou não uma lista é vazia (isnil), um operação para colocar um valor dado em uma (possivelmente vazia) lista (cons) e duas operações para determinar o primeiro elemento e a lista dos elementos restantes de uma lista não-vazia (head e tail).

Pares de Church[editar | editar código-fonte]

Uma lista não-vazia pode ser basicamente codificada por um par de Church com a cabeça da lista armazenada no primeiro componente do par e o fim da lista no segundo componente. Entretanto, casos especiais são necessários para decodificar de maneira inequívoca a lista vazia. Isto pode ser conseguido pelo encapsulamento de qual qualquer nó individual da lista com outro par com o segundo componente contendo o nó da lista e o primeiro componente contendo um booleano de Church, que é verdadeiro para a lista vazia e falso caso contrário, similarmente às uniões disjuntas. Usando esta ideia, uma lista básica de operações pode ser definida, tal como:[1]

nilpair true true
isnilfst
cons ≡ λh.λt.pair false (pair h t)
head ≡ λz.fst (snd z)
tail ≡ λz.snd (snd z)

O Segundo componente do par codificado nil nunca é usado, desde que head e tail sejam somente aplicados a listas não-vazias. Alternativamente, pode-se definir:[2]

conspair
headfst
tailsnd
nilfalse
isnil ≡ λl.l (λh.λt.λd.false) true

Onde a última definição é um caso especial de

process-list ≡ λl.l (λh.λt.λd. head-and-tail-clause) nil-clause.

Função de ordem superior[editar | editar código-fonte]

Como alternative para codificação usando os pares de Church, uma lista pode ser codificada pela identificação com sua função de acumulação à direita. Por exemplo, uma lista de três elementos x,y e z, pode ser codificada por uma função de ordem superior que, quando aplicada ao combinador c e um valor n, retorna c x (c y (c z n)).

Referências

  1. Pierce, Benjamin C.. Types and Programming Languages. [S.l.]: MIT Press, 2002. 500 pp. ISBN 978-0262162098
  2. John Tromp, Binary Lambda Calculus and Combinatory Logic (outubro 2008). Randomness And Complexity, from Leibniz To Chaitin (PDF) (em inglês). Cristian S. Calude, World Scientific Publishing Company. Cwi.nl.

Ver também[editar | editar código-fonte]