Introducción al cálculo Lambda (2): codificación de iglesias

En el artículo anterior, hemos construido las bases del cálculo lambda. Lo que necesitamos saber a continuación es cómo construir algunas herramientas generales para los cálculos sobre esta base, como números naturales, valores booleanos. y operaciones básicas. y operaciones booleanas, etc.

Antes de introducir los números de Church, es necesario explicar las características esenciales de los números naturales definiendo los axiomas de Peano de los números naturales:

El sistema de axiomas de Peano consta de cinco elementos basados ​​en los conjunto de números naturales. La composición del axioma de N y la función sucesora S:

Los axiomas de Peano estipulan que el conjunto de números naturales es el conjunto formado a partir de 0 hasta la función sucesora S (Nota: Los axiomas originales de Peano). estipula que los números naturales comienzan desde 1), donde el inyectivo S(n) corresponde a n+1 en nuestra vida diaria, S(0) es 1, S(S(0)) es 2, y así sucesivamente.

Además, es obvio que el sistema de axiomas de Peano describe las propiedades esenciales de los números naturales y tiene poco que ver con la forma de expresión. La expresión en números arábigos es {0,1,2,.. .}, Expresado en caracteres chinos es {〇,一,二,...}, expresado en inglés es {cero, uno, dos,...}, expresado según los axiomas de Peano es {0,S( 0),S(S (0)),...} , expresado en cálculo lambda como números de iglesia.

Según los axiomas de Peano, podemos saber que siempre que se determinen el número natural 0 y la función posterior S, todos los números naturales se pueden obtener según los axiomas. Dado que solo hay funciones en el cálculo lambda, el número natural 0 también debe representarse mediante una función. Esta función tiene las propiedades del número natural 0 y se expresa como:

Y la función posterior S en lambda. El cálculo se expresa como:

Entonces estos números de Iglesia se expresan como:

Una verificación simple de la función posterior S y los números de Iglesia es la siguiente:

Siguiente podemos aprender algunas operaciones relacionadas en el cálculo lambda. Durante este proceso, necesitamos entendernos con los números de Church y referirnos a los principios, procesos y resultados de las operaciones con números naturales, para que podamos resolver mejor preguntas como "¿Por qué es esto?" operación expresada de esta manera?"

Ya sabemos que el número de Church n ≡ λf.λx.f n x significa aplicar f a x n veces. Luego, de acuerdo con las propiedades de la suma, para calcular la suma del número de Church my n, podemos usar el. función Aplicada m veces a n (m f n -> m f (n f x)), es decir,

De hecho, la función sucesora S se utiliza como el mapeo de +1 en el cálculo lambda, que es MÁS 1 después de la reducción:

Entonces piénselo desde otro ángulo, MÁS m n en realidad puede entenderse como aplicar S a n m veces, es decir,

Intente verificarlo ~

Continuar Lo siguiente que vamos a introducir es la multiplicación de Church. A través de las propiedades de la multiplicación de números naturales, podemos hacer una analogía. El resultado de la multiplicación de dos números de Church myn debe representar tal número de Church p ≡ λf.λx.f p x. : aplique f a p en x = m * n veces.

Obviamente, para calcular tal resultado p, puedes

¿Es también muy simple? De esta manera, hemos reinventado la multiplicación de Iglesias:

Entonces se puede obtener su expresión lambda:

Tenga en cuenta que estas son dos expresiones equivalentes de multiplicación de Iglesias, se pueden convertir a cada una. otros mediante reducción de eta.