Codificação de igreja - Church encoding

Em matemática , a codificação Church é um meio de representar dados e operadores no cálculo lambda . Os numerais da Igreja são uma representação dos números naturais usando a notação lambda. O método tem o nome de Alonzo Church , que primeiro codificou os dados no cálculo lambda desta forma.

Os termos que geralmente são considerados primitivos em outras notações (como inteiros, booleanos, pares, listas e uniões marcadas) são mapeados para funções de ordem superior na codificação Church. A tese de Church-Turing afirma que qualquer operador computável (e seus operandos) pode ser representado pela codificação Church. No cálculo lambda sem tipo, o único tipo de dado primitivo é a função.

A codificação Church não se destina a ser uma implementação prática de tipos de dados primitivos. Seu uso é para mostrar que outros tipos de dados primitivos não são necessários para representar qualquer cálculo. A completude é representacional. Funções adicionais são necessárias para traduzir a representação em tipos de dados comuns, para exibição às pessoas. Em geral, não é possível decidir se duas funções são extensionalmente iguais devido à indecidibilidade de equivalência do teorema de Church . A tradução pode aplicar a função de alguma forma para recuperar o valor que ela representa ou procurar seu valor como um termo lambda literal.

O cálculo lambda é geralmente interpretado como usando igualdade intensional . Existem problemas potenciais com a interpretação dos resultados devido à diferença entre a definição intensional e extensional de igualdade.

Numerais de igreja

Os numerais da igreja são as representações dos números naturais sob a codificação da igreja. A função de ordem superior que representa o número natural n é uma função que mapeia qualquer função para sua composição n- vezes . Em termos mais simples, o "valor" do numeral é equivalente ao número de vezes que a função encapsula seu argumento. ${\ displaystyle f}$

${\ displaystyle f ^ {\ circ n} = \ underbrace {f \ circ f \ circ \ cdots \ circ f} _ {n {\ text {vezes}}}. \,}$

Todos os numerais de igreja são funções que aceitam dois parâmetros. Os numerais da igreja 0 , 1 , 2 , ..., são definidos como segue no cálculo lambda .

Começando com 0 sem aplicar a função de forma alguma, prossiga com 1 aplicando a função uma vez, 2 aplicando a função duas vezes, 3 aplicando a função três vezes, etc .:

${\ displaystyle {\ begin {array} {r | l | l} {\ text {Número}} & {\ text {Definição da função}} & {\ text {Lambda expression}} \\\ hline 0 & 0 \ f \ x = x & 0 = \ lambda f. \ lambda xx \\ 1 & 1 \ f \ x = f \ x & 1 = \ lambda f. \ lambda xf \ x \\ 2 & 2 \ f \ x = f \ (f \ x) & 2 = \ lambda f. \ lambda xf \ (f \ x) \\ 3 & 3 \ f \ x = f \ (f \ (f \ x)) & 3 = \ lambda f. \ lambda xf \ (f \ (f \ x)) \ \\ vdots & \ vdots & \ vdots \\ n & n \ f \ x = f ^ {n} \ x & n = \ lambda f. \ lambda xf ^ {\ circ n} \ x \ end {array}}}$

O numeral da Igreja 3 representa a ação de aplicar qualquer função dada três vezes a um valor. A função fornecida é aplicada primeiro a um parâmetro fornecido e, em seguida, sucessivamente ao seu próprio resultado. O resultado final não é o numeral 3 (a menos que o parâmetro fornecido seja 0 e a função seja uma função sucessora ). A função em si, e não seu resultado final, é o numeral da Igreja 3 . O número 3 da Igreja significa simplesmente fazer qualquer coisa três vezes. É uma demonstração ostensiva do que se entende por "três vezes".

Cálculo com numerais de igreja

As operações aritméticas em números podem ser representadas por funções em numerais de Igreja. Essas funções podem ser definidas no cálculo lambda ou implementadas na maioria das linguagens de programação funcionais (consulte conversão de expressões lambda em funções ).

A função de adição usa a identidade . ${\ displaystyle \ operatorname {plus} (m, n) = m + n}$${\ displaystyle f ^ {\ circ (m + n)} (x) = f ^ {\ circ m} (f ^ {\ circ n} (x))}$

${\ displaystyle \ operatorname {plus} \ equiv \ lambda m. \ lambda n. \ lambda f. \ lambda xm \ f \ (n \ f \ x)}$

A função sucessora é β-equivalente a . ${\ displaystyle \ operatorname {succ} (n) = n + 1}$${\ displaystyle (\ operatorname {plus} \ 1)}$

${\ displaystyle \ operatorname {succ} \ equiv \ lambda n. \ lambda f. \ lambda xf \ (n \ f \ x)}$

A função de multiplicação usa a identidade . ${\ displaystyle \ operatorname {mult} (m, n) = m * n}$${\ displaystyle f ^ {\ circ (m * n)} (x) = (f ^ {\ circ n}) ^ {\ circ m} (x)}$

${\ displaystyle \ operatorname {mult} \ equiv \ lambda m. \ lambda n. \ lambda f. \ lambda xm \ (n \ f) \ x}$

