Codificación de la iglesia

La introducción de este artículo puede ser demasiado breve para resumir adecuadamente los puntos clave . Considere ampliar la introducción para brindar una descripción general accesible de todos los aspectos importantes del artículo. ( Julio de 2023 )

En matemáticas , la codificación Church es un medio para representar datos y operadores en el cálculo lambda . Los numerales Church son una representación de los números naturales mediante la notación lambda. El método recibe su nombre de Alonzo Church , quien fue el primero en codificar datos en el cálculo lambda de esta manera.

Los términos que normalmente se consideran primitivos en otras notaciones (como números enteros, booleanos, pares, listas y uniones etiquetadas) se asignan a funciones de orden superior bajo la codificación Church. La tesis de Church-Turing afirma que cualquier operador computable (y sus operandos) se puede representar bajo la codificación Church. ^{[ dudoso – discutir ]} En el cálculo lambda no tipificado, el único tipo de datos primitivo es la función.

Una implementación sencilla de la codificación Church ralentiza algunas operaciones de acceso de a , donde es el tamaño de la estructura de datos, lo que hace que la codificación Church sea poco práctica. ^[1] La investigación ha demostrado que esto se puede abordar mediante optimizaciones específicas, pero la mayoría de los lenguajes de programación funcional , en cambio, expanden sus representaciones intermedias para contener tipos de datos algebraicos . ^[2] No obstante, la codificación Church se utiliza a menudo en argumentos teóricos, ya que es una representación natural para la evaluación parcial y la demostración de teoremas. ^[1] Las operaciones se pueden tipificar utilizando tipos de rango superior , ^[3] y la recursión primitiva es fácilmente accesible. ^[1] La suposición de que las funciones son los únicos tipos de datos primitivos agiliza muchas pruebas.${\estilo de visualización O(1)}$${\displaystyle O(n)}$${\estilo de visualización n}$

La codificación de Church está completa, pero solo representativamente. Se necesitan funciones adicionales para traducir la representación a tipos de datos comunes, para mostrarlos a las personas. En general, no es posible decidir si dos funciones son extensionalmente iguales debido a la indecidibilidad de la equivalencia del teorema de Church . La traducción puede aplicar la función de alguna manera para recuperar el valor que representa, o buscar su valor como un término lambda literal. El cálculo lambda generalmente se interpreta como el uso de la igualdad intensional . Existen problemas potenciales con la interpretación de los resultados debido a la diferencia entre la definición intensional y extensional de igualdad.

Los numerales de la Iglesia son las representaciones de los números naturales según la codificación de la Iglesia. La función de orden superior que representa el número natural n es una función que asigna cualquier función a su composición de n veces . En términos más simples, el "valor" del numeral es equivalente a la cantidad de veces que la función encapsula su argumento.${\estilo de visualización f}$

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

Todos los numerales de Church son funciones que toman dos parámetros. Los numerales de Church 0 , 1 , 2 , ..., se definen de la siguiente manera en el cálculo lambda .

Comenzando con 0 sin aplicar la función en absoluto, proceda con 1 aplicando la función una vez, 2 aplicando la función dos veces, 3 aplicando la función tres veces, etc .:

${\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}$

El numeral 3 de la Iglesia representa la acción de aplicar cualquier función dada tres veces a un valor. La función suministrada se aplica primero a un parámetro suministrado y luego sucesivamente a su propio resultado. El resultado final no es el numeral 3 (a menos que el parámetro suministrado sea 0 y la función sea una función sucesora ). La función en sí misma, y ​​no su resultado final, es el numeral 3 de la Iglesia . El numeral 3 de la Iglesia significa simplemente hacer algo tres veces. Es una demostración ostensible de lo que significa "tres veces".

Las operaciones aritméticas con números se pueden representar mediante funciones en numerales de Church. Estas funciones se pueden definir en el cálculo lambda o implementar en la mayoría de los lenguajes de programación funcional (consulte conversión de expresiones lambda a funciones ).

La función de suma utiliza la identidad .${\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 x.m\ f\ (n\ f\ x)}$

La función sucesora es β-equivalente a .${\displaystyle \operatorname {succ} (n)=n+1}$${\displaystyle (\operatorname {plus} \ 1)}$

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

