lambda calculus - significado - Pasos de reducción de cálculo de Lambda
lambda symbol (1)
Estoy estudiando Lambda Cálculo y estoy atascado en Reducción ... ¿Alguien puede explicar los tipos de reducción con este ejemplo, especialmente la reducción beta de la manera más sencilla posible? Tampoco le importaría un tutorial fácil de entender.
(λxyz .xyz )(λx .xx )(λx .x )x
Calculo lambda
El cálculo Lambda tiene una forma de girar en espiral en muchos pasos, lo que hace que los problemas de resolución sean tediosos, y puede parecer realmente difícil, pero en realidad no es tan malo. En el cálculo lambda, solo hay lambdas, y todo lo que puedes hacer con ellas es la sustitución. Lambdas es como una función o método si está familiarizado con la programación, son funciones que toman una función como entrada y devuelven una nueva función como salida.
Hay básicamente dos procesos y medio en el cálculo lambda:
1) Conversión alfa: si está aplicando dos expresiones lambda con el mismo nombre de variable en el interior, cambia una de ellas por un nuevo nombre de variable. Por ejemplo (λx.xx) (λx.x) se convierte en algo así como (λx.xx) (λy.y) o (λx.xx) (λx''.x '') después de la reducción. El resultado es equivalente a lo que empezaste con, solo que con diferentes nombres de variables.
2) Reducción Beta - Básicamente solo sustitución. Este es el proceso de llamar a la expresión lambda con entrada y obtener la salida. Una expresión lambda es como una función, se llama la función sustituyendo la entrada en toda la expresión. Tome (λx.xy) z, la segunda mitad de (λx.xy), todo después del período, se imprime, conserva la salida, pero sustituye la variable (nombrada antes del período) con la entrada provista. z es la entrada, x es el nombre del parámetro, xy es la salida. Encuentre todas las apariciones del parámetro en la salida, y reemplácelas con la entrada y eso es lo que reduce, por lo que (λx.xy)z => xy con z sustituido por x , que es zy .
2.5) Eta Conversion / Eta Reduction: se trata de una reducción de casos especial, a la que solo llamo medio proceso, porque es algo así como Beta Reduction, algo así como, técnicamente, no lo es . Puede verlo escrito en wikipedia o en un libro de texto como "La conversión de Eta se convierte entre λx. (Fx) yf cuando x no aparece libre en f", lo que suena realmente confuso. Todo lo que realmente significa es λx. (Fx) = f si f no hace uso de x. Si realmente tiene sentido completo pero se muestra mejor a través de un ejemplo. Considere (λx. (Λy.yy) x), esto es equivalente a través de la reducción eta a (λy.yy), porque f = (λy.yy), que no tiene una x, puede mostrarlo al reducirlo , como resolvería a (λx.xx), que es observable la misma cosa. Usted dijo que se centre en la reducción beta, por lo que no voy a discutir la conversión de eta con el detalle que merece, pero muchas personas lo intentaron en el intercambio de pila de la teoría cs
En la notación para la reducción Beta:
Voy a usar la siguiente notación para sustituir la entrada provista en la salida:
(λ param . output)input => output [param := input] => result
Esto significa que sustituimos las apariciones de param en la salida, y eso es lo que reduce a
Ejemplo:
(λx.xy)z
= (xy)[x:=z]
= (zy)
= zy
Basta de teoría, vamos a resolver esto. Lambda Cálculo es muy divertido.
El problema que surgió se puede resolver solo con Conversión alfa y Reducción Beta. No se desanime por el tiempo que dura el proceso a continuación. Es bastante largo, sin duda, pero ningún paso para resolverlo es realmente difícil.
(λxyz.xyz) (λx.xx) (λx.x) x
= (((λxyz.xyz) (λx.xx)) (λx.x)) x - Añadamos el paréntesis en "Orden normal", asociatividad a la izquierda, abc se reduce como ((ab) c), donde b se aplica a a, yc se aplica al resultado de esa
= (( (λxyz.xyz) (λx.xx) ) (λx.x)) x - Seleccione la aplicación anidada más profunda y redúzcala primero.
La sección en negrita se reduce como:
(λxyz.xyz) (λx.xx)
= (λx.λyz.xyz) (λx.xx) - significa lo mismo, pero sacamos el primer parámetro ya que lo vamos a reducir y por eso quiero que quede claro
= (λx.λyz.xyz) (λx''.x''x '') - Conversión alfa, algunas personas se apegan a nuevas letras, pero me gusta agregar números al final o `s, de cualquier manera está bien. Debido a que ambas expresiones usan el parámetro x, tenemos que cambiarles el nombre en un lado, porque las dos X son variables locales, por lo que no tienen que representar lo mismo.
= (λyz.xyz) [x: = λx''.x''x ''] - Notación para una reducción beta, eliminamos el primer parámetro y reemplazamos sus ocurrencias en la salida con lo que se está aplicando [a: = b] denota que a debe ser reemplazado por b.
= (λyz. (λx''.x''x '') yz) - La reducción real, reemplazamos la aparición de x con la expresión lambda proporcionada.
= (λyz. ( (λx''.x''x '') y) z) - Orden normal para paréntesis nuevamente, y busque, otra aplicación para reducir, esta vez y se aplica a (λx .x x`), así que reduzcamos que ahora
= (λyz. ((x''x '') [x'': = y]) z) - Ponga esto en notación para la reducción beta.
= (λyz. (yy) z): cambiamos las dos apariciones de x''x ''por Ys, y esto ahora está completamente reducido.
Agregue esto nuevamente a la expresión original:
(( (λxyz.xyz) (λx.xx) ) (λx.x)) x
= ((λyz. (yy) z) (λx.x)) x - Esto no es nuevo, solo ponemos de nuevo lo que encontramos anteriormente.
= ( (λyz. (yy) z) (λx.x) ) x - Agarra la aplicación anidada más profunda, es de (λx.x) aplicada a (λyz. (yy) z)
Resolveremos esto por separado otra vez:
(λyz. (yy) z) (λx.x)
= (λy.λz. (yy) z) (λx.x) - Solo sacando el primer parámetro para mayor claridad.
= (λz. (yy) z) [y: = (λx.x)] - Poner en notación de reducción beta, sacamos el primer parámetro y notamos que Ys cambiará por (λx.x)
= (λz. ( (λx.x) (λx.x) ) z) - La reducción / sustitución real, la sección en negrita ahora se puede reducir
= (λz. ( (x) [x: = λx.x] ) z) - Esperemos que ya tengas la imagen, estamos comenzando a reducir beta (λx.x) (λx.x) al ponerla en la forma (x) [x: = λx.x]
= (λz. ( (λx.x) ) z) - Y allí está la sustitución
= (λz. (λx.x) z ) - Limpiar el paréntesis excesivo, y qué encontramos, pero otra aplicación para tratar
= (λz. (x) [x: = z]) - Pop el parámetro x, puesto en notación
= (λz. (z)) - Realizar la sustitución
= (λz.z) - Limpie el paréntesis excesivo
Ponlo de nuevo en la expresión principal:
( (λyz. (yy) z) (λx.x) ) x
= ( (λz.z) ) x - Completando lo que probamos arriba
= (λz.z) x - limpiando el paréntesis excesivo, ahora se reduce a una aplicación final, se aplica x a (λz.z)
= (z) [z: = x] - reducción beta, puesta en notación
= (x) - hacer la sustitución
= x - limpiar el paréntesis excesivo
Así que sí. La respuesta es x , se redujo simplemente groovy.