Representación de números negativos y complejos usando cálculo Lambda

La mayoría de los tutoriales sobre el cálculo de Lambda proporcionan un ejemplo en el que los enteros positivos y los booleanos pueden representarse mediante funciones. ¿Qué pasa con -1 y yo?

data-structures lambda-calculus integers real-numbers zcaudate
fuente

Respuestas:

Primero codifique números y pares naturales, como lo describe jmad.

Representa un número entero $k$ como un par de números naturales $(a,b)$ tal que $k = a - b$ . Luego puede definir las operaciones habituales en enteros como (usando la notación de Haskell para cálculo $\lambda$ ):

neg = \k -> (snd k, fst k)
add = \k m -> (fst k + fst m, snd k + snd m)
sub = \k m -> add k (neg m)
mul = \k m -> (fst k * fst m + snd k * snd m, fst k * snd m + snd k * fst m)

El caso de los números complejos es similar en el sentido de que un número complejo está codificado como un par de reales. Pero una pregunta más complicada es cómo codificar los reales. Aquí tienes que hacer más trabajo:

Codifique un número racional como un par donde es un número entero, es natural y . $q$ $(k,a)$ $k$ $a$ $q = k / (1 + a)$
Codifique un número real mediante una función tal que para cada natural , codifique un número racional tal que . En otras palabras, un real se codifica como una secuencia de racionales que convergen a la velocidad . $x$ $f$ $k \in \mathbb{N}$ $f k$ $q$ $|x - q| < 2^{-k}$ $k \mapsto 2^{-k}$

Codificar reales es mucho trabajo y no quieres hacerlo en el cálculo . Pero vea, por ejemplo, el subdirectorio de Marshall para una implementación simple de reales en Haskell puro. En principio, esto podría traducirse al cálculo puro . $\lambda$ etc/haskell $\lambda$

Andrej Bauer
fuente

Wow =) Me pregunto intuitivamente qué significa eso ... por ejemplo, usando la codificación de los números de la iglesia ... es decir. un número de iglesia de valor entero n está representado por una función que aplica una función a un valor n veces. ¿Los pares y los valores lambda negativos tienen esa sensación intuitiva similar sobre ellos?

zcaudate

La codificación de la iglesia codifica los números naturales

, ... No codifica los números negativos. En la respuesta anterior supuse que ya conoces una codificación de números naturales, así que te expliqué cómo obtener números enteros. Los enteros como los codifiqué son una construcción más formal, a diferencia de los números de la Iglesia, que están más intrincadamente conectados con el cálculo

. No creo que "valores lambda negativos" sea una frase significativa.

0

$0$

1

$1$

2

$2$

λ

$\lambda$

Andrej Bauer

@zcaudate [anotaciones Tipo: i:ℤ, x:a, f,u,s:a→a, p:(a→a,a→a)] Si codifican ℤ como (Sign,ℕ)entonces, dado un par de funciones (s,f)como p, el término λi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x)producirá ya sea f(…f(x)…)o s(f(…f(x)…))(si el resultado es negativo). Si codifica ℤ como (ℕ,ℕ), necesita una función que tenga un inverso, dado un par (f,u)y x, la función λi.λp.λx.(snd i)(snd p)((fst i)(fst p) x)producirá u(…u(f(…f(x)…))…)lo que dejará los tiempos faplicados . Ambos funcionan en diferentes contextos (el resultado puede "voltearse" || es invertible). ixf

nadie

@zcaudate Las funciones adicionales son necesarias ya que los números codificados por la Iglesia "se repiten por sí mismos", pero los pares solo le entregarán sus componentes. Las funciones auxiliares solo pegan los componentes en el orden "correcto" (que ocurre automáticamente para los nats). Ver también: en.wikipedia.org/wiki/… - La codificación de la iglesia es básicamente fold . ctorpara cualquier constructor y ese tipo fold( r). (Es por eso que, para los tipos recursivos, los datos "recurrirán por sí mismos". Para los tipos no recursivos es más como una casecoincidencia de patrón /.)

nadie

El cálculo Lambda puede codificar la mayoría de las estructuras de datos y tipos básicos. Por ejemplo, puede codificar un par de términos existentes en el cálculo lambda, utilizando la misma codificación de Church que suele ver para codificar enteros no negativos y booleanos:

pair = λ x y z . z x y

$\mbox{pair}= λxyz.zxy$

fst = λ p . p (λ x y . x)

$\mbox{fst} = λp.p(λxy.x)$

snd = λ p . p (λ x y . y)

$\mbox{snd} = λp.p(λxy.y)$

Entonces el par es y si quieres volver y se puede hacer y . $(a,b)$ $p=(\mbox{pair }ab)$ $a$ $b$ $(\mbox{fst }p)$ $(\mbox{snd }p)$