La función de multiplicación utiliza la identidad .${\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 x.m\ (n\ f)\ x}$

La función exponencial viene dada por la definición de numerales de Church, . En la definición, sustituya para obtener y,${\displaystyle \operatorname {exp} (m,n)=m^{n}}$${\displaystyle n\ h\ x=h^{n}\ x}$${\displaystyle h\to m,x\to f}$${\displaystyle n\ m\ f=m^{n}\ f}$

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

que da la expresión lambda,

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

La función es más difícil de entender.${\displaystyle \operatorname {pred} (n)}$

${\displaystyle \operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$

Un numeral de Church aplica una función n veces. La función predecesora debe devolver una función que aplique su parámetro n - 1 veces. Esto se logra construyendo un contenedor alrededor de f y x , que se inicializa de una manera que omite la aplicación de la función la primera vez. Consulte predecesor para obtener una explicación más detallada.

La función resta se puede escribir basándose en la función predecesora.

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

Función	Álgebra	Identidad	Definición de función	Expresiones lambda
Sucesor	${\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 x.f\ (n\ f\ x)}$	...
Suma	${\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 x.m\ f\ (n\ f\ x)}$	${\displaystyle \lambda m.\lambda n.n\operatorname {succ} m}$
Multiplicación	${\displaystyle m*n}$	${\displaystyle f^{m*n}\ x=(f^{m})^{n}\ x}$	${\displaystyle \operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x}$	${\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}$	${\displaystyle \lambda m.\lambda n.\lambda f.m\ (n\ f)}$
Exponenciación	${\displaystyle m^{n}}$	${\displaystyle n\ m\ f=m^{n}\ f}$[a]	${\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 n.n\ m}$
Predecesor [b]	${\displaystyle n-1}$	${\displaystyle \operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)}$	${\displaystyle \operatorname {if} (n==0)\ 0\ \operatorname {else} \ (n-1)}$	${\displaystyle \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$
Resta [b] ( Monus )	${\displaystyle m-n}$	${\displaystyle f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)}$	${\displaystyle \operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m}$	...	${\displaystyle \lambda m.\lambda n.n\operatorname {pred} m}$

Notas :

La función predecesora utilizada en la codificación de la Iglesia es,

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

Necesitamos una forma de aplicar la función 1 veces menos para construir la predecesora. Un numeral n aplica la función f n veces a x . La función predecesora debe usar el numeral n para aplicar la función n -1 veces.

Antes de implementar la función predecesora, aquí hay un esquema que envuelve el valor en una función contenedora. Definiremos nuevas funciones para usar en lugar de f y x , llamadas inc e init . La función contenedora se llama value . El lado izquierdo de la tabla muestra un numeral n aplicado a inc e init .

${\displaystyle {\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (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 {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}}$

La regla general de recurrencia es:

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

Si también hay una función para recuperar el valor del contenedor (llamada extract ),

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

Luego, el extracto se puede utilizar para definir la función samenum como,

${\displaystyle \operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n}$

La función samenum no es intrínsecamente útil. Sin embargo, como inc delega la llamada de f a su argumento contenedor, podemos disponer que en la primera aplicación inc reciba un contenedor especial que ignore su argumento, lo que permite omitir la primera aplicación de f . Llamemos a este nuevo contenedor inicial const . El lado derecho de la tabla anterior muestra las expansiones de n inc const . Luego, al reemplazar init con const en la expresión para la misma función, obtenemos la función predecesora,

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

Como se explica a continuación, las funciones inc , init , const , value y extract pueden definirse como:

${\displaystyle {\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}}$

Lo que da la expresión lambda para pred como,

${\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$

Pred también puede definirse utilizando pares:

${\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}}$

Esta es una definición más simple pero conduce a una expresión más compleja para pred. La expansión para :${\displaystyle \operatorname {pred} \operatorname {three} }$

${\displaystyle {\begin{aligned}\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{aligned}}}$

La división de números naturales se puede implementar mediante ^[4]

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

El cálculo requiere muchas reducciones beta. A menos que se haga la reducción a mano, esto no importa tanto, pero es preferible no tener que hacer este cálculo dos veces. El predicado más simple para probar números es IsZero , así que considere la condición.${\displaystyle n-m}$

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

Pero esta condición es equivalente a , no a . Si se utiliza esta expresión, entonces la definición matemática de división dada anteriormente se traduce en función de los números de Church 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 {minus} \ n\ m)}$

