Codificación de la iglesia

En matemáticas , la codificación de Church significa la representación (o procedimiento de representación) de datos y operadores en un procedimiento de cálculo lambda. La necesidad del procedimiento se debe a que en el cálculo lambda puro entre los términos solo hay variables y no hay constantes. Para obtener objetos que se comporten de la misma forma que los números, se aplica la codificación Church. El procedimiento en sí lleva el nombre de Alonzo Church , quien desarrolló el cálculo lambda y fue pionero en este método de codificación de datos. Al igual que los números, la codificación de Church también se puede utilizar para representar otros tipos de objetos que se comportan como constantes.

Los términos que suelen ser primitivos en otras notaciones (como números enteros, booleanos, pares, listas y uniones etiquetadas) se representan en el código de Church mediante funciones de orden superior . En una de sus formulaciones, la tesis de Turing-Church establece que cualquier operador computable (y sus operandos) pueden ser representados en la codificación de Church. En el cálculo lambda sin tipo, las funciones son el único tipo de datos primitivo y todas las demás entidades se construyen utilizando la codificación Church.

La codificación de iglesia generalmente no se usa para la implementación práctica de tipos de datos primitivos. Se utiliza con el propósito de demostrar de manera concluyente que no se requieren otros tipos de datos primitivos para realizar cálculos.

Números de iglesia

Los números de la Iglesia son representaciones de números naturales en la codificación de la Iglesia. Una función de orden superior , que representa un número natural n, es una función que asigna cualquier función a su composición de n veces . En pocas palabras, el "valor" de un número es equivalente al número de veces que la función encapsula su argumento. $F$

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

Todos los números de la Iglesia son funciones con dos parámetros. Los números de Iglesia '0' , '1' , '2' , …, se definen en el cálculo lambda de la siguiente manera:

${\ estilo de visualización 0 \ f \ x}$ significa "no aplicar la función en absoluto", significa "aplicar la función 1 vez", etc.: $F$ $X$ ${\ estilo de visualización 1 \ f \ x}$

Número	Definición numérica	expresión lambda
0	${\ estilo de visualización 0 \ f \ x = x}$	$0=\lambda f.\lambda xx$
una	${\ estilo de visualización 1 \ f \ x = f \ x}$	$1=\lambda f.\lambda xf\x$
2	${\ estilo de visualización 2 \ f \ x = f \ (f \ x)}$	$2=\lambda f.\lambda xf\ (f\ x)$
3	${\ estilo de visualización 3 \ f \ x = f \ (f \ (f \ x))}$	$3=\lambda f.\lambda xf\ (f\ (f\ x))$
⋮	⋮	⋮
$norte$	${\ estilo de visualización n \ f \ x = f ^ {n} \ x}$	$n=\lambda f.\lambda xf^{\circ n}\ x$

El número 3 de Church representa el proceso de aplicar cualquier función f utilizada tres veces. Esta función se aplica secuencialmente primero al parámetro que se le pasa y luego al resultado obtenido como resultado de su aplicación anterior.

Cálculos con números de Iglesia

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

Codificación de booleanos

Los booleanos de iglesia son el resultado de la codificación de iglesia aplicada a la representación de los valores booleanos verdaderos y falsos. Algunos lenguajes de programación los utilizan como modelo de implementación para la aritmética booleana. Ejemplos de este tipo de lenguajes son Smalltalk y Pico .

La lógica booleana puede verse como una opción. La codificación de iglesia para booleanos es una función de dos parámetros:

true selecciona el primer parámetro.
false selecciona la segunda opción.

Estas dos definiciones se conocen como booleanos de la iglesia:

{\begin{alineado}\operatorname {verdadero} &\equiv \lambda a.\lambda ba\\\operatorname {falso} &\equiv \lambda a.\lambda bb\end{alineado))

Esta definición permite que los predicados (es decir, las funciones que devuelven un valor booleano ) funcionen directamente como si fueran condiciones:

Una función que devuelve un valor booleano, que luego se aplica a dos parámetros, devuelve el primer o el segundo parámetro:

\operatorname {predicado} \ x\ \operatorname {entonces-cláusula} \ \operatorname {otra-cláusula}

se resuelve como una cláusula entonces si x se evalúa como verdadero, y como una cláusula si x se evalúa como falso.

Dado que verdadero y falso corresponden a la elección del primer o segundo parámetro de esta función, este formalismo se puede utilizar para implementar operadores lógicos estándar. Tenga en cuenta que hay dos versiones de la implementación del operador not, según la estrategia de resolución de expresión elegida .

{\begin{alineado}\operatorname {y} &=\lambda p.\lambda qp\ q\ p\\\operatorname {o} &=\lambda p.\lambda qp\ p\ q\\\ operatorname {not} _{1}&=\lambda p.\lambda a.\lambda bp\ b\ a\ {\scriptstyle {\text{(Esta es la versión de implementación correcta para el orden de evaluación aplicativa.)))}\ \ \operatorname {no} _{2}&=\lambda pp\ (\lambda a.\lambda bb)\ (\lambda a.\lambda ba)=\lambda pp\operatorname {falso} \operatorname {verdadero} \ { \scriptstyle {\text{(Esta es la versión de implementación correcta para el orden normal de evaluación.)}}}\\\operatorname {xor} &=\lambda a.\lambda ba\ (\operatorname {not} \ b )\ b\ \\operatorname {si} &=\lambda p.\lambda a.\lambda bp\ a\ b\end{alineado}}