Eso significa que puede representar fácilmente enteros positivos y negativos con un par: el signo a la izquierda y el valor absoluto a la derecha. El signo es un booleano que especifica si el número es positivo. El derecho es un número natural que usa la codificación de Church.

(s i g n, n)

$(sign,n)$

Y ahora que tienes enteros relativos. La multiplicación es fácil de definir, solo tiene que aplicar la función $\mbox{xor}$ en el signo y la multiplicación en números naturales en el valor absoluto:

{mult}_{ℤ} = λ a b . pair (xor (fst a) (fst b)) ({mult}_{ℕ} (snd a) (snd b))

$\mbox{mult}_ℤ=λab.\mbox{pair} ~~(\mbox{xor}(\mbox{fst }a)(\mbox{fst }b)) ~~(\mbox{mult}_ℕ(\mbox{snd }a)(\mbox{snd }b))$

Para definir la suma, debe comparar dos números naturales y usar la resta cuando los signos son diferentes, por lo que este no es un término λ pero puede adaptarlo si realmente desea:

{add}_{ℤ} = λ a b . {\begin{cases} (true, {add}_{ℕ} (snd a) (snd b)) & if a \geq 0 \land b \geq 0 \\ (false, {add}_{ℕ} (snd a) (snd b)) & if a < 0 \land b < 0 \\ (true, {sub}_{ℕ} (snd a) (snd b)) & if a \geq 0 \land b < 0 \land | a | \geq | b | \\ (false, {sub}_{ℕ} (snd b) (snd a)) & if a \geq 0 \land b < 0 \land | a | < | b | \\ (true, {sub}_{ℕ} (snd b) (snd a)) & if a < 0 \land b \geq 0 \land | a | < | b | \\ (false, {sub}_{ℕ} (snd a) (snd b)) & if a < 0 \land b \geq 0 \land | a | \geq | b | \end{cases}

$\mbox{add}_ℤ=λab.\left\{\begin{array}{ll} (\mbox{true},\mbox{add}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a≥0∧b≥0 \\ (\mbox{false},\mbox{add}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a<0∧b<0 \\ (\mbox{true},\mbox{sub}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a≥0∧b<0∧|a|≥|b| \\ (\mbox{false},\mbox{sub}_ℕ(\mbox{snd }b)(\mbox{snd }a)) & \mbox{if } a≥0∧b<0∧|a|<|b| \\ (\mbox{true},\mbox{sub}_ℕ(\mbox{snd }b)(\mbox{snd }a)) & \mbox{if } a<0∧b≥0∧|a|<|b| \\ (\mbox{false},\mbox{sub}_ℕ(\mbox{snd }a)(\mbox{snd }b)) & \mbox{if } a<0∧b≥0∧|a|≥|b| \\ \end{array}\right.$

pero luego la resta es realmente fácil de definir:

{minus}_{ℤ} = λ a . pair (not (fst a)) (snd a)

$\mbox{minus}_ℤ=λa.\mbox{pair}(\mbox{not}(\mbox{fst } a))(\mbox{snd } a)$

{sub}_{ℤ} = λ a b . {add}_{ℤ} (a) ({minus}_{ℤ} b)

$\mbox{sub}_ℤ=λab.\mbox{add}_ℤ(a)(\mbox{minus}_ℤb)$

$(a,b)$ $a+b\mbox{i}$

{add}_{ℤ [i]} = λ z_{1} z_{2} . pair ({add}_{ℤ} (fst z_{1}) (fst z_{2})) ({add}_{ℤ} (snd z_{1}) (snd z_{2}))

$\mbox{add}_{ℤ[\mbox{i}]}=λz_1z_2.\mbox{pair} (\mbox{add}_ℤ(\mbox{fst }z_1)(\mbox{fst }z_2)) (\mbox{add}_ℤ(\mbox{snd }z_1)(\mbox{snd }z_2))$

jmad
fuente

Puede evitar las distinciones entre mayúsculas y minúsculas si en cambio representa el número entero

k

$k$ como un par de números naturales

(a, b)

$(a,b)$ tal que

k = a - b

$k = a - b$ .

Andrej Bauer

Enteros complejos bien, pero estaba pidiendo números complejos. Por otra parte, por supuesto, nunca se pueden representar, ya que son incontables.

HdM

@AndrejBauer: muy buen truco (tal vez no tan simple) HdM: seguro que pueden, incluso en no todos. Pero pensé que el método para construir cosas en el cálculo λ con codificación de Church era más importante / apropiado aquí.

jmad

Desearía poder dar dos respuestas correctas =) ¡Ni siquiera estaba pensando que los reales podrían representarse cuando pregunté sobre números complejos, pero ahí lo tienes!

zcaudate