Representando números negativos e complexos usando o cálculo Lambda

A maioria dos tutoriais sobre o Cálculo Lambda fornece um exemplo em que números inteiros positivos e booleanos podem ser representados por funções. E quanto a -1 e eu?

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

Respostas:

Primeiro codifique números e pares naturais, conforme descrito por jmad.

Represente um número inteiro como um par de números naturais tal que . Em seguida, você pode definir as operações usuais em números inteiros como (usando a notação Haskell para -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)

O caso de números complexos é semelhante no sentido em que um número complexo é codificado como um par de reais. Mas uma pergunta mais complicada é como codificar reais. Aqui você tem que fazer mais trabalho:

Codifique um número racional como um par que é um número inteiro, é natural e . $q$ $(k,a)$ $k$ $a$ $q = k / (1 + a)$
Codifique um número real por uma função tal que para cada natural , codifique um número racional tal que . Em outras palavras, um real é codificado como uma sequência de racionais convergindo para ele na taxa . $x$ $f$ $k \in \mathbb{N}$ $f k$ $q$ $|x - q| < 2^{-k}$ $k \mapsto 2^{-k}$

Codificar reais é muito trabalhoso e você não deseja realmente fazê-lo no -calculus. Mas veja, por exemplo, o subdiretório Marshall, para uma simples implementação de reais em puro Haskell. Isso poderia, em princípio, ser traduzido para o cálcio puro . $\lambda$ etc/haskell $\lambda$

Andrej Bauer
fonte

Uau =) Estou me perguntando intuitivamente o que isso significa ... por exemplo, usando os números da igreja que codificam ... ie. um número de igreja de valor inteiro n é representado por uma função que aplica uma função a um valor n vezes. Os pares e valores lambda negativos têm uma sensação intuitiva semelhante sobre eles?

Zcaudate 8/06

A codificação de igreja codifica números naturais

, ... Não codifica números negativos. Na resposta acima, assumi que você já sabia sobre uma codificação de números naturais, então expliquei como obter números inteiros. Os números inteiros, como os codifiquei, são uma construção mais formal, diferentemente dos numerais da Igreja, que são mais intrinsecamente conectados ao

cálcio. Não acho que "valores lambda negativos" sejam uma frase significativa.

0

$0$

1

$1$

2

$2$

λ

$\lambda$

Andrej Bauer

@zcaudate [Tipo anotações: i:ℤ, x:a, f,u,s:a→a, p:(a→a,a→a)] Se codificar ℤ como (Sign,ℕ)em seguida, dado um par de funções (s,f)como p, o termo λi.λp.λx.(fst i) (fst p) id ((snd i) (snd p) x)irão produzir tanto f(…f(x)…)ou s(f(…f(x)…))(se o resultado for negativo). Se você codificar ℤ como (ℕ,ℕ), precisará de uma função que tenha um inverso - dado um par (f,u)e x, a função λi.λp.λx.(snd i)(snd p)((fst i)(fst p) x)produzirá a u(…u(f(…f(x)…))…)qual deixará os tempos faplicados . Ambos funcionam em contextos diferentes (o resultado pode ser "invertido" || é invertível). ixf

ninguém

@zcaudate As funções extras são necessárias, pois os números codificados pela Igreja "recursam por conta própria", mas os pares entregam apenas seus componentes. As funções auxiliares apenas colam os componentes na ordem "correta" (o que ocorre automaticamente para nats.) Veja também: en.wikipedia.org/wiki/… - A codificação da igreja é basicamente fold . ctorpara qualquer construtor e esse tipo fold( r). (É por isso que, para os tipos de recursiva, os dados serão "recurse por conta própria" Para os tipos não-recursiva é mais como um. case/ Correspondência de padrão.)

ninguém

O cálculo lambda pode codificar a maioria das estruturas de dados e tipos básicos. Por exemplo, você pode codificar um par de termos existentes no cálculo lambda, usando a mesma codificação da Igreja que você normalmente vê para codificar números inteiros não negativos e booleanos:

par = λ x y z . z x y

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

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

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

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

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

Em seguida, o par é e se você quiser voltar e que você pode fazer e . $(a,b)$ $p=(\mbox{pair }ab)$ $a$ $b$ $(\mbox{fst }p)$ $(\mbox{snd }p)$

Isso significa que você pode facilmente representar números inteiros positivos e negativos com um par: o sinal à esquerda e o valor absoluto à direita. O sinal é um booleano que especifica se o número é positivo. O direito é um número natural usando a codificação da Igreja.

(s Eu g n, n)

$(sign,n)$

E agora que você tem números inteiros relativos. A multiplicação é fácil de definir, basta aplicar a função $\mbox{xor}$ no sinal e a multiplicação em números naturais no valor absoluto:

{mult}_{ℤ} = λ uma b . par (xor (primeiro uma) (primeiro b)) ({mult}_{ℕ} (snd uma) (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 a adição, você deve comparar dois números naturais e usar subtração quando os sinais forem diferentes; portanto, esse não é um termo λ, mas você pode adaptá-lo se realmente quiser:

{adicionar}_{ℤ} = λ uma b . {\begin{cases} (verdade, {adicionar}_{ℕ} (snd uma) (snd b)) & E se uma \geq 0 0 \land b \geq 0 0 \\ (falso, {adicionar}_{ℕ} (snd uma) (snd b)) & E se uma < 0 0 \land b < 0 0 \\ (verdade, {sub}_{ℕ} (snd uma) (snd b)) & E se uma \geq 0 0 \land b < 0 0 \land | uma | \geq | b | \\ (falso, {sub}_{ℕ} (snd b) (snd uma)) & E se uma \geq 0 0 \land b < 0 0 \land | uma | < | b | \\ (verdade, {sub}_{ℕ} (snd b) (snd uma)) & E se uma < 0 0 \land b \geq 0 0 \land | uma | < | b | \\ (falso, {sub}_{ℕ} (snd uma) (snd b)) & E se uma < 0 0 \land b \geq 0 0 \land | uma | \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.$

mas a subtração é realmente fácil de definir:

{menos}_{ℤ} = λ uma . par (não (primeiro uma)) (snd uma)

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

{sub}_{ℤ} = λ uma b . {adicionar}_{ℤ} (uma) ({menos}_{ℤ} b)

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

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

{adicionar}_{ℤ [Eu]} = λ z_{1} z_{2} . par ({adicionar}_{ℤ} (primeiro z_{1}) (primeiro z_{2})) ({adicionar}_{ℤ} (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
fonte

k

$k$

(a, b)

$(a,b)$

k = a - b

$k = a - b$

Inteiros complexos, tudo bem, mas ele estava pedindo números complexos. Por outro lado, é claro que eles nunca podem ser representados, pois são incontáveis.

HdM

@AndrejBauer: truque muito bom (talvez não tão simples) HdM: com certeza eles podem, mesmo em nem todos eles. Mas achei que o método para construir coisas no cálculo-λ com codificação da Igreja era mais importante / apropriado aqui.

Jmad

Eu gostaria de poder dar duas respostas corretas =) Eu nem estava pensando que os reais pudessem ser representados quando perguntei sobre números complexos, mas aí está!

Zcaudate 16/06/2012