A função de exponenciação é dada pela definição dos numerais da Igreja ,. Na definição, substitua por obter e, ${\ displaystyle \ operatorname {exp} (m, n) = m ^ {n}}$${\ displaystyle n \ h \ x = h ^ {n} \ x}$${\ displaystyle h \ para m, x \ para f}$${\ displaystyle n \ m \ f = m ^ {n} \ f}$

${\ displaystyle \ operatorname {exp} \ m \ n = m ^ {n} = n \ m}$

que dá a expressão lambda,

${\ displaystyle \ operatorname {exp} \ equiv \ lambda m. \ lambda nn \ m}$

A função é mais difícil de entender. ${\ displaystyle \ operatorname {pred} (n)}$

${\ displaystyle \ operatorname {pred} \ equiv \ lambda n. \ lambda f. \ lambda xn \ (\ lambda g. \ lambda hh \ (g \ f)) \ (\ lambda ux) \ (\ lambda uu)}$

Um numeral de Igreja aplica uma função n vezes. A função predecessora deve retornar uma função que aplica seu parâmetro n - 1 vezes. Isso é obtido construindo um contêiner em torno de f e x , que é inicializado de uma maneira que omite a aplicação da função na primeira vez. Veja predecessor para uma explicação mais detalhada.

A função de subtração pode ser escrita com base na função predecessora.

${\ displaystyle \ operatorname {menos} \ equiv \ lambda m. \ lambda n. (n \ operatorname {pred}) \ m}$

Tabela de funções em numerais de igreja

Função	Álgebra	Identidade	Definição de função	Expressões lambda
Sucessor	${\ displaystyle n + 1}$	${\ displaystyle f ^ {n + 1} \ x = f (f ^ {n} x)}$	${\ displaystyle \ operatorname {succ} \ n \ f \ x = f \ (n \ f \ x)}$	${\ displaystyle \ lambda n. \ lambda f. \ lambda xf \ (n \ f \ x)}$	...
Adição	${\ displaystyle m + n}$	${\ displaystyle f ^ {m + n} \ x = f ^ {m} (f ^ {n} x)}$	${\ displaystyle \ operatorname {plus} \ m \ n \ f \ x = m \ f \ (n \ f \ x)}$	${\ displaystyle \ lambda m. \ lambda n. \ lambda f. \ lambda xm \ f \ (n \ f \ x)}$	${\ displaystyle \ lambda m. \ lambda nn \ operatorname {succ} m}$
Multiplicação	${\ displaystyle m * n}$	${\ displaystyle f ^ {m * n} \ x = (f ^ {m}) ^ {n} \ x}$	${\ displaystyle \ operatorname {multiplicar} \ m \ n \ f \ x = m \ (n \ f) \ x}$	${\ displaystyle \ lambda m. \ lambda n. \ lambda f. \ lambda xm \ (n \ f) \ x}$	${\ displaystyle \ lambda m. \ lambda n. \ lambda fm \ (n \ f)}$
Exponenciação	${\ displaystyle m ^ {n}}$	${\ displaystyle n \ m \ f = m ^ {n} \ f}$	${\ displaystyle \ operatorname {exp} \ m \ n \ f \ x = (n \ m) \ f \ x}$	${\ displaystyle \ lambda m. \ lambda n. \ lambda f. \ lambda x. (n \ m) \ f \ x}$	${\ displaystyle \ lambda m. \ lambda nn \ m}$
Predecessor *	${\ displaystyle n-1}$	${\ displaystyle \ operatorname {inc} ^ {n} \ operatorname {con} = \ operatorname {val} (f ^ {n-1} x)}$	${\ displaystyle if (n == 0) \ 0 \ else \ (n-1)}$	${\ displaystyle \ lambda n. \ lambda f. \ lambda xn \ (\ lambda g. \ lambda hh \ (g \ f)) \ (\ lambda ux) \ (\ lambda uu)}$
Subtração *	${\ displaystyle mn}$	${\ displaystyle f ^ {mn} \ x = (f ^ {- 1}) ^ {n} (f ^ {m} x)}$	${\ displaystyle \ operatorname {menos} \ m \ n = (n \ operatorname {pred}) \ m}$	...	${\ displaystyle \ lambda m. \ lambda nn \ operatorname {pred} m}$

* Observe que na codificação da Igreja,

• ${\ displaystyle \ operatorname {pred} (0) = 0}$
• ${\ displaystyle m <= n \ a mn = 0}$

Derivação da função predecessora

A função predecessora usada na codificação Church é,

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

Para construir o predecessor, precisamos de uma maneira de aplicar a função 1 menos tempo. Um numeral n aplica a função f n vezes a x . A função predecessora deve usar o numeral n para aplicar a função n -1 vezes.

Antes de implementar a função predecessora, aqui está um esquema que envolve o valor em uma função de contêiner. Definiremos novas funções para usar no lugar de f e x , chamadas inc e init . A função do contêiner é chamada de valor . O lado esquerdo da tabela mostra um numeral n aplicado a inc e init .

