Reprezentowanie liczb ujemnych i zespolonych za pomocą rachunku Lambda

Większość samouczków na temat rachunku Lambda stanowi przykład, w którym dodatnie liczby całkowite i liczby boolowskie mogą być reprezentowane przez funkcje. Co z -1 i ja?

data-structures lambda-calculus integers real-numbers zcaudate
źródło

Odpowiedzi:

Najpierw zakoduj liczby naturalne i pary, jak opisano w jmad.

Reprezentują liczbę całkowitą jako parę liczb naturalnych takich, że . Następnie możesz zdefiniować zwykłe operacje na liczbach całkowitych jako (używając notacji Haskell dla -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)

Przypadek liczb zespolonych jest podobny w tym sensie, że liczba zespolona jest kodowana jako para liczb rzeczywistych. Ale bardziej skomplikowanym pytaniem jest, jak zakodować rzeczywiste. Tutaj musisz wykonać więcej pracy:

Zakoduj liczbę wymierną jako parę gdzie jest liczbą całkowitą, jest naturalne, a . $q$ $(k,a)$ $k$ $a$ $q = k / (1 + a)$
Zakoduj liczbę rzeczywistą za pomocą funkcji tak że dla każdego naturalnego , koduje liczbę wymierną tak że . Innymi słowy, rzeczywistość jest kodowana jako sekwencja racjonałów zbiegających się z nią w tempie . $x$ $f$ $k \in \mathbb{N}$ $f k$ $q$ $|x - q| < 2^{-k}$ $k \mapsto 2^{-k}$

Kodowanie reali to dużo pracy i nie chcesz tego robić w -calculus. Ale zobacz na przykład podkatalog Marshall, aby zobaczyć prostą implementację wartości rzeczywistych w czystym Haskell. Można to w zasadzie przetłumaczyć na czysty -calculus. $\lambda$ etc/haskell $\lambda$

Andrej Bauer
źródło

Wow =) Intuicyjnie zastanawiam się, co to znaczy ... na przykład, używając kodowania liczb kościelnych ... tj. liczba kościelna liczby całkowitej n jest reprezentowana przez funkcję, która stosuje funkcję do wartości n razy. Czy pary i ujemne wartości lambda mają podobne intuicyjne odczucia?

zcaudate

Kodowanie kościelne koduje liczby naturalne

, ... Nie koduje liczb ujemnych. W powyższej odpowiedzi założyłem, że wiesz już o kodowaniu liczb naturalnych, więc wyjaśniłem, jak uzyskać liczby całkowite. Zakodowane przeze mnie liczby całkowite są bardziej formalną konstrukcją, w przeciwieństwie do liczb kościelnych, które są ściślej powiązane z rachunkiem

. Nie sądzę, by „ujemne wartości lambda” były znaczącym zwrotem.

0

$0$

1

$1$

2

$2$

λ

$\lambda$

Andrej Bauer

@zcaudate [TYP Objaśnienia: i:ℤ, x:a, f,u,s:a→a, p:(a→a,a→a)] W przypadku kodowania ℤ a (Sign,ℕ)następnie, ze względu parę funkcji (s,f)jak ptermin λi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x)spowoduje zarówno f(…f(x)…)lub s(f(…f(x)…))(jeśli wynik jest ujemny). Jeśli kodujesz ℤ as (ℕ,ℕ), potrzebujesz funkcji, która ma odwrotność - biorąc pod uwagę parę (f,u)i x, funkcja λi.λp.λx.(snd i)(snd p)((fst i)(fst p) x)wygeneruje, u(…u(f(…f(x)…))…)co pozostawi fzastosowane iczasy x. Oba działają w różnych kontekstach (wynik można „odwrócić” || fjest odwracalny).

nikt

@zcaudate Dodatkowe funkcje są konieczne, ponieważ liczby zakodowane w Kościele „powtarzają się same”, ale pary przekażą ci tylko ich elementy. Funkcje pomocnika po prostu sklejają komponenty w „właściwej” kolejności (co dzieje się automatycznie dla nats.) Zobacz także: en.wikipedia.org/wiki/… - Kodowanie w kościele jest w zasadzie fold . ctordla każdego konstruktora i tego typu fold( r). (Dlatego w przypadku typów rekurencyjnych dane „same się powtarzają”. W przypadku typów nierekurencyjnych bardziej przypomina casedopasowanie / wzorzec.)

nikt

Rachunek Lambda może kodować większość struktur danych i podstawowe typy. Na przykład, możesz zakodować parę istniejących terminów w rachunku lambda, używając tego samego kodowania Kościoła , które zwykle widzisz, aby zakodować nieujemne liczby całkowite i logiczne:

para = λ x y z . z x y

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

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

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

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

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

Zatem para to a jeśli chcesz odzyskać i , możesz zrobić i . $(a,b)$ $p=(\mbox{pair }ab)$ $a$ $b$ $(\mbox{fst }p)$ $(\mbox{snd }p)$

Oznacza to, że możesz łatwo przedstawić dodatnie i ujemne liczby całkowite za pomocą pary: znak po lewej stronie i wartość bezwzględna po prawej stronie. Znak jest wartością logiczną, która określa, czy liczba jest dodatnia. Po prawej jest liczba naturalna z wykorzystaniem kodowania Church.

(s ja sol n, n)

$(sign,n)$

A teraz, gdy masz względne liczby całkowite. Mnożenie jest łatwe do zdefiniowania, po prostu trzeba zastosować funkcji $\mbox{xor}$ na znak i mnożenia na liczbach naturalnych w wartości bezwzględnej:

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

Aby zdefiniować dodanie, musisz porównać dwie liczby naturalne i użyć odejmowania, gdy znaki są różne, więc nie jest to termin λ, ale możesz go dostosować, jeśli naprawdę chcesz:

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

ale wtedy odejmowanie jest naprawdę łatwe do zdefiniowania:

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

Gdy masz dodatnie i ujemne liczby całkowite, możesz bardzo łatwo zdefiniować liczby całkowite złożone : jest to tylko para dwóch liczb całkowitych które reprezentują . Zatem dodawanie jest punktowe, a mnożenie jest jak zwykle , ale nie będę tego pisać, powinno być łatwo: $(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
źródło

k

$k$

(a, b)

$(a,b)$

k = a - b

$k = a - b$

Złożone liczby całkowite w porządku, ale prosił o liczby zespolone. Z drugiej strony, oczywiście, nigdy nie mogą być reprezentowane, ponieważ są niepoliczalne.

HdM

@AndrejBauer: bardzo fajna sztuczka (być może nie taka prosta) HdM: na pewno mogą, nawet nie we wszystkich. Ale pomyślałem, że metoda budowania rzeczy w rachunku λ z kodowaniem Churcha była tutaj ważniejsza / odpowiedniejsza.

jmad

Chciałbym móc podać dwie poprawne odpowiedzi =) Nawet nie myślałem, że rzeczywiste mogą być reprezentowane, kiedy pytałem o liczby zespolone, ale proszę bardzo!

zcaudate