Beta reducción
Avanzado Lógica Computación
Aquí está el motor entero del cálculo λ y, por tanto — en un sentido muy real — el motor entero de la computación.
La regla
Un término de la forma (λx.M) N se llama un
redex — una expresión reducible. Encontrar
uno y reescribirlo es un paso β. Sigue hasta que no
quede ningún redex y tienes una forma normal: una
respuesta.
Cámara lenta
Nada se «computó» en el sentido aritmético — la máquina simplemente reescribió símbolos y la respuesta cayó sola. Míralo ocurrir en directo:
¿Qué redex primero? El orden importa — más o menos
Los términos grandes pueden contener varios redex a la vez. Dos estrategias clásicas:
- Orden normal — reduce siempre el redex más externo y más a la izquierda. Paciente, perezoso, siempre encuentra la respuesta si existe.
- Orden aplicativo — reduce los argumentos primero, luego aplica. Ansioso; más rápido cuando el argumento se necesita, desperdiciador cuando no.
El teorema de Church–Rosser garantiza la parte tranquilizadora: si dos estrategias terminan, coinciden en la respuesta. Solo está en juego si terminas.
La trampa: la captura
La sustitución tiene un modo de fallo sutil. Mira:
La y entrante era libre — pertenecía a quien
escribiera el término. Dejarla caer bajo una λy la
secuestra como variable ligada. La solución es el
α-renombrado: las variables ligadas son ficticias y
pueden renombrarse libremente — λy.x y
λw.x son la misma función — así que renombramos antes
de sustituir.
λx.f x ≡ f —
una función que simplemente reenvía su argumento es la
función. No la necesitarás mucho, pero la conocerás.
Tu turno a los mandos
Escribe cualquier término λ (usa λ o \), o pulsa un preajuste:
(λx.λy.x) y se reduce a ___ (α-renombrado permitido)
Un término sin redexes está en…
¿Qué orden reduce el redex más externo y más a la izquierda?
(λx.λy.y) a b → ___
Siguiente: numerales de Church · Anterior: sintaxis lambda