Algunos ejemplos:

{\begin{alineado}\operatorname {y} \operatorname {verdadero} \operatorname {falso} &=(\lambda p.\lambda qp\ q\ p)\ \operatorname {verdadero} \ \operatorname {falso } =\operatorname {verdadero} \operatorname {falso} \operatorname {verdadero} =(\lambda a.\lambda ba)\operatorname {falso} \operatorname {verdadero} =\operatorname {falso} \\\operatorname {o} \operatorname {verdadero} \operatorname {falso} &=(\lambda p.\lambda qp\ p\ q)\ (\lambda a.\lambda ba)\ (\lambda a.\lambda bb)=(\lambda a .\lambda ba)\ (\lambda a.\lambda ba)\ (\lambda a.\lambda bb)=(\lambda a.\lambda ba)=\operatorname {verdadero} \\\operatorname {no}_{ 1}\ \operatorname {verdadero} &=(\lambda p.\lambda a.\lambda bp\ b\ a)(\lambda a.\lambda ba)=\lambda a.\lambda b.(\lambda a. \lambda ba)\ b\ a=\lambda a.\lambda b.(\lambda cb)\ a=\lambda a.\lambda bb=\operatorname {falso} \\\operatorname {no} _{2}\ \operatorname {verdadero} &=(\lambda pp\ (\lambda a.\lambda bb)(\lambda a.\lambda ba))(\lambda a.\lambda ba)=(\lambda a.\lambda ba) (\lambda a.\lambda bb)(  \lambda a.\lambda ba)=(\lambda b.(\lambda a.\lambda bb))\ (\lambda a.\lambda ba)=\lambda a.\lambda bb=\operatorname {falso} \end {alineado}}

Predicados

Los predicados son funciones que devuelven un valor booleano.

El predicado más fundamental es , que devuelve (verdadero) si su argumento es un número de Iglesia y (falso) si su argumento es cualquier otro número de Iglesia: $\operatorname {EsCero}$ ${\ estilo de visualización \ nombre del operador {verdadero}}$ ${\ estilo de visualización 0}$ ${\ estilo de visualización \ nombre del operador {falso}}$

\operatorname {IsZero} =\lambda nn\ (\lambda x.\operatorname {falso} )\ \operatorname {verdadero}

Este predicado comprueba si su primer argumento es menor o igual que su segundo:

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

En relación con la identidad

x=y\equiv (x\leq y\land y\leq x)

La verificación de igualdad se puede implementar de la siguiente manera:

\operatorname {EQ} =\lambda m.\lambda n.\operatorname {y} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)

Parejas de la iglesia

Ver también: contras

Los pares de iglesias son una representación codificada por la iglesia de un tipo de par, es decir, una tupla de dos valores. Un par se representa como una función que toma otra función como argumento. El resultado de esta función es aplicar el argumento a los dos componentes del par. Definición en cálculo lambda :

{\begin{alineado}\operatorname {par} &\equiv \lambda x.\lambda y.\lambda zz\ x\ y\\\operatorname {primero} &\equiv \lambda pp\ (\lambda x .\lambda yx)\\\operatorname {segundo} &\equiv \lambda pp\ (\lambda x.\lambda yy)\end{alineado}}

Ejemplo:

{\begin{alineado}&\operatorname {primero} \ (\operatorname {par} \ a\ b)\\=&(\lambda pp\ (\lambda x.\lambda yx))\ ((\ lambda x.\lambda y.\lambda zz\ x\ y)\ a\ b)\\=&(\lambda pp\ (\lambda x.\lambda yx))\ (\lambda zz\ a\ b)\ \=&(\lambda zz\ a\ b)\ (\lambda x.\lambda yx)\\=&(\lambda x.\lambda yx)\ a\ b=a\end{alineado}}

Codificaciones de lista

La lista ( inmutable ) consta de nodos. Las siguientes son las operaciones básicas para las listas:

Función	Descripción
nulo	Devuelve una lista vacía.
isil	Comprueba si la lista está vacía.
contras	Agrega el valor dado al comienzo de una lista (posiblemente vacía).
cabeza	Devuelve el primer elemento de la lista.
cola	Devuelve la lista completa excepto el primer elemento.

A continuación se muestran cuatro vistas de lista diferentes:

A través de la creación de cada nodo de la lista de dos pares.
A través de la creación de cada nodo de la lista a partir de un par.
Representación de una lista a través de una función de pliegue asociativa por la derecha .
Representación de listas utilizando la codificación Scott.

Representación como dos pares

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

First contiene el primer elemento de la lista.
El segundo contiene los elementos restantes (la 'cola' de la lista).

Sin embargo, no es posible expresar una lista vacía de esta manera, porque no tenemos una representación del valor vacío (nulo) definido. Para representarlo y poder codificar listas vacías, un par puede estar envuelto en otro par.

