Codificación de la iglesia

Representación de los números naturales como funciones de orden superior

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

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

La codificación de Church no pretende ser una implementación práctica de tipos de datos primitivos. Su uso es para mostrar que no se requieren otros tipos de datos primitivos para representar ningún cálculo. La integridad es representativa. Se necesitan funciones adicionales para traducir la representación en 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 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 se suele interpretar en el sentido de que utiliza 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.

Números de la iglesia

Los números de la Iglesia son las representaciones de números naturales bajo 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 n- veces . En términos más simples, el "valor" del numeral es equivalente al número de veces que la función encapsula su argumento.${\displaystyle f}$

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

Todos los números de la Iglesia son funciones que toman dos parámetros. Los números de iglesia 0 , 1 , 2 , ..., se definen como sigue en el cálculo lambda .

Comenzando con 0 no aplicación de la función en absoluto, proceder 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 número 3 de la Iglesia representa la acción de aplicar una función dada tres veces a un valor. La función proporcionada se aplica primero a un parámetro proporcionado y luego sucesivamente a su propio resultado. El resultado final no es el número 3 (a menos que el parámetro proporcionado sea 0 y la función sea una función sucesora ). La función en sí, y no su resultado final, es el número 3 de la Iglesia . El número 3 de la Iglesia significa simplemente hacer cualquier cosa tres veces. Es una demostración ostensiva de lo que se entiende por "tres tiempos".

Cálculo con números de la Iglesia

Las operaciones aritméticas sobre números pueden representarse mediante funciones sobre numerales de la Iglesia. Estas funciones pueden definirse en cálculo lambda o implementarse en la mayoría de los lenguajes de programación funcionales (consulte conversión de expresiones lambda en funciones ).

La función de suma usa 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 usa 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 es dada por la definición de los números de la Iglesia, . En la definición, sustitúyase por 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 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 el predecesor para obtener una explicación más detallada.

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

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

Tabla de funciones en los números de la Iglesia

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)}$	...
Adición	${\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}$[1]	${\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 *	${\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 x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}$
Resta *	${\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}$

* Tenga en cuenta que en la codificación de la Iglesia,

• ${\displaystyle \operatorname {pred} (0)=0}$
• ${\displaystyle m<n\to m-n=0}$

Derivación de la función predecesora

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}}}$.

Para construir el predecesor, necesitamos una forma de aplicar la función 1 vez menos. Un numeral n aplica la función f n veces ax . 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 de contenedor. Definiremos nuevas funciones para usar en lugar de f y x , llamadas inc e init . La función de contenedor se llama valor . El lado izquierdo de la tabla muestra un número 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 (llamado extracto ),

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

Luego, extraer puede usarse 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 arreglar que en la primera aplicación inc reciba un contenedor especial que ignore su argumento permitiendo omitir la primera aplicación de f . Llame 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 de 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)}$

Contenedor de valor El contenedor de valor aplica una función a su valor. Está definido por, ${\displaystyle \operatorname {value} \ v\ h=h\ v}$ asi que, ${\displaystyle \operatorname {value} =\lambda v.(\lambda h.h\ v)}$ Inc La función inc debe tomar un valor que contenga v y devolver un nuevo valor que contenga fv . ${\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}$ Dejando que g sea el contenedor de valor, ${\displaystyle g=\operatorname {value} \ v}$ entonces, ${\displaystyle g\ f=\operatorname {value} \ v\ f=f\ v}$ asi que, ${\displaystyle \operatorname {inc} \ g=\operatorname {value} \ (g\ f)}$ ${\displaystyle \operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)}$

Extraer El valor se puede extraer aplicando la función de identidad, ${\displaystyle I=\lambda u.u}$ Usando yo , ${\displaystyle \operatorname {value} \ v\ I=v}$ asi que, ${\displaystyle \operatorname {extract} \ k=k\ I}$ Const Para implementar pred, la función init se reemplaza con la constante que no aplica f . Necesitamos constante para satisfacer ${\displaystyle \operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x}$ ${\displaystyle \lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x}$ Que se satisface si, ${\displaystyle \operatorname {const} \ f=x}$ O como expresión lambda, ${\displaystyle \operatorname {const} =\lambda u.x}$

Otra forma de definir pred

Pred también se puede definir usando 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}}}$

División

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

${\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 haga la reducción a mano, esto no importa mucho, 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 . Si se usa esta expresión, la definición matemática de división dada anteriormente se traduce en función en los números de la Iglesia 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 desee, 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 puede corregirse sumando 1 an antes de llamar a dividir . La definición de dividir es entonces,

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

dividir1 es una definición recursiva. El combinador Y se puede utilizar para implementar la recursividad. Cree una nueva función llamada div por;

• 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 (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)))

Números firmados

Un método simple para extender los números de la iglesia a números con signo es usar un par de iglesias que contenga números de la iglesia que representen un valor positivo y uno negativo. ^[3] El valor entero es la diferencia entre los dos números 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 logra 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 recursividad se puede implementar usando 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} }$

Más y menos

La suma 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)))}$

Multiplica y divide

La multiplicación se puede definir 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 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)}$

divZ se usa 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)))}$

Números racionales y reales

