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 números de Church son una representación de los números naturales utilizando notación lambda. El método lleva el 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) puede representarse mediante la codificación de Church. ^{[ dudoso ]} En el cálculo lambda sin tipo, 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 desde hasta , donde está el tamaño de la estructura de datos, lo que hace que la codificación Church no sea práctica. ^[1] Las investigaciones han demostrado que esto se puede abordar mediante optimizaciones específicas, pero la mayoría de los lenguajes de programación funcionales expanden sus representaciones intermedias para contener tipos de datos algebraicos . ^[2] No obstante, la codificación de 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 escribir utilizando tipos de clasificación superior , ^[3] y la recursividad primitiva es fácilmente accesible. ^[1] La suposición de que las funciones son los únicos tipos de datos primitivos simplifica muchas pruebas. ${\displaystyle O(1)}$ ${\displaystyle O(n)}$ ${\displaystyle n}$

La codificación de la iglesia es completa pero sólo representativa. 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 extensivamente 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 igualdad intensional . Existen problemas potenciales con la interpretación de los resultados debido a la diferencia entre la definición intencional 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 equivale 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 Church son funciones que toman dos parámetros. Los números de iglesia 0 , 1 , 2 , ..., se definen de la siguiente manera en el cálculo lambda .

Comenzando con 0 sin aplicar la función en absoluto, continúe 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 cualquier 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 eclesiástico 3 . 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 iglesia.

Las operaciones aritméticas con números pueden representarse mediante funciones con números de Iglesia. Estas funciones pueden definirse en cálculo lambda o implementarse en la mayoría de los lenguajes de programación funcionales (consulte convertir 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 de exponenciación viene dada por la definición de números 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 número de la Iglesia 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 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 en función de la función predecesora.

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

Tabla de funciones en números de la iglesia.

 Nota:

1. Esta fórmula es la definición de un número 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}}}$.

Para construir el predecesor necesitamos una forma de aplicar la función 1 menos veces. Un numeral n aplica la función f n veces a x . La función predecesora debe usar el número 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 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 (llamada extraer ),

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

Luego, se puede utilizar extracto 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, reemplazando 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 se pueden definir 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 as,

${\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 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, ^[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 hagamos 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 equivale a , no . Si se usa esta expresión, entonces la definición matemática de división dada anteriormente se traduce en función de 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 se puede corregir sumando 1 an antes de llamar a divide . La definición de división 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 recursividad. Crea una nueva función llamada div by;

• 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 sencillo para extender los números de la Iglesia a números con signo es utilizar un par de la Iglesia, que contenga números de la Iglesia que representen un valor positivo y uno negativo. ^[5] 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 del par 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)))}$

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 componente cero.

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

Luego, 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 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 limitante que garantiza que la diferencia con el valor real difiere en un número que puede hacerse tan pequeño como necesitemos. ^{[6] [7]} Las referencias proporcionadas describen software que, en teoría, podría traducirse al cálculo lambda. Una vez definidos 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 se puede codificar en 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 church y unchurch convierten entre números enteros no negativos y sus correspondientes números Church. Las funciones se dan aquí en Haskell , donde \corresponde a λ del cálculo Lambda. Las implementaciones en otros idiomas son similares.

escriba 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 la Iglesia son la codificación de la Iglesia 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 es función de dos parámetros:

• true elige el primer parámetro.
• false 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, 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 en la cláusula entonces si el predicado-x se evalúa como verdadero y en la cláusula más si el predicado-x se evalúa como falso .

Debido a que verdadero y falso eligen el primer o segundo parámetro, pueden combinarse 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 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 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 iglesias son la codificación de iglesias del tipo par (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}}}$

Codificaciones de lista

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

A continuación damos 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.
• Representa la lista usando la función de plegado a la derecha .
• Representar la lista usando la codificación de Scott que toma casos de expresión coincidente como argumentos.

Dos pares como nodo de lista

Un par de Iglesias puede implementar una lista no vacía;

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

Sin embargo, esto no proporciona una representación de la lista vacía, porque no hay ningún puntero "nulo". Para representar nulo, el par puede estar envuelto en otro par, dando tres valores:

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

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

En un nodo nulo, nunca se accede al segundo , siempre que el principio y el final 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 del 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 usando el pliegue derecho.

Como alternativa a la codificación que utiliza 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 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 tipo en el Sistema F.

Representar la lista usando 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] (ver 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, 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 ) }           

El listviene dado por cómo actúa sobre nilCodey consCode. Por lo tanto, definimos una lista como una función que acepta tales nilCodey consCodecomo argumentos, de modo que en lugar del patrón 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}$

De manera más general, un tipo de datos algebraico con alternativas se convierte en una función con parámetros. Cuando el ésimo 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 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 elemento de tipo 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 sobre C. Una lista genérica ^{[ aclaración necesaria ]} también Etomaría Ecomo argumento de tipo.

Ver también

• cálculo lambda
• Sistema F para números de Iglesia en un cálculo mecanografiado
• Codificación Mogensen-Scott
• Definición de ordinales de von Neumann : otra forma de codificar 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. XIX Taller Internacional, IFL 2007, Friburgo, Alemania, 27 al 29 de septiembre de 2007 Artículos seleccionados revisados. Apuntes de conferencias sobre informática. vol. 5083, págs. 228-229. doi :10.1007/978-3-540-85373-2_13. ISBN 978-3-540-85372-5.
2. Jansen, Jan Martín; Koopman, Pieter WM; Plasmeijer, Marinus J. (2006). "Interpretación eficiente transformando tipos y patrones de datos en funciones". En Nilsson, Henrik (ed.). Tendencias en programación funcional. Volumen 7 . Bristol: intelecto. págs. 73–90. CiteSeerX 10.1.1.73.9841 . ISBN  978-1-84150-188-8.
3. "El predecesor y las listas no se pueden representar en un cálculo lambda simplemente escrito". Cálculo Lambda y Calculadoras Lambda . okmij.org.
4. Allison, Lloyd. "Cálculo Lambda de 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". Haskel . 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, Benjamín C. (2002). Tipos y Lenguajes de Programación . Prensa del MIT . pag. 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 . Científico mundial. 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 Martín (2013). "Programación en λ-Cálculo: de Church a Scott y viceversa". 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 conferencias sobre informática. vol. 8106. Saltador. págs. 168–180. doi :10.1007/978-3-642-40355-2_12.

• Tocón, A. (2009). "Metaprogramación directamente reflexiva" (PDF) . Computación simbólica de alto orden . 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 eclesiásticos y los valores booleanos" (PDF) . Comp 311 - Revisión 2 . Universidad de Rice .
• Kemp, Colin (2007). "§2.4.1 Church Naturals, §2.4.2 Church Booleanos, Capítulo 5 Técnicas de derivación para TFP". Fundamentos teóricos para una 'programación totalmente funcional' práctica(Doctor). Escuela 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 la Iglesia y otras codificaciones similares, incluido cómo derivarlas y sus operaciones, desde los primeros principios.
• Algunos ejemplos interactivos de números de la Iglesia.
• Tutorial en vivo de cálculo Lambda: álgebra booleana