${\ displaystyle {\ begin {array} {r | r | r} {\ text {Número}} & {\ text {Usando init}} & {\ text {Usando const}} \\\ hline 0 & \ operatorname {init } = \ operatorname {valor} \ x & \\ 1 & \ operatorname {inc} \ \ operatorname {init} = \ operatorname {valor} \ (f \ x) & \ operatorname {inc} \ \ operatorname {const} = \ operatorname {value} \ x \\ 2 & \ operatorname {inc} \ (\ operatorname {inc} \ \ operatorname {init}) = \ operatorname {value} \ (f \ (f \ x)) & \ operatorname {inc} \ (\ operatorname {inc} \ \ operatorname {const}) = \ operatorname {valor} \ (f \ x) \\ 3 & \ operatorname {inc} \ (\ operatorname {inc} \ (\ operatorname {inc} \ \ operatorname {init})) = \ operatorname {valor} \ (f \ (f \ (f \ x))) & \ operatorname {inc} \ (\ operatorname {inc} \ (\ operatorname {inc} \ \ operatorname {const })) = \ operatorname {valor} \ (f \ (f \ x)) \\\ vdots & \ vdots & \ vdots \\ n & n \ operatorname {inc} \ \ operatorname {init} = \ operatorname {valor} \ (f ^ {n} \ x) = \ operatorname {valor} \ (n \ f \ x) & n \ operatorname {inc} \ \ operatorname {const} = \ operatorname {valor} \ (f ^ {n-1} \ x) = \ o peratorname {valor} \ ((n-1) \ f \ x) \\\ end {array}}}$

A regra geral de recorrência é,

${\ displaystyle \ operatorname {inc} \ (\ operatorname {valor} \ v) = \ operatorname {valor} \ (f \ v)}$

Se também houver uma função para recuperar o valor do contêiner (chamada de extração ),

${\ displaystyle \ operatorname {extract} \ (\ operatorname {value} \ v) = v}$

Em seguida, extrair pode ser usado para definir a função samenum como,

${\ displaystyle \ operatorname {samenum} = \ lambda n. \ lambda f. \ lambda x. \ operatorname {extrato} \ (n \ operatorname {inc} \ operatorname {init}) = \ lambda n. \ lambda f. \ lambda x. \ operatorname {extrato} \ (\ operatorname {valor} \ (n \ f \ x)) = \ lambda n. \ lambda f. \ lambda xn \ f \ x = \ lambda nn}$

A função samenum não é intrinsecamente útil. No entanto, como inc delega a chamada de f para seu argumento de contêiner, podemos fazer com que no primeiro aplicativo inc receba um contêiner especial que ignora seu argumento, permitindo pular a primeira aplicação de f . Chame esse novo contêiner inicial de const . O lado direito da tabela acima mostra as expansões de n inc const . Então, substituindo init por const na expressão para a mesma função, obtemos a função predecessora,

${\ displaystyle \ operatorname {pred} = \ lambda n. \ lambda f. \ lambda x. \ operatorname {extrato} \ (n \ operatorname {inc} \ operatorname {const}) = \ lambda n. \ lambda f. \ lambda x. \ operatorname {extrato} \ (\ operatorname {valor} \ ((n-1) \ f \ x)) = \ lambda n. \ lambda f. \ lambda x. (n-1) \ f \ x = \ lambda n. (n-1)}$

Conforme explicado abaixo, as funções inc , init , const , value e extract podem ser definidas como,

${\ displaystyle {\ begin {alinhado} \ operatorname {value} & = \ lambda v. (\ lambda hh \ v) \\\ operatorname {extract} k & = k \ \ lambda uu \\\ operatorname {inc} & = \ lambda g. \ lambda hh \ (g \ f) \\\ operatorname {init} & = \ lambda hh \ x \\\ operatorname {const} & = \ lambda ux \ end {alinhado}}}$

O que dá a expressão lambda para pred as,

${\ displaystyle \ operatorname {pred} = \ lambda n. \ lambda f. \ lambda xn \ (\ lambda g. \ lambda hh \ (g \ f)) \ (\ lambda ux) \ (\ lambda uu)}$

Outra maneira de definir pred

Pred também pode ser definido usando pares:

${\ displaystyle {\ begin {alinhado} \ operatorname {f} = & \ \ lambda p. \ \ operatorname {par} \ (\ operatorname {segundo} \ p) \ (\ operatorname {succ} \ (\ operatorname {segundo } \ p)) \\\ operatorname {zero} = & \ (\ lambda f. \ lambda x. \ x) \\\ operatorname {pc0} = & \ \ operatorname {par} \ \ operatorname {zero} \ \ operatorname {zero} \\\ operatorname {pred} = & \ \ lambda n. \ \ operatorname {primeiro} \ (n \ \ operatorname {f} \ \ operatorname {pc0}) \\\ end {alinhado}}}$

Esta é uma definição mais simples, mas leva a uma expressão mais complexa para pred. A expansão para : ${\ displaystyle \ operatorname {pred} \ operatorname {três}}$

${\ displaystyle {\ begin {alinhado} \ operatorname {pred} \ operatorname {three} = & \ \ operatorname {first} \ (\ operatorname {f} \ (\ operatorname {f} \ (\ operatorname {f} \ ( \ operatorname {pair} \ \ operatorname {zero} \ \ operatorname {zero})))) \\ = & \ \ operatorname {first} \ (\ operatorname {f} \ (\ operatorname {f} \ (\ operatorname { pair} \ \ operatorname {zero} \ \ operatorname {one}))) \\ = & \ \ operatorname {first} \ (\ operatorname {f} \ (\ operatorname {pair} \ \ operatorname {one} \ \ operatorname {two})) \\ = & \ \ operatorname {first} \ (\ operatorname {pair} \ \ operatorname {two} \ \ operatorname {three}) \\ = & \ \ operatorname {two} \ end {alinhado} }}$

