Codificação de Church

CODIFICAÇÃO DE CHURCH

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

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

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

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 f$f^{(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

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

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

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

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

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:

nil ≡ pair true true

isnil ≡ fst

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:

cons ≡ pair

head ≡ fst

tail ≡ snd

nil ≡ false

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

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

• Directly Reflective Meta-Programming
• Church numerals and booleans explained by Robert Cartwright at Rice University
• Theoretical Foundations For Practical 'Totally Functional Programming' (Chapters 2 and 5) All about Church and other similar encodings, including how to derive them and operations on them, from first principles
• Some interactive examples of Church numerals

Ver também

• Lambda calculus
• System F for Church numerals in a typed calculus
• Mogensen–Scott encoding