Codificación de la iglesia

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

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.

Usar

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. ${\displaystyle O(1)}$ ${\displaystyle O(n)}$ ${\displaystyle 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.

Números de la iglesia

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

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

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".

Cálculo con numerales de la Iglesia

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

Tabla de funciones de los numerales de la Iglesia

Notas :

1. Esta fórmula es la definición de un numeral de la Iglesia n con . ${\displaystyle f\to m,x\to f}$
2. En la codificación de la Iglesia,
   • ${\displaystyle \operatorname {pred} (0)=0}$
   • ${\displaystyle m\leq 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}}}$.

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

Otra forma de definir pred

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

División

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

Números con signo

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

Más y menos

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

Multiplicar y dividir

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

Números racionales y reales

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 .

Traducción con otras representaciones

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           

Booleanos de la iglesia

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

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

Pares de iglesias

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

Codificaciones de listas

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

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 "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]

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

Un par como nodo de lista

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

Representar la lista utilizandopliegue derecho

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.

Representar la lista utilizando la codificación Scott

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 una lista vacía Nily un constructor, Cons(h, t)podemos inspeccionar la lista y calcular nilCodesi la lista está vacía y consCode(h, t)si 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 .

Véase también

• 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

Referencias

1. Trancón y Widemann, Baltasar; Parnas, David Lorge (2008). "Expresiones tabulares y programación funcional total". En Olaf Chitil; Zoltán Horváth; Viktória Zsók (eds.). Implementación y aplicación de lenguajes funcionales. 19.° taller internacional, IFL 2007, Friburgo, Alemania, 27-29 de septiembre de 2007. Documentos revisados ​​seleccionados. Lecture Notes in Computer Science. Vol. 5083. págs. 228-229. doi :10.1007/978-3-540-85373-2_13. ISBN 978-3-540-85372-5.
2. Jansen, Jan Martin; Koopman, Pieter WM; Plasmeijer, Marinus J. (2006). "Interpretación eficiente mediante la transformación de tipos de datos y patrones en funciones". En Nilsson, Henrik (ed.). Tendencias en programación funcional. Volumen 7. Bristol: Intellect. págs. 73–90. CiteSeerX 10.1.1.73.9841 . ISBN.  978-1-84150-188-8.
3. "Los predecesores y las listas no son representables en el cálculo lambda de tipos simples". Cálculo lambda y calculadoras lambda . okmij.org.
4. Allison, Lloyd. "Cálculo Lambda: números enteros".
5. Bauer, Andrej. "Respuesta de Andrej a una pregunta; "Representación de números negativos y complejos mediante cálculo lambda"".
6. "Aritmética real exacta". Haskell . Archivado desde el original el 26 de marzo de 2015.
7. Bauer, Andrej (26 de septiembre de 2022). «Software computacional de números reales». GitHub .
8. Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . MIT Press . pág. 500. ISBN. 978-0-262-16209-8.
9. 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 .
10. Jansen, Jan Martin (2013). "Programación en el cálculo λ: de Church a Scott y de regreso". En Achten, Peter; Koopman, Pieter WM (eds.). La belleza del código funcional: ensayos dedicados a Rinus Plasmeijer con motivo de su 61.º cumpleaños . Apuntes de clase en informática. Vol. 8106. Springer. págs. 168–180. doi :10.1007/978-3-642-40355-2_12.

• 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