Primero es nulo (una lista vacía).
Second.First contiene el primer elemento de la lista.
Second.Second contiene la cola de la lista.

Usando esta idea, las operaciones de lista básicas se pueden expresar de la siguiente manera: [1]

expresión	Descripción
$\operatorname {nil} \equiv \operatorname {par} \ \operatorname {verdadero} \ \operatorname {verdadero}$	El primer elemento del par es verdadero , lo que significa que la lista está vacía.
$\operatorname {esnil} \equiv \operatorname {primero}$	Comprobando si la lista está vacía.
$\operatorname {contras} \equiv \lambda h.\lambda t.\operatorname {par} \operatorname {falso} \ (\operatorname {par} h\ t)$	cree un nodo de lista no vacío y pásele el primer elemento (el encabezado de la lista) h y la cola t .
$\operatorname {cabeza} \equiv \lambda z.\operatorname {primero} \ (\operatorname {segundo} z)$	segundo.primero es el encabezado de la lista.
$\operatorname {cola} \equiv \lambda z.\operatorname {segundo} \ (\operatorname {segundo} z)$	segundo.segundo es la cola de la lista.

En una lista vacía, el acceso al segundo elemento ( Second ) nunca se utiliza, en la medida en que los conceptos de cabeza y cola de una lista se aplican solo a listas no vacías.

Representación como un solo par

Alternativamente, las listas se pueden definir de la siguiente manera: [2]

{\begin{alineado}\operatorname {contras} &\equiv \operatorname {par} \\\operatorname {cabeza} &\equiv \operatorname {primero} \\\operatorname {cola} &\equiv \operatorname { segundo} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda ll(\lambda h.\lambda t.\lambda d.\operatorname {false} )\ nombre del operador {verdadero} \end{alineado}}

donde la última definición es un caso especial de una función más general:

\operatorname {lista de procesos} \equiv \lambda ll(\lambda h.\lambda t.\lambda d.\operatorname {cláusula de cabeza y cola} )\operatorname {cláusula nula}

Representación de una lista a través de una función de pliegue asociativa por la derecha

Como alternativa a la codificación mediante pares de iglesias, se puede codificar una lista identificándola con una función de pliegue asociativo derecho. Por ejemplo, una lista de tres elementos x, y y z se puede codificar con una función de orden superior que, cuando se aplica al combinador c y el valor n, devuelve cx(cy(czn)).

{\begin{alineado}\operatorname {nil} &\equiv \lambda c.\lambda nn\\\operatorname {isnil} &\equiv \lambda ll\ (\lambda h.\lambda t.\operatorname { false} )\ \operatorname {true} \\\operatorname {contras} &\equiv \lambda h.\lambda t.\lambda c.\lambda nc\ h\ (t\ c\ n)\\\operatorname {cabeza } &\equiv \lambda ll\ (\lambda h.\lambda th)\ \operatorname {falso} \\\operatorname {cola} &\equiv \lambda l.\lambda c.\lambda nl\ (\lambda h. \lambda t.\lambda gg\ h\ (t\ c))\ (\lambda tn)\ (\lambda h.\lambda tt)\end{alineado}}

Representación de listas utilizando la codificación Scott

Otra representación alternativa es la representación codificada de listas de Scott, que utiliza la idea de continuación y puede conducir a la simplificación del código [3] . (ver también codificación Mogensen-Scott ). En este enfoque, utilizamos el hecho de que las listas se pueden procesar mediante la coincidencia de patrones .

Literatura

Metaprogramación directamente reflexiva
Explicación de los números de iglesia y booleanos . Universidad Robert
Fundamentos teóricos para la 'programación totalmente funcional' práctica (capítulos 2 y 5). Todo sobre la codificación de la Iglesia y otros métodos de codificación similares.
Algunos ejemplos interactivos de números de la Iglesia
Lambda Calculus Live Tutorial: Álgebra booleana

Véase también

cálculo lambda
Sistema F con respecto al uso e implementación de números de iglesia en él para cálculos escritos
Codificación Mogensen-Scott
La definición de números ordinales según von Neumann es otra forma de representar los números naturales. En este caso, se definen en términos de conjuntos.

Notas

↑ Pierce, Benjamín C. Tipos y lenguajes de programación . - MIT Press , 2002. - Pág. 500. - ISBN 978-0-262-16209-8 .
↑ Trompo, John. 14. Cálculo Lambda Binario y Lógica Combinatoria // Aleatoriedad y Complejidad, De Leibniz a Chaitin (Inglés) / Calude, Cristian S.. - World Scientific , 2007. - P. 237-262. — ISBN 978-981-4474-39-9 .
Como PDF: Tromp, John Binary Lambda Calculus and Combinatory Logic (PDF) (14 de mayo de 2014). Consultado el 24 de noviembre de 2017. Archivado desde el original el 1 de junio de 2018. (indefinido)
↑ Jansen, Jan Martín. Programación en el λ-Calculus: de Church a Scott y viceversa // LNCS : diario. - 2013. - Vol. 8106 . - pág. 168-180 . -doi : 10.1007 / 978-3-642-40355-2_12 .