Darstellung negativer und komplexer Zahlen mit Lambda-Kalkül

Die meisten Tutorials zu Lambda Calculus bieten Beispiele, in denen positive Ganzzahlen und Boolesche Werte durch Funktionen dargestellt werden können. Was ist mit -1 und ich?

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

Antworten:

Kodieren Sie zunächst natürliche Zahlen und Paare, wie von jmad beschrieben.

Stellen Sie eine ganze Zahl als ein Paar natürlicher Zahlen so dass . Dann können Sie die üblichen Operationen für ganze Zahlen wie folgt definieren (unter Verwendung der Haskell-Notation für Kalkül): $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)

Der Fall komplexer Zahlen ist in dem Sinne ähnlich, dass eine komplexe Zahl als ein Paar von Real codiert wird. Eine kompliziertere Frage ist jedoch, wie man reelle Zahlen codiert. Hier muss man mehr arbeiten:

Kodieren Sie eine rationale Zahl als Paar wobei eine ganze Zahl ist, natürlich ist und . $q$ $(k,a)$ $k$ $a$ $q = k / (1 + a)$
Encode eine reelle Zahl durch eine Funktion , so dass für jedes natürlichen , kodiert für eine rationale Zahl , so dass . Mit anderen Worten, ein Real wird als eine Folge von Rationalen codiert, die mit der Rate zu ihm konvergieren . $x$ $f$ $k \in \mathbb{N}$ $f k$ $q$ $|x - q| < 2^{-k}$ $k \mapsto 2^{-k}$

Das Codieren von Real ist eine Menge Arbeit und Sie möchten es nicht wirklich im Kalkül tun. Schauen Sie sich zum Beispiel das Unterverzeichnis von Marshall an, um eine einfache Implementierung von Real in pure Haskell zu erhalten. Dies könnte prinzipiell auf den reinen Kalkül übertragen werden. $\lambda$ etc/haskell $\lambda$

Andrej Bauer
quelle

Wow =) Ich frage mich intuitiv, was das bedeutet ... zum Beispiel mit der Kodierung der Kirchennummern ... dh. Eine Kirchennummer mit dem ganzzahligen Wert n wird durch eine Funktion dargestellt, die eine Funktion n-mal auf einen Wert anwendet. Haben Paare und negative Lambda-Werte ein ähnliches intuitives Gefühl?

Zcaudate

Die Kirchenkodierung kodiert die natürlichen Zahlen

0

$0$

1

$1$

2

$2$ , ... Sie kodiert keine negativen Zahlen. In der obigen Antwort habe ich angenommen, dass Sie bereits über eine Kodierung natürlicher Zahlen Bescheid wissen, und deshalb erklärt, wie man Ganzzahlen erhält. Die Ganzzahlen, wie ich sie codierte, sind eine formalere Konstruktion, im Gegensatz zu den Zahlen der Kirche, die mit dem

Kalkül enger verbunden sind. Ich denke nicht, dass "negative Lambda-Werte" eine aussagekräftige Phrase sind.

λ

$\lambda$

Andrej Bauer

@zcaudate [Typ Anmerkungen: i:ℤ, x:a, f,u,s:a→a, p:(a→a,a→a)] Wenn Sie kodieren z als (Sign,ℕ)dann, da ein Paar von Funktionen (s,f)wie pder Begriff λi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x)produziert entweder f(…f(x)…)oder s(f(…f(x)…))(wenn das Ergebnis negativ ist ). Wenn Sie ℤ as codieren (ℕ,ℕ), benötigen Sie eine Funktion, die ein inverses gegebenes Paar hat, (f,u)und xdie Funktion λi.λp.λx.(snd i)(snd p)((fst i)(fst p) x)wird erzeugen, u(…u(f(…f(x)…))…)was die fangewendeten iZeiten belässt x. Beide arbeiten in unterschiedlichen Kontexten (Ergebnis kann "gespiegelt" werden || fist invertierbar).

Niemand

@zcaudate Die zusätzlichen Funktionen sind notwendig, da kirchencodierte Zahlen "von selbst wiederkehren", aber Paare geben Ihnen nur ihre Komponenten. Die Hilfsfunktionen kleben die Komponenten einfach in der "richtigen" Reihenfolge zusammen (was bei nats automatisch geschieht). Siehe auch: En.wikipedia.org/wiki/... - Kirche Codierung ist im Grunde fold . ctorfür jeden Konstrukteur und diese Art der fold( r). (Aus diesem Grund werden die Daten bei rekursiven Typen "von selbst rekursiv". Bei nicht rekursiven Typen handelt es sich eher um eine case/ pattern-Übereinstimmung.)

nobody

Lambda-Kalkül kann die meisten Datenstrukturen und Grundtypen codieren. Sie können beispielsweise ein Paar vorhandener Terme im Lambda-Kalkül codieren, indem Sie dieselbe Church-Codierung verwenden, mit der Sie normalerweise nichtnegative Ganzzahlen und Boolesche Werte codieren:

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

Dann wird das Paar ist und wenn Sie möchten , um wieder und können Sie tun und . $(a,b)$ $p=(\mbox{pair }ab)$ $a$ $b$ $(\mbox{fst }p)$ $(\mbox{snd }p)$

Das bedeutet, dass Sie positive und negative ganze Zahlen mit einem Paar leicht darstellen können: das Vorzeichen links und den absoluten Wert rechts. Das Vorzeichen ist ein Boolescher Wert, der angibt, ob die Zahl positiv ist. Das Recht ist eine natürliche Zahl, die die Kodierung der Kirche verwendet.

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

Um die Addition zu definieren, müssen Sie zwei natürliche Zahlen vergleichen und Subtraktion verwenden, wenn sich die Vorzeichen unterscheiden. Dies ist also kein λ-Term, aber Sie können ihn anpassen, wenn Sie wirklich wollen:

{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
quelle

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