Como se deseaba, esta definición tiene una única llamada a . Sin embargo, el resultado es que esta fórmula da el valor de .${\displaystyle \operatorname {minus} \ n\ m}$${\displaystyle (n-1)/m}$

Este problema se puede corregir sumando 1 a n antes de llamar a divide . La definición de divide es entonces:

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

divide1 es una definición recursiva. El combinador Y se puede utilizar para implementar la recursión. Crea una nueva función llamada div mediante:

• En el lado izquierdo${\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}$
• En el lado derecho${\displaystyle \operatorname {divide1} \rightarrow c}$

Llegar,

${\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 {minus} \ n\ m)}$

Entonces,

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

dónde,

${\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}$

${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}$

${\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}$

Da,

${\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}$

O como texto, usando \ para λ ,

dividir = (\n.((\f.(\xx x) (\xf (xx))) (\c.\n.\m.\f.\x.(\d.(\nn (\x .(\a.\bb)) (\a.\ba)) d ((\f.\xx) fx) (f (cdmfx))) ((\m.\nn (\n.\f.\ xn (\g.\hh (gf)) (\ux) (\uu)) m) nm))) ((\n.\f.\x. f (nfx)) n))

Por ejemplo, 9/3 está representado por

dividir (\f.\xf (f (f (f (f (f (f (f (f (f (f (f (f (fx))))))))) (\f.\xf (f (fx)))

Usando una calculadora de cálculo lambda, la expresión anterior se reduce a 3, usando el orden normal.

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

Un enfoque simple para extender los numerales de la Iglesia a números con signo es utilizar un par de numerales de la Iglesia, que contiene numerales de la Iglesia que representan un valor positivo y uno negativo. ^[5] El valor entero es la diferencia entre los dos numerales de la Iglesia.

Un número natural se convierte en un número con signo mediante,

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

La negación se realiza intercambiando los valores.

${\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}$

El valor entero se representa de forma más natural si uno de los pares es cero. La función OneZero cumple esta condición.

${\displaystyle \operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))}$

La recursión se puede implementar utilizando el combinador Y,

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

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

La adición se define matemáticamente en el 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}]}$

La última expresión se traduce al cálculo lambda como,

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

De manera similar se define la resta,

${\displaystyle x-y=[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}]}$

donación,

${\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}$

La multiplicación puede definirse 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}]}$

La última expresión se traduce al cálculo lambda como,

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

Aquí se da una definición similar para la división, excepto que en esta definición, un valor en cada par debe ser cero (ver OneZero arriba). La función divZ nos permite ignorar el valor que tiene un componente cero.

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

Luego, divZ se utiliza en la siguiente fórmula, que es la misma que para la multiplicación, pero con mult reemplazado por divZ .

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

Los números reales racionales y computables también pueden codificarse en el cálculo lambda. Los números racionales pueden codificarse como un par de números con signo. Los números reales computables pueden codificarse mediante un proceso de limitación que garantiza que la diferencia con el valor real difiere en un número que puede hacerse tan pequeño como sea necesario. ^{[6] [7]} Las referencias proporcionadas describen software que, en teoría, podría traducirse al cálculo lambda. Una vez que se definen los números reales, los números complejos se codifican naturalmente como un par de números reales.

Los tipos de datos y funciones descritos anteriormente demuestran que cualquier tipo de datos o cálculo puede codificarse en el cálculo lambda. Esta es la tesis de Church-Turing .

La mayoría de los lenguajes del mundo real admiten números enteros nativos de máquina; las funciones church y unchurch convierten entre números enteros no negativos y sus numerales Church correspondientes. Las funciones se dan aquí en Haskell , donde \corresponde a λ del cálculo Lambda. Las implementaciones en otros lenguajes son similares.

