Numerales de Church

Avanzado Lógica Aritmética

El cálculo λ no tiene números. Así que Church los inventó — y el truco es una de las ideas más hermosas de las matemáticas: un número es cuántas veces haces algo.

Contar como aplicar

0 = λf.λx.x aplica f cero veces — solo devuelve x 1 = λf.λx.f x aplica f una vez 2 = λf.λx.f (f x) aplica f dos veces 3 = λf.λx.f (f (f x)) tres veces

Lee λf.λx.… como «dame una forma de avanzar un paso (f) y un lugar donde empezar (x)». El numeral n es la máquina que avanza n pasos. Esto se llama un numeral de Church.

Por qué esto es profundo Números-como-repetición no es un truco — es discutiblemente lo que los números son. «Tres» significa «hazlo tres veces». Church no codificó el conteo; lo reveló.

Sucesor: añadir una aplicación

SUCC = λn.λf.λx.f (n f x) «toma el numeral n, luego el paso, luego el inicio — y haz una f extra encima»

Mira cómo SUCC 1 se convierte en 2 — cuatro pasos β, uno cada vez:

Suma y multiplicación

PLUS = λm.λn.λf.λx.m f (n f x) haz n pasos, luego m más MULT = λm.λn.λf.m (n f) una pila de m pasos de n cada uno

El truco sucio

Los numerales de Church suman y multiplican hermosamente. La resta es famosamente dolorosa — PRED existe pero el campo tardó años en encontrarlo. Necesita pares, que son asunto de la página siguiente.

Práctica

λf.λx.f (f (f x)) codifica ¿qué número? ___

ZERO = λf.λx.x — aplicar ZERO g v da…

Escribe el numeral de Church para 2: ___

SUCC n suma uno…

Siguiente: booleanos y pares · Anterior: beta reducción

← Inicio de Matemáticas · Investigación y referencias