Divisão

A divisão de números naturais pode ser implementada por,

${\ displaystyle n / m = \ operatorname {if} \ n \ geq m \ \ operatorname {then} \ 1+ (nm) / m \ \ operatorname {else} \ 0}$

O cálculo requer muitas reduções beta. A menos que faça a redução manualmente, isso não importa muito, mas é preferível não ter que fazer esse cálculo duas vezes. O predicado mais simples para testar números é IsZero, portanto, considere a condição. ${\ displaystyle nm}$

${\ displaystyle \ operatorname {IsZero} \ (\ operatorname {menos} \ n \ m)}$

Mas essa condição é equivalente a , não . Se esta expressão for usada, então a definição matemática da divisão dada acima é traduzida em função em numerais de Igreja como, ${\ displaystyle n \ leq m}$${\ displaystyle n <m}$

${\ displaystyle \ operatorname {divide1} \ n \ m \ f \ x = (\ lambda d. \ operatorname {IsZero} \ d \ (0 \ f \ x) \ (f \ (\ operatorname {divide1} \ d \ m \ f \ x))) \ (\ operatorname {menos} \ n \ m)}$

Conforme desejado, essa definição tem uma única chamada para . No entanto, o resultado é que essa fórmula fornece o valor de . ${\ displaystyle \ operatorname {menos} \ n \ m}$${\ displaystyle (n-1) / m}$

Este problema pode ser corrigido adicionando 1 an antes de chamar divide . A definição de divisão é, então,

${\ displaystyle \ operatorname {divide} \ n = \ operatorname {divide1} \ (\ operatorname {succ} \ n)}$

divide1 é uma definição recursiva. O combinador Y pode ser usado para implementar a recursão. Crie uma nova função chamada div por;

• No lado esquerdo ${\ displaystyle \ operatorname {divide1} \ rightarrow \ operatorname {div} \ c}$
• No lado direito ${\ displaystyle \ operatorname {divide1} \ rightarrow c}$

para obter,

${\ displaystyle \ operatorname {div} = \ lambda c. \ lambda n. \ lambda m. \ lambda f. \ lambda x. (\ lambda d. \ operatorname {IsZero} \ d \ (0 \ f \ x) \ (f \ (c \ d \ m \ f \ x))) \ (\ operatorname {menos} \ n \ m)}$

Então,

${\ displaystyle \ operatorname {divide} = \ lambda n. \ operatorname {divide1} \ (\ operatorname {succ} \ n)}$

Onde,

${\ displaystyle {\ begin {alinhado} \ operatorname {divide1} & = Y \ \ operatorname {div} \\\ operatorname {succ} & = \ lambda n. \ lambda f. \ lambda xf \ (n \ f \ x ) \\ Y & = \ lambda f. (\ Lambda xf \ (x \ x)) \ (\ lambda xf \ (x \ x)) \\ 0 & = \ lambda f. \ Lambda xx \\\ operatorname {IsZero} & = \ lambda nn \ (\ lambda x. \ operatorname {false}) \ \ operatorname {verdadeiro} \ end {alinhado}}}$

${\ displaystyle {\ begin {alinhado} \ operatorname {true} & \ equiv \ lambda a. \ lambda ba \\\ operatorname {false} & \ equiv \ lambda a. \ lambda bb \ end {alinhado}}}$

${\ displaystyle {\ begin {alinhado} \ operatorname {menos} & = \ lambda m. \ lambda nn \ operatorname {pred} m \\\ operatorname {pred} & = \ lambda n. \ lambda f. \ lambda xn \ (\ lambda g. \ lambda hh \ (g \ f)) \ (\ lambda ux) \ (\ lambda uu) \ end {alinhado}}}$

Dá,

${\ displaystyle \ scriptstyle \ operatorname {divide} = \ lambda n. ((\ lambda f. (\ lambda xx \ x) \ (\ lambda xf \ (x \ x))) \ (\ lambda c. \ lambda n . \ lambda m. \ lambda f. \ lambda x. (\ lambda d. (\ lambda nn \ (\ lambda x. (\ lambda a. \ lambda bb)) \ ​​(\ lambda a. \ lambda ba)) \ d \ ((\ lambda f. \ lambda xx) \ f \ x) \ (f \ (c \ d \ m \ f \ x))) \ ((\ lambda m. \ lambda nn (\ lambda n. \ lambda f. \ lambda xn \ (\ lambda g. \ lambda hh \ (g \ f)) \ (\ lambda ux) \ (\ lambda uu)) m) \ n \ m))) \ ((\ lambda n . \ lambda f. \ lambda xf \ (n \ f \ x)) \ n)}$

Ou como texto, usando \ para λ ,

divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

Por exemplo, 9/3 é representado por

divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))

Usando uma calculadora de cálculo lambda, a expressão acima se reduz a 3, usando a ordem normal.

\f.\x.f (f (f (x)))

Números assinados

Uma abordagem simples para estender Números de Igreja a números com sinais é usar um par de Igreja, contendo numerais de Igreja que representam um valor positivo e um valor negativo. O valor inteiro é a diferença entre os dois números da Igreja.