tipo Iglesia a = ( a -> a ) -> a -> a          iglesia :: Entero -> Iglesia Entero iglesia 0 = \ f -> \ x -> x iglesia n = \ f -> \ x -> f ( iglesia ( n - 1 ) f x )                       unchurch :: Iglesia Entero -> Entero unchurch cn = cn ( + 1 ) 0           

Los booleanos de Church son la codificación de Church de los valores booleanos verdadero y falso. Algunos lenguajes de programación los utilizan como modelo de implementación para la aritmética booleana; algunos ejemplos son Smalltalk y Pico .

La lógica booleana puede considerarse una opción. La codificación de la Iglesia de verdadero y falso son funciones de dos parámetros:

• verdadero elige el primer parámetro.
• falso elige el segundo parámetro.

Las dos definiciones se conocen como Booleanos de la Iglesia:

${\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}$

Esta definición permite que los predicados (es decir, las funciones que devuelven valores lógicos ) actúen directamente como cláusulas if. Una función que devuelve un valor booleano, que luego se aplica a dos parámetros, devuelve el primero o el segundo parámetro:

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

se evalúa como cláusula-then si el predicado-x se evalúa como verdadero , y como cláusula-else si el predicado-x se evalúa como falso .

Dado que true y false eligen el primer o segundo parámetro, se pueden combinar para proporcionar operadores lógicos. Tenga en cuenta que existen múltiples implementaciones posibles de not .

${\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}$

Algunos ejemplos:

${\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}}$

Un predicado es una función que devuelve un valor booleano. El predicado más fundamental es , que devuelve si su argumento es el numeral de Church y si su argumento es cualquier otro numeral de Church:${\displaystyle \operatorname {IsZero} }$${\displaystyle \operatorname {true} }$${\displaystyle 0}$${\displaystyle \operatorname {false} }$

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

El siguiente predicado prueba si el primer argumento es menor o igual que el segundo:

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

Por la identidad,

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

La prueba de igualdad puede implementarse como,

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

Los pares de Church son la codificación de Church del tipo de par (dos tuplas). El par se representa como una función que toma un argumento de función. Cuando se le da su argumento, aplicará el argumento a los dos componentes del par. La definición en cálculo lambda es:

${\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda x.\lambda y.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda x.\lambda y.y)\end{aligned}}}$

Por ejemplo,

${\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)\\=&(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)\\=&(\lambda x.\lambda y.x)\ a\ b=a\end{aligned}}}$

Una lista ( inmutable ) se construye a partir de nodos de lista. Las operaciones básicas en la lista son:

A continuación presentamos cuatro representaciones diferentes de listas:

• Construya cada nodo de lista a partir de dos pares (para permitir listas vacías).
• Construye cada nodo de lista a partir de un par.
• Representar la lista utilizando la función de plegado a la derecha .
• Representar la lista utilizando la codificación de Scott que toma casos de expresión coincidente como argumentos

Una lista no vacía puede ser implementada por un par de Iglesias;

• Primero contiene la cabeza.
• El segundo contiene la cola.

Sin embargo, esto no da una representación de la lista vacía, porque no hay un puntero "null". Para representar el valor nulo, el par puede estar envuelto en otro par, lo que da tres valores:

• Primero , el puntero nulo (lista vacía).
• Segundo.Primero contiene la cabeza.
• Segundo.Segundo contiene la cola.

Utilizando esta idea las operaciones básicas de lista se pueden definir así: ^[8]

Expresión	Descripción
${\displaystyle \operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true} }$	El primer elemento del par es verdadero, lo que significa que la lista es nula.
${\displaystyle \operatorname {isnil} \equiv \operatorname {first} }$	Recupere el indicador nulo (o lista vacía).
${\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)}$	Crea un nodo de lista que no sea nulo y asígnale una cabeza h y una cola t .
${\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}$	segundo.primero es la cabeza.
${\displaystyle \operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)}$	segundo.segundo es la cola.

En un nodo nulo nunca se accede al segundo , siempre que la cabeza y la cola solo se apliquen a listas no vacías.

Alternativamente, defina ^[9]

${\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {first} \\\operatorname {tail} &\equiv \operatorname {second} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {false} )\operatorname {true} \end{aligned}}}$

donde la última definición es un caso especial de la general

${\displaystyle \operatorname {process-list} \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nil-clause} }$

