Introducción al cálculo Lambda (1): definición y reducción

Esta serie de artículos es un resumen y una revisión de mi estudio del cálculo lambda, centrándose en "por qué" y "cómo". Espero que sea útil para quienes lo vean comprender este sistema formal. Porque he leído muchos wikis, tutoriales e introducciones antes, y la mayoría de ellos no los supe hasta que los leí, y no sé por qué. No sé por qué no explican por qué hacen esto, por qué están ahí estas cosas, cómo surgieron, pero ese hecho me molesta, de ahí esta serie. Intenté explicar y ordenar mi comprensión superficial, pero todavía sé un poco al respecto. Si hay algún error u omisión, no dude en señalarlo. Agradecemos el intercambio de opiniones, críticas y sugerencias.

Cita parcial:

Wikipedia (un proyecto de colaboración de enciclopedia multilingüe basado en tecnología wiki, es también una enciclopedia en línea escrita en diferentes idiomas. Sus metas y objetivos son Una enciclopedia gratuita para toda la humanidad)ˌUna enciclopedia abierta

Enciclopedia de Filosofía de Stanford

Curso de recitación de Cornell inteligente

Tutorial con traducción: [Traducción][ Original]

Introducción completa sobre cómo

Para describir un sistema formal, primero debemos acordar la notación básica. Para el cálculo lambda presentado en esta serie, su conjunto de símbolos incluye lambda. () y nombres de variables (x, y, z, etc.).

Solo hay tres expresiones legales (también llamadas términos: λ-λ-expresiones o λ-términos) en el cálculo lambda:

En este momento, algunas personas pueden preguntarse, el significado de (λ x x) y es muy claro, pero ¿por qué λy.xy representa la abstracción de funciones en lugar de aplicar la función λy.x a la aplicación de funciones de Y? ? Para eliminar la ambigüedad de expresiones similares, puede utilizar paréntesis con más frecuencia. Puede consultar la siguiente convención de desambiguación:

Como se mencionó anteriormente, en la abstracción de funciones, los parámetros formales están vinculados al cuerpo de la función. es decir, los parámetros formales son variables vinculadas y, en consecuencia, la naturaleza de las variables independientes es variable libre. Entendamos esta relación a través de algunos ejemplos:

Dado que cada función lambda tiene solo un parámetro, también tiene solo una variable vinculada, que cambia a medida que cambia el parámetro formal.

Usamos FV para representar el conjunto de todas las variables libres en una expresión lambda, por ejemplo:

A veces nuestra función requiere múltiples parámetros, lo cual es normal, pero si la función lambda solo ¿Puede haber un parámetro? La solución a este problema es la adulación.

La formación es un método para manejar la entrada de múltiples parámetros. Ya sabemos que la entrada y salida de la función lambda también pueden ser funciones, por lo que, en base a ello, podemos convertir funciones multiparamétricas y funciones de un solo parámetro de la siguiente manera:

currying: λx y.xy = λx.(λy. xy)

La función externa acepta un parámetro X y devuelve una función λy.xy. Esta función de retorno (función interna) acepta un parámetro Y y devuelve xy. La función externa e Y están vinculadas a la función interna, por lo que podemos implementar la función de la función multiparamétrica bajo la restricción de que la función lambda solo acepta un parámetro, que se llama forización λx y.xy se llama abreviatura. de λx.(λy.xy) por conveniencia de expresión.

Ahora que conocemos la definición básica y la sintaxis de las expresiones lambda, presentaremos cómo simplificarlas.

Para una aplicación de función (λ x x) y, significa que la aplicación de función λ x x se aplica a y, lo que equivale a x[x:=y], es decir, el resultado es y. En este proceso, (λ x x ) y ≡ x [x:=y] se llama reducción beta, x[x:=y] ≡ y se llama sustitución, [x:=y] se refiere a reemplazar la libertad en la expresión con y variable x.

Si tienes cuidado, podrás notar que algunos x ≠ y o y están especialmente marcados en las reglas de reemplazo. Restricciones como FV(N) están destinadas a evitar la ambigüedad durante el proceso de reducción de expresiones lambda.

Por ejemplo, el siguiente proceso:

Se puede ver que cuando las restricciones no se cumplen, la sustitución forzada conduce a resultados incorrectos. Entonces, ¿cómo lidiar con esta situación? Entonces necesitas conversión alfa.

Esta regla significa que la abstracción de la función lambda es equivalente antes y después de cambiar el nombre de la variable de enlace, es decir:

α: λx.x ≡ λy.y

Su función es resolver el conflicto del mismo nombre entre variables ligadas y variables libres.

Entonces el proceso de reducción de errores anterior se puede corregir:

¡Perfecto! Esto presenta la definición más básica y las reglas de reducción del cálculo lambda. Aunque el contenido es sencillo, es fácil volverse arrogante. Intenta practicar.

El uso flexible de alfa y beta puede resolver todos los problemas de reducción de expresiones lambda, pero considere la siguiente expresión:

Si se aplica a cualquier parámetro, como (λ x m x) n, después de β Después de la reducción y sustitución, se encontrará que es equivalente a M N. Esto no significa.

Sí, para la forma λ x m x, donde la expresión m no contiene la abstracción de función de la variable vinculada Elimine las abstracciones funcionales redundantes de las expresiones lambda.