Um número natural é convertido em um número assinado por,

${\ displaystyle \ operatorname {convert} _ {s} = \ lambda x. \ operatorname {par} \ x \ 0}$

A negação é realizada trocando os valores.

${\ displaystyle \ operatorname {neg} _ {s} = \ lambda x. \ operatorname {par} \ (\ operatorname {segundo} \ x) \ (\ operatorname {primeiro} \ x)}$

O valor inteiro é mais naturalmente representado se um do par for zero. A função OneZero atinge essa condição,

${\ displaystyle \ operatorname {OneZero} = \ lambda x. \ operatorname {IsZero} \ (\ operatorname {primeiro} \ x) \ x \ (\ operatorname {IsZero} \ (\ operatorname {segundo} \ x) \ x \ (\ operatorname {OneZero} \ \ operatorname {par} \ (\ operatorname {pred} \ (\ operatorname {primeiro} \ x)) \ (\ operatorname {pred} \ (\ operatorname {segundo} \ x)))) }$

A recursão pode ser implementada usando o combinador Y,

${\ displaystyle \ operatorname {OneZ} = \ lambda c. \ lambda x. \ operatorname {IsZero} \ (\ operatorname {first} \ x) \ x \ (\ operatorname {IsZero} \ (\ operatorname {second} \ x ) \ x \ (c \ \ operatorname {par} \ (\ operatorname {pred} \ (\ operatorname {primeiro} \ x)) \ (\ operatorname {pred} \ (\ operatorname {segundo} \ x)))) }$

${\ displaystyle \ operatorname {OneZero} = Y \ operatorname {OneZ}}$

Mais e menos

A adição é definida matematicamente no par por,

${\ displaystyle x + y = [x_ {p}, x_ {n}] + [y_ {p}, y_ {n}] = x_ {p} -x_ {n} + y_ {p} -y_ {n} = (x_ {p} + y_ {p}) - (x_ {n} + y_ {n}) = [x_ {p} + y_ {p}, x_ {n} + y_ {n}]}$

A última expressão é traduzida em cálculo lambda como,

${\ displaystyle \ operatorname {plus} _ {s} = \ lambda x. \ lambda y. \ operatorname {OneZero} \ (\ operatorname {pair} \ (\ operatorname {plus} \ (\ operatorname {first} \ x) \ (\ operatorname {primeiro} \ y)) \ (\ operatorname {mais} \ (\ operatorname {segundo} \ x) \ (\ operatorname {segundo} \ y)))}$

Da mesma forma a subtração é definida,

${\ displaystyle xy = [x_ {p}, x_ {n}] - [y_ {p}, y_ {n}] = x_ {p} -x_ {n} -y_ {p} + y_ {n} = ( x_ {p} + y_ {n}) - (x_ {n} + y_ {p}) = [x_ {p} + y_ {n}, x_ {n} + y_ {p}]}$

dando,

${\ displaystyle \ operatorname {menos} _ {s} = \ lambda x. \ lambda y. \ operatorname {OneZero} \ (\ operatorname {par} \ (\ operatorname {mais} \ (\ operatorname {primeiro} \ x) \ (\ operatorname {segundo} \ y)) \ (\ operatorname {mais} \ (\ operatorname {segundo} \ x) \ (\ operatorname {primeiro} \ y)))}$

Multiplique e divida

A multiplicação pode ser definida por,

${\ displaystyle x * y = [x_ {p}, x_ {n}] * [y_ {p}, y_ {n}] = (x_ {p} -x_ {n}) * (y_ {p} -y_ {n}) = (x_ {p} * y_ {p} + x_ {n} * y_ {n}) - (x_ {p} * y_ {n} + x_ {n} * y_ {p}) = [ x_ {p} * y_ {p} + x_ {n} * y_ {n}, x_ {p} * y_ {n} + x_ {n} * y_ {p}]}$

A última expressão é traduzida em cálculo lambda como,

${\ displaystyle \ operatorname {mult} _ {s} = \ lambda x. \ lambda y. \ operatorname {pair} \ (\ operatorname {plus} \ (\ operatorname {mult} \ (\ operatorname {primeiro} \ x) \ (\ operatorname {first} \ y)) \ (\ operatorname {mult} \ (\ operatorname {second} \ x) \ (\ operatorname {second} \ y))) \ (\ operatorname {plus} \ (\ operatorname {mult} \ (\ operatorname {primeiro} \ x) \ (\ operatorname {segundo} \ y)) \ (\ operatorname {mult} \ (\ operatorname {segundo} \ x) \ (\ operatorname {primeiro} \ y)))}$

Uma definição semelhante é dada aqui para divisão, exceto nesta definição, um valor em cada par deve ser zero (consulte OneZero acima). A função divZ nos permite ignorar o valor que tem um componente zero.

${\ displaystyle \ operatorname {divZ} = \ lambda x. \ lambda y. \ operatorname {IsZero} \ y \ 0 \ (\ operatorname {divide} \ x \ y)}$

divZ é então usado na seguinte fórmula, que é a mesma da multiplicação, mas com mult substituído por divZ .