Los números reales racionales y computables también se pueden codificar en el cálculo lambda. Los números racionales se pueden codificar 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 del valor real difiera en un número que puede ser tan pequeño como necesitemos. ^{[4] [5]} Las referencias dadas 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 las funciones descritas anteriormente demuestran que cualquier tipo de datos o cálculo puede codificarse en el cálculo lambda. Ésta es la tesis de Church-Turing .

Traducción con otras representaciones

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

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

Iglesia booleana

Church Booleanos 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; 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:

• true elige el primer parámetro.
• false elige el segundo parámetro.

Las dos definiciones se conocen como Church Booleanos:

${\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, funciones que devuelven valores lógicos ) actúen directamente como cláusulas if. Una función que devuelve un 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-entonces 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 verdadero y falso eligen el primer o segundo parámetro, se pueden combinar para proporcionar operadores lógicos. Tenga en cuenta que hay dos versiones de no , dependiendo de la estrategia de evaluación que se elija.

${\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\ {\scriptstyle {\text{(This is only a correct implementation if the evaluation strategy is applicative order.)}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ {\scriptstyle {\text{(This is only a correct implementation if the evaluation strategy is normal order.)}}}\\\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}}}$

Predicados

Un predicado es una función que devuelve un valor booleano. El predicado más fundamental es , que devuelve si su argumento es el número de la Iglesia , y si su argumento es cualquier otro número de la Iglesia:${\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 se puede implementar como,

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

Pares de iglesias

Ver también: Contras

Los pares de iglesias son la codificación de la iglesia del tipo de pares (dos tuplas). El par se representa como una función que toma un argumento de función. Cuando se le dé su argumento, lo aplicará a los dos componentes del par. La definición en el 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}}}$

Enumerar codificaciones

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

Función	Descripción
nulo	Construye una lista vacía.
isnil	Prueba si la lista está vacía.
contras	Anteponer un valor dado a una lista (posiblemente vacía).
cabeza	Obtenga el primer elemento de la lista.
cola	Obtenga el resto de la lista.

A continuación, ofrecemos cuatro representaciones diferentes de listas:

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

Dos pares como un nodo de lista

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 "nulo". Para representar nulo, el par se puede envolver en otro par, dando valores libres,

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

Usando esta idea, las operaciones básicas de la lista se pueden definir así: ^[6]

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)}$	Cree un nodo de lista, que no sea nulo, y asígnele una cabeza hy una cola t .
${\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}$	segundo, el 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 el encabezado y el final solo se apliquen a listas no vacías.

Un par como nodo de lista

Alternativamente, defina ^[7]

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

Represente la lista usando el pliegue derecho

Como alternativa a la codificación mediante pares de iglesias, se puede codificar una lista identificándola con su función de plegado derecho . 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 cy 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}}}$

Esta representación de la lista se puede dar el tipo de sistema F .

Representar la lista con la codificación Scott

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

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

lista de  coincidencias  {  case  Nil  =>  nilCode  case  Cons ( h ,  t )  =>  consCode ( h , t ) }

La 'lista' viene dada por cómo actúa sobre 'nilCode' y 'consCode'. Por lo tanto, definimos una lista como una función que acepta tales 'nilCode' y 'consCode' como argumentos, de modo que en lugar de la coincidencia de patrón anterior simplemente podemos escribir:

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

Denotemos por 'n' el parámetro correspondiente a 'nilCode' y por 'c' el 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 la cabeza 'h' y la cola 't' viene dada por

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

De manera más general, 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 toma argumentos.${\displaystyle m}$${\displaystyle m}$${\displaystyle i}$${\displaystyle n_{i}}$${\displaystyle n_{i}}$

La codificación de Scott se puede realizar en cálculo lambda sin tipo, mientras que su uso con tipos requiere un sistema de tipos con recursividad 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 recursivo, donde '=>' denota el tipo de función:

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

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

Ver también

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

Notas

1. Esta fórmula es la definición de un número de Iglesia n con f -> m, x -> f.
2. Allison, Lloyd. "Enteros de cálculo Lambda" .
3. Bauer, Andrej. "Respuesta de Andrej a una pregunta;" Representación de números negativos y complejos mediante cálculo lambda " " .
4. "Aritmética real exacta" . Haskell .
5. Bauer, Andrej. "Software computacional de números reales" .
6. Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . Prensa del MIT . pag. 500. ISBN 978-0-262-16209-8.
7. Tromp, John (2007). "14. Cálculo lambda binario y lógica combinatoria". En Calude, Cristian S (ed.). Aleatoriedad y complejidad, de Leibniz a Chaitin . World Scientific. págs. 237-262. ISBN 978-981-4474-39-9.
   Como PDF: Tromp, John (14 de mayo de 2014). "Cálculo lambda binario y lógica combinatoria" (PDF) . Consultado el 24 de noviembre de 2017 .
8. Jansen, Jan Martin (2013). "Programación en el λ-cálculo: de la iglesia a Scott y viceversa". LNCS . 8106 : 168–180. doi : 10.1007 / 978-3-642-40355-2_12 .

Referencias

• Metaprogramación directamente reflexiva
• Números de iglesia y booleanos explicados por Robert Cartwright en Rice University
• Fundamentos teóricos para la práctica 'Programación totalmente funcional' (Capítulos 2 y 5) Todo sobre Church y otras codificaciones similares, incluyendo cómo derivarlas y operaciones en ellas, desde los primeros principios
• Algunos ejemplos interactivos de numerales de la Iglesia
• Tutorial de Lambda Calculus Live: Álgebra booleana