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]