${\ displaystyle \ operatorname {divide} _ {s} = \ lambda x. \ lambda y. \ operatorname {pair} \ (\ operatorname {plus} \ (\ operatorname {divZ} \ (\ operatorname {primeiro} \ x) \ (\ operatorname {first} \ y)) \ (\ operatorname {divZ} \ (\ operatorname {second} \ x) \ (\ operatorname {second} \ y))) \ (\ operatorname {plus} \ (\ operatorname {divZ} \ (\ operatorname {primeiro} \ x) \ (\ operatorname {segundo} \ y)) \ (\ operatorname {divZ} \ (\ operatorname {segundo} \ x) \ (\ operatorname {primeiro} \ y)))}$

Números racionais e reais

Os números reais racionais e computáveis ​​também podem ser codificados no cálculo lambda. Os números racionais podem ser codificados como um par de números com sinal. Os números reais computáveis ​​podem ser codificados por um processo de limitação que garante que a diferença do valor real difere em um número que pode ser tão pequeno quanto necessário. As referências fornecidas descrevem software que poderia, em teoria, ser traduzido em cálculo lambda. Uma vez que os números reais são definidos, os números complexos são codificados naturalmente como um par de números reais.

Os tipos de dados e funções descritos acima demonstram que qualquer tipo de dados ou cálculo pode ser codificado no cálculo lambda. Esta é a tese de Church-Turing .

Tradução com outras representações

A maioria das linguagens do mundo real tem suporte para inteiros nativos da máquina; as funções igreja e não igreja são convertidas entre inteiros não negativos e seus números de igreja correspondentes. As funções são fornecidas aqui em Haskell , onde o \corresponde ao λ do cálculo Lambda. As implementações em outras linguagens são semelhantes.

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 cn = cn (+ 1) 0

Igreja Booleana

Os booleanos da Igreja são a codificação da Igreja dos valores booleanos verdadeiro e falso. Algumas linguagens de programação usam isso como um modelo de implementação para aritmética booleana; exemplos são Smalltalk e Pico .

A lógica booleana pode ser considerada uma escolha. A codificação da Igreja de verdadeiro e falso são funções de dois parâmetros:

• true escolhe o primeiro parâmetro.
• false escolhe o segundo parâmetro.

As duas definições são conhecidas como Church Booleans:

${\ displaystyle {\ begin {alinhado} \ operatorname {true} & \ equiv \ lambda a. \ lambda ba \\\ operatorname {false} & \ equiv \ lambda a. \ lambda bb \ end {alinhado}}}$

Esta definição permite que predicados (ou seja, funções que retornam valores lógicos ) atuem diretamente como cláusulas if. Uma função que retorna um booleano, que é então aplicado a dois parâmetros, retorna o primeiro ou o segundo parâmetro:

${\ displaystyle \ operatorname {predicate-} x \ \ operatorname {then-clause} \ \ operatorname {else-clause}}$

avalia a cláusula then se o predicado-x for avaliado como verdadeiro , e a cláusula else se o predicado-x for avaliado como falso .

Como verdadeiro e falso escolhem o primeiro ou o segundo parâmetro, eles podem ser combinados para fornecer operadores lógicos. Observe que existem várias implementações possíveis de não .

${\ displaystyle {\ begin {alinhado} \ operatorname {e} & = \ lambda p. \ lambda qp \ q \ p \\\ operatorname {ou} & = \ lambda p. \ lambda qp \ p \ q \\\ operatorname {not} _ {1} & = \ lambda p. \ lambda a. \ lambda bp \ b \ a \\\ operatorname {not} _ {2} & = \ lambda pp \ (\ lambda a. \ lambda bb ) \ (\ lambda a. \ lambda ba) = \ lambda pp \ operatorname {false} \ operatorname {true} \\\ operatorname {xor} & = \ lambda a. \ lambda ba \ (\ operatorname {not} \ b ) \ b \\\ operatorname {if} & = \ lambda p. \ lambda a. \ lambda bp \ a \ b \ end {alinhado}}}$

Alguns exemplos:

${\ displaystyle {\ begin {alinhado} \ operatorname {e} \ operatorname {true} \ operatorname {false} & = (\ lambda p. \ lambda qp \ q \ p) \ \ operatorname {true} \ \ operatorname {false } = \ operatorname {true} \ operatorname {false} \ operatorname {true} = (\ lambda a. \ lambda ba) \ operatorname {false} \ operatorname {true} = \ operatorname {false} \\\ operatorname {ou} \ operatorname {true} \ operatorname {false} & = (\ lambda p. \ lambda qp \ p \ q) \ (\ lambda a. \ lambda ba) \ (\ lambda a. \ lambda bb) = (\ lambda a . \ lambda ba) \ (\ lambda a. \ lambda ba) \ (\ lambda a. \ lambda bb) = (\ lambda a. \ lambda ba) = \ operatorname {true} \\\ operatorname {not} _ { 1} \ \ operatorname {true} & = (\ lambda p. \ Lambda a. \ Lambda bp \ b \ a) (\ lambda a. \ Lambda ba) = \ lambda a. \ Lambda b. (\ Lambda a. \ lambda ba) \ b \ a = \ lambda a. \ lambda b. (\ lambda cb) \ a = \ lambda a. \ lambda bb = \ operatorname {false} \\\ operatorname {not} _ {2} \ \ operatorname {true} & = (\ lambda pp \ (\ lambda a. \ lambda bb) (\ lambda a. \ lambda ba)) (\ lambda a. \ lambda ba) = (\ lambda a. \ lambda ba) (\ lambda a. \ lambda bb) ( \ lambda a. \ lambda ba) = (\ lambda b. (\ lambda a. \ lambda bb)) \ ​​(\ lambda a. \ lambda ba) = \ lambda a. \ lambda bb = \ operatorname {false} \ end {alinhado}}}$