Como alternativa a la codificación mediante pares de Church, una lista se puede codificar identificándola con su función de plegado a la derecha . Por ejemplo, una lista de tres elementos x, y y z se puede codificar mediante una función de orden superior que, cuando se aplica a un combinador c y un valor n, devuelve cx (cy (czn)).

${\displaystyle {\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda t.\operatorname {false} )\ \operatorname {true} \\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda t.h)\ \operatorname {false} \\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda t.\lambda g.g\ h\ (t\ c))\ (\lambda t.n)\ (\lambda h.\lambda t.t)\end{aligned}}}$

A esta representación de lista se le puede dar el tipo en el Sistema F.

Una representación alternativa es la codificación Scott, que utiliza la idea de continuaciones y puede conducir a un código más simple. ^[10] (véase también codificación Mogensen-Scott ).

En este enfoque, utilizamos el hecho de que las listas se pueden observar mediante expresiones de coincidencia de patrones. Por ejemplo, utilizando la notación Scala , si listdenota un valor de tipo Listcon lista vacía Nily constructor, Cons(h, t)podemos inspeccionar la lista y calcular nilCodeen caso de que la lista esté vacía y consCode(h, t)cuando no lo esté:

lista coincidente { caso Nil => nilCode caso Cons ( h , t ) => consCode ( h , t ) }           

La función listse determina por su acción sobre nilCodey consCode. Por lo tanto, definimos una lista como una función que acepta tales nilCodey consCodecomo argumentos, de modo que en lugar de la coincidencia de patrones anterior, podemos simplemente escribir:

${\displaystyle \operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode} }$

Denotemos por nel parámetro correspondiente a nilCodey por cel parámetro correspondiente a consCode. La lista vacía es la que devuelve el argumento nulo:

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

La lista no vacía con cabeza hy cola tviene dada por

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

En términos más generales, un tipo de datos algebraicos con alternativas se convierte en una función con parámetros. Cuando el constructor tiene argumentos, el parámetro correspondiente de la codificación también recibe argumentos.${\displaystyle m}$${\displaystyle m}$${\displaystyle i}$${\displaystyle n_{i}}$${\displaystyle n_{i}}$

La codificación Scott se puede realizar en el cálculo lambda sin tipo, mientras que su uso con tipos requiere un sistema de tipos con recursión y polimorfismo de tipos. Una lista con el tipo de elemento E en esta representación que se utiliza para calcular valores de tipo C tendría la siguiente definición de tipo recursiva, donde '=>' denota el tipo de función:

tipo Lista = C => // argumento nulo ( E => Lista => C ) => // argumento cons C // resultado de la coincidencia de patrones               

Una lista que se puede utilizar para calcular tipos arbitrarios tendría un tipo que cuantifica sobre C. Una lista genérica ^{[ aclaración necesaria ]} en Etambién tomaría Ecomo argumento de tipo .

• Cálculo lambda
• Sistema F para numerales de la Iglesia en un cálculo tipificado
• Codificación Mogensen-Scott
• Definición de ordinales de Von Neumann : otra forma de codificar los números naturales: como conjuntos

• Stump, A. (2009). "Metaprogramación directamente reflexiva" (PDF) . High-Order Symb Comput . 22 (2): 115–144. CiteSeerX  10.1.1.489.5018 . doi :10.1007/s10990-007-9022-0. S2CID  16124152.
• Cartwright, Robert. "Explicación de los números y los valores booleanos de la Iglesia" (PDF) . Comp 311 — Revisión 2. Universidad Rice .
• Kemp, Colin (2007). "§2.4.1 Church Naturals, §2.4.2 Church Booleans, Cap. 5 Técnicas de derivación para TFP". Fundamentos teóricos para la "programación totalmente funcional" práctica(PhD). Facultad de Tecnología de la Información e Ingeniería Eléctrica, Universidad de Queensland. págs. 14–17, 93–145. CiteSeerX  10.1.1.149.3505 . Todo sobre Church y otras codificaciones similares, incluyendo cómo derivarlas y operaciones con ellas, desde los primeros principios.
• Algunos ejemplos interactivos de numerales de la Iglesia
• Tutorial en vivo de cálculo lambda: álgebra booleana