Représentation de nombres négatifs et complexes à l'aide du calcul lambda

La plupart des didacticiels sur Lambda Calculus fournissent un exemple où les entiers positifs et les booléens peuvent être représentés par des fonctions. Et -1 et moi?

data-structures lambda-calculus integers real-numbers zcaudate
la source

Réponses:

D'abord encoder des nombres naturels et des paires, comme décrit par jmad.

Représente un entier comme une paire de nombres naturels tels que . Ensuite, vous pouvez définir les opérations habituelles sur les entiers comme (en utilisant la notation Haskell pour -calculus): $k$ $(a,b)$ $k = a - b$ $\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)

Le cas des nombres complexes est similaire en ce sens qu'un nombre complexe est codé comme une paire de réels. Mais une question plus compliquée est de savoir comment coder les réels. Ici, vous devez faire plus de travail:

Encode un nombre rationnel comme une paire où est un entier, est naturel et $q$ $(k,a)$ $k$ $a$ $q = k / (1 + a)$ .
Coder un nombre réel par une fonction telle que pour tout naturel , code un nombre rationnel tel que . En d'autres termes, un réel est codé comme une séquence de rationnels convergeant vers lui à la vitesse . $x$ $f$ $k \in \mathbb{N}$ $f k$ $q$ $|x - q| < 2^{-k}$ $k \mapsto 2^{-k}$

Encoder des réels demande beaucoup de travail et vous ne voulez pas vraiment le faire dans le -calculus. Mais voir par exemple le sous - répertoire de Marshall pour une implémentation simple des réels en Haskell pur. Cela pourrait en principe être traduit par le -calculus pur . $\lambda$ etc/haskell $\lambda$

Andrej Bauer
la source

Wow =) Je me demande intuitivement ce que cela signifie ... par exemple, en utilisant l'encodage des numéros d'église ... ie. un numéro d'église de valeur entière n est représenté par une fonction qui applique une fonction à une valeur n fois. Les paires et les valeurs lambda négatives ont-elles une impression intuitive similaire à leur sujet?

zcaudate

Le codage d'église code les nombres naturels

0

$0$

1

$1$

2

$2$ , ... Il n'encode pas les nombres négatifs. Dans la réponse ci-dessus, j'ai supposé que vous connaissiez déjà un codage de nombres naturels, j'ai donc expliqué comment obtenir des entiers. Les entiers tels que je les ai encodés sont une construction plus formelle, contrairement aux chiffres de l'Église, qui sont plus étroitement liés au

-calculus. Je ne pense pas que "valeurs lambda négatives" soit une expression significative.

λ

$\lambda$

Andrej Bauer

@zcaudate [annotations de type: i:ℤ, x:a, f,u,s:a→a, p:(a→a,a→a)] Si vous encodez ℤ comme (Sign,ℕ)alors, étant donné une paire de fonctions (s,f)que ple terme λi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x)produira soit f(…f(x)…)ou s(f(…f(x)…))(si le résultat est négatif). Si vous encodez ℤ as (ℕ,ℕ), vous avez besoin d'une fonction qui a une inverse - étant donné une paire (f,u)et x, la fonction λi.λp.λx.(snd i)(snd p)((fst i)(fst p) x)produira u(…u(f(…f(x)…))…)ce qui laissera fles itemps appliqués à x. Les deux fonctionnent dans des contextes différents (le résultat peut être "inversé" || fest inversible).

personne le

@zcaudate Les fonctions supplémentaires sont nécessaires car les nombres encodés par l'Église "récursent d'eux-mêmes", mais les paires ne vous remettront que leurs composants. Les fonctions d'assistance collent simplement les composants ensemble dans le "bon" ordre (ce qui se produit automatiquement pour les nats.) Voir aussi: en.wikipedia.org/wiki/… - Le codage d'église est fondamentalement fold . ctorpour tout constructeur et ce type fold( r). (C'est pourquoi, pour les types récursifs, les données seront "récursives par elles-mêmes". Pour les types non récursifs, cela ressemble plus à une casecorrespondance de modèle /.)

personne le

Le lambda-calcul peut coder la plupart des structures de données et des types de base. Par exemple, vous pouvez encoder une paire de termes existants dans le calcul lambda, en utilisant le même encodage Church que vous voyez habituellement pour encoder des entiers non négatifs et booléens:

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)$

Alors la paire est et si vous voulez récupérer et vous pouvez faire et . $(a,b)$ $p=(\mbox{pair }ab)$ $a$ $b$ $(\mbox{fst }p)$ $(\mbox{snd }p)$

Cela signifie que vous pouvez facilement représenter des entiers positifs et négatifs avec une paire: le signe à gauche et la valeur absolue à droite. Le signe est un booléen qui spécifie si le nombre est positif. La droite est un nombre naturel utilisant le codage Eglise.

(s i g n, n)

$(sign,n)$

$\mbox{xor}$

{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))$

Pour définir l'addition, vous devez comparer deux nombres naturels et utiliser la soustraction lorsque les signes sont différents, donc ce n'est pas un terme λ mais vous pouvez l'adapter si vous voulez vraiment:

{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.$

but then subtraction is really easy to define:

{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)$

Once you have positive and negative integers you can define complex integers very easily: it is just a pair of two integers $(a,b)$ which represents $a+b\mbox{i}$ . Then addition is point-wise and multiplication is as usual, but I won't write it, it should be easy:

{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
la source

You can avoid the case distinctions if instead you represent the integer

k

$k$ as a pair of natural numbers

(a, b)

$(a,b)$ such that

k = a - b

$k = a - b$ .

Andrej Bauer

Complex integers alright, but he was asking for complex numbers. Then again, they of course can never be represented since there are uncountable.

HdM

@AndrejBauer: very nice trick (maybe not that simpler) HdM: sure they can, even in not all of them. But I figured that the method for building stuff in the λ-calculus with Church encoding was more important/appropriate here.

jmad

I wish I could give two correct answers =) I wasn't even thinking that reals could be represented when I asked about complex numbers but there you go!.

zcaudate