Predicados

Um predicado é uma função que retorna um valor booleano. O predicado mais fundamental é , que retorna se seu argumento for o numeral da Igreja e se seu argumento for qualquer outro numeral da Igreja: ${\ displaystyle \ operatorname {IsZero}}$${\ displaystyle \ operatorname {true}}$${\ displaystyle 0}$${\ displaystyle \ operatorname {false}}$

${\ displaystyle \ operatorname {IsZero} = \ lambda nn \ (\ lambda x. \ operatorname {false}) \ \ operatorname {true}}$

O seguinte predicado testa se o primeiro argumento é menor ou igual ao segundo:

${\ displaystyle \ operatorname {LEQ} = \ lambda m. \ lambda n. \ operatorname {IsZero} \ (\ operatorname {menos} \ m \ n)}$,

Por causa da identidade,

${\ displaystyle x = y \ equiv (x \ leq y \ land y \ leq x)}$

O teste de igualdade pode ser implementado como,

${\ displaystyle \ operatorname {EQ} = \ lambda m. \ lambda n. \ operatorname {e} \ (\ operatorname {LEQ} \ m \ n) \ (\ operatorname {LEQ} \ n \ m)}$

Pares de igreja

Os pares de igrejas são a codificação de igrejas do tipo par (duas tuplas). O par é representado como uma função que recebe um argumento de função. Quando receber seu argumento, ele o aplicará aos dois componentes do par. A definição em cálculo lambda é,

${\ displaystyle {\ begin {alinhado} \ operatorname {pair} & \ equiv \ lambda x. \ lambda y. \ lambda zz \ ​​x \ y \\\ operatorname {first} & \ equiv \ lambda pp \ (\ lambda x . \ lambda yx) \\\ operatorname {segundo} & \ equiv \ lambda pp \ (\ lambda x. \ lambda yy) \ end {alinhado}}}$

Por exemplo,

${\ displaystyle {\ begin {alinhado} & \ operatorname {first} \ (\ operatorname {pair} \ a \ b) \\ = & (\ lambda pp \ (\ lambda x. \ lambda yx)) \ ((\ lambda x. \ lambda y. \ lambda zz \ ​​x \ y) \ a \ b) \\ = & (\ lambda pp \ (\ lambda x. \ lambda yx)) \ (\ lambda zz \ ​​a \ b) \ \ = & (\ lambda zz \ ​​a \ b) \ (\ lambda x. \ lambda yx) \\ = & (\ lambda x. \ lambda yx) \ a \ b = a \ end {alinhado}}}$

Codificações de lista

Uma lista ( imutável ) é construída a partir de nós de lista. As operações básicas da lista são;

Fornecemos quatro representações diferentes de listas abaixo:

• Construa cada nó da lista a partir de dois pares (para permitir listas vazias).
• Construa cada nó da lista a partir de um par.
• Represente a lista usando a função de dobra à direita .
• Representa a lista usando a codificação de Scott que recebe casos de expressão de correspondência como argumentos

Dois pares como um nó de lista

Uma lista não vazia pode ser implementada por um par de Church;

• Primeiro contém a cabeça.
• Em segundo lugar, contém a cauda.

No entanto, isso não dá uma representação da lista vazia, porque não há um ponteiro "nulo". Para representar nulo, o par pode ser agrupado em outro par, fornecendo valores livres,

• Primeiro - é o ponteiro nulo (lista vazia).
• Second.First contém a cabeça.
• Second.Second contém a cauda.

Usando essa ideia, as operações básicas da lista podem ser definidas assim:

Expressão	Descrição
${\ displaystyle \ operatorname {nil} \ equiv \ operatorname {par} \ \ operatorname {true} \ \ operatorname {true}}$	O primeiro elemento do par é verdadeiro, o que significa que a lista é nula.
${\ displaystyle \ operatorname {isnil} \ equiv \ operatorname {primeiro}}$	Recupere o indicador nulo (ou lista vazia).
${\ displaystyle \ operatorname {cons} \ equiv \ lambda h. \ lambda t. \ operatorname {par} \ operatorname {falso} \ (\ operatorname {par} h \ t)}$	Crie um nó de lista, que não seja nulo, e atribua a ele um cabeçalho h e um tail t .
${\ displaystyle \ operatorname {head} \ equiv \ lambda z. \ operatorname {primeiro} \ (\ operatorname {segundo} z)}$	em segundo lugar, o primeiro é a cabeça.
${\ displaystyle \ operatorname {cauda} \ equiv \ lambda z. \ operatorname {segundo} \ (\ operatorname {segundo} z)}$	o segundo.segundo é a cauda.

Em um nulo nó segundo nunca é acessado, desde que a cabeça e cauda são aplicadas apenas a listas não vazios.

Um par como um nó de lista

Alternativamente, defina

