¿Cómo multiplicar en el cálculo lambda?

Question

Tengo problemas cuando intento multiplicar números de la Iglesia con lambda.

En primer lugar, ¿funciona?

MULT := $\lambda$ mnfx.m ( PLUS n )

MULT := $\lambda$ mnfx.m ( m SUCC n )

MULT := $\lambda$ mnfx.m(m f(n f x))

Por lo tanto, si multiplico 3 ( $\lambda$ fx.f(f(f x))) y 4 ( $\lambda$ fx.f(f(f(f x)))), debería verse así cuando empiece:

( $\lambda$ mnfx.m(m f(n f x)))( $\lambda$ fx.f(f(f x)))( $\lambda$ fx.f(f(f(f x))))

= $\lambda$ fx. $\lambda$ fx.f(f(f x))( $\lambda$ fx.f(f(f x)) f( $\lambda$ fx.f(f(f(f x))) f x))

= $\lambda$ fx. $\lambda$ fx.f(f(f x))( $\lambda$ fx.f(f(f x)) f(f(f(f x)))))

Aquí es donde estoy confundido. ¿Hago ( $\lambda$ fx.f(f(f x)))[f := f(f(f(f(f x))))]? O ( $\lambda$ fx.f(f(f x)))[f := f][x := f(f(f(f x)))]?

Si hago lo primero, entonces termino con:

= $\lambda$ fx. $\lambda$ fx.f(f(f x))( $\lambda$ fx.f(f(f x)) f(f(f(f x)))))

= $\lambda$ fx. $\lambda$ fx.f(f(f x))( $\lambda$ x.f(f(f(f(f x))))(f(f(f(f x))))(f(f(f(f x)))) x))

Y no estoy seguro de dónde ir desde allí, porque no tengo parámetros para la x.

Si hago lo segundo, entonces termino con:

= $\lambda$ fx. $\lambda$ fx.f(f(f x))(f

= $\lambda$ fx.f(f(f(f(f(f(f(f(f x))))))))

o 3 * 4 = 8, por lo que no puede ser correcto.

Answer 1

Parece que estás codificando el entero $n$ como $$ \textrm{N}(n) \equiv \lambda fx.\underbrace{f( \ldots f(f x) \ldots)}_{n\text{ applications}} $$

Esto facilita la multiplicación: multiplicar con $m$ necesita reemplazar cada $f$ con $m$ copias de $f$ y eso es exactamente lo que la representación de $m$ ya lo hace. Así que sólo tiene que establecer $$ \textrm{MULT} \equiv \lambda nmfx. n (m f) x = \lambda nmf.n (m f) $$ donde la segunda equivalencia se deriva de una $\eta$ -conversión.

Para $3\cdot 4$ obtienes $$\begin{eqnarray} \textrm{N}(3) &\equiv& \lambda fx.f(f(fx)) \\ \textrm{N}(4) &\equiv& \lambda gy.g(g(g(gy))) \\ \textrm{MULT}\, \textrm{N}(3)\, \textrm{N}(4) &\equiv& \left(\underline{\lambda nm}h. n (m h)\right)\, \left(\lambda fx.f(f(fx))\right)\, \left(\lambda gy.g(g(g(gy)))\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda fx.f(f(fx))\right) \left(\left(\underline{\lambda g}y.g(g(g(gy)))\right) h\right)\, \, \\ &\overset{\beta}{=}& \lambda h. \left(\underline{\lambda f}x.f(f(fx))\right) \left(\lambda y.h(h(h(hy)))\right)\, \, \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.\left(\lambda y.h(h(h(hy)))\right)\left(\left(\lambda y.h(h(h(hy)))\right)\left(\left(\underline{\lambda y}.h(h(h(hy)))\right)x\right)\right)\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.\left(\lambda y.h(h(h(hy)))\right)\left(\left(\underline{\lambda y}.h(h(h(hy)))\right)\left(h(h(h(hx)))\right)\right)\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.\left(\underline{\lambda y}.h(h(h(hy)))\right)\left(h(h(h(h(h(h(h(hx)))))))\right)\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.h(h(h(h(h(h(h(h(h(h(h(hx)))))))))))\right) \\ &=& \lambda hx.h(h(h(h(h(h(h(h(h(h(h(hx))))))))))) \\ &\equiv& \textrm{N}(12)\textrm{.} \end{eqnarray}$$ Equivalencias marcadas con $\beta$ proceden de $\beta$ -reducciones, y el reducido $\lambda$ -La expresión está subrayada. Las demás equivalencias son de naturaleza sintáctica.