${\ displaystyle {\ begin {alinhado} \ operatorname {cons} & \ equiv \ operatorname {pair} \\\ operatorname {head} & \ equiv \ operatorname {first} \\\ operatorname {tail} & \ equiv \ operatorname { segundo} \\\ operatorname {nil} & \ equiv \ operatorname {false} \\\ operatorname {isnil} & \ equiv \ lambda ll (\ lambda h. \ lambda t. \ lambda d. \ operatorname {false}) \ operatorname {verdadeiro} \ end {alinhado}}}$

onde a última definição é um caso especial do geral

${\ displaystyle \ operatorname {lista de processos} \ equiv \ lambda ll (\ lambda h. \ lambda t. \ lambda d. \ operatorname {head-and-tail-clause}) \ operatorname {nil-clause}}$

Represente a lista usando a dobra direita

Como alternativa à codificação usando pares de Church, uma lista pode ser codificada identificando-a com sua função de dobra à 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 a um combinador ce um valor n retorna cx (cy (czn)).

${\ displaystyle {\ begin {alinhado} \ operatorname {nil} & \ equiv \ lambda c. \ lambda nn \\\ operatorname {isnil} & \ equiv \ lambda ll \ (\ lambda h. \ lambda t. \ operatorname { false}) \ \ operatorname {true} \\\ operatorname {cons} & \ equiv \ lambda h. \ lambda t. \ lambda c. \ lambda nc \ h \ (t \ c \ n) \\\ operatorname {head } & \ equiv \ lambda ll \ (\ lambda h. \ lambda th) \ \ operatorname {false} \\\ operatorname {cauda} & \ equiv \ lambda l. \ lambda c. \ lambda nl \ (\ lambda h. \ lambda t. \ lambda gg \ h \ (t \ c)) \ (\ lambda tn) \ (\ lambda h. \ lambda tt) \ end {alinhado}}}$

Esta representação lista pode ser determinado tipo no Sistema F .

Represente a lista usando a codificação Scott

Uma representação alternativa é a codificação Scott, que usa a ideia de continuações e pode levar a um código mais simples. (veja também a codificação Mogensen – Scott ).

Nesta abordagem, usamos o fato de que as listas podem ser observadas usando a expressão de correspondência de padrões. Por exemplo, usando a notação Scala , se listdenota um valor do tipo Listcom lista Nile construtor vazios Cons(h, t), podemos inspecionar a lista e calcular nilCodecaso a lista esteja vazia e consCode(h, t)quando a lista não estiver vazia:

list match {
  case Nil        => nilCode
  case Cons(h, t) => consCode(h,t)
}

A 'lista' é dada pela forma como atua sobre 'nilCode' e 'consCode'. Portanto, definimos uma lista como uma função que aceita 'nilCode' e 'consCode' como argumentos, de modo que, em vez da correspondência de padrão acima, possamos simplesmente escrever:

${\ displaystyle \ operatorname {lista} \ \ operatorname {nilCode} \ (\ operatorname {consCode} \ h \ t)}$

Vamos denotar por 'n' o parâmetro correspondente a 'nilCode' e por 'c' o parâmetro correspondente a 'consCode'. A lista vazia é aquela que retorna o argumento nulo:

${\ displaystyle \ operatorname {nil} \ equiv \ lambda n. \ lambda c. \ n}$

A lista não vazia com cabeça 'h' e cauda 't' é dada por

${\ displaystyle \ operatorname {cons} \ h \ t \ \ \ equiv \ \ \ lambda n. \ lambda c. \ c \ h \ t}$

Mais geralmente, um tipo de dados algébrico com alternativas torna-se uma função com parâmetros. Quando o enésimo construtor tem argumentos, o parâmetro correspondente da codificação também aceita argumentos. ${\ displaystyle m}$${\ displaystyle m}$${\ displaystyle i}$${\ displaystyle n_ {i}}$${\ displaystyle n_ {i}}$

A codificação de Scott pode ser feita em cálculo lambda sem tipo, enquanto seu uso com tipos requer um sistema de tipos com recursão e polimorfismo de tipo. Uma lista com o tipo de elemento E nesta representação que é usada para calcular valores do tipo C teria a seguinte definição de tipo recursiva, onde '=>' denota o tipo de função:

type List = 
  C =>                    // nil argument
  (E => List => C) =>     // cons argument
  C                       // result of pattern matching

Uma lista que pode ser usada para calcular tipos arbitrários teria um tipo que é quantificado C. Uma lista genérica em Etambém tomaria Ecomo argumento de tipo.

Veja também

• Cálculo lambda
• Sistema F para numerais de igreja em um cálculo digitado
• Codificação Mogensen-Scott
• Definição de Von Neumann de ordinais - outra maneira de codificar números naturais: como conjuntos

Notas

Referências

• Metaprogramação Diretamente Reflexiva
• Números de igreja e booleanos explicados por Robert Cartwright na Rice University
• Fundamentos Teóricos para 'Programação Totalmente Funcional' Prática (Capítulos 2 e 5) Tudo sobre a Igreja e outras codificações semelhantes, incluindo como derivá-las e operações nelas, a partir dos primeiros princípios
• Alguns exemplos interativos de numerais de igrejas
• Lambda Calculus Live Tutorial: Boolean Algebra