Consulta em booleanos no cálculo lambda

Question

Esta é a representação do cálculo lambda para o operador e:

lambda(m).lambda(n).lambda (a).lambda (b). m(n a b) b

Alguém pode me ajudar a entender essa representação?

Answer 1

Para entender como representar booleanos no cálculo lambda, ajuda a pensar em uma expressão IF, "se a então b else c". Esta é uma expressão que escolhe o primeiro ramo, B, se for verdadeiro, e o segundo, C, se for falso. As expressões lambda podem fazer isso com muita facilidade:

lambda(x).lambda(y).x

dará a você o primeiro de seus argumentos, e

lambda(x).lambda(y).y

dá a você o segundo. Então, se A é uma dessas expressões, então

a b c

dá um b ou c, que é exatamente o que queremos o se fazer. Então defina

 true = lambda(x).lambda(y).x
false = lambda(x).lambda(y).y

e a b c vai se comportar como if a then b else c.

Olhando dentro da sua expressão em (n a b), que significa if n then a else b. Então m (n a b) b significa

if m then (if n then a else b) else b

Esta expressão avalia para a se ambos m e n são true, e para b por outro lado. Desde a é o primeiro argumento de sua função e b é o segundo, e true foi definido como uma função que dá o primeiro de seus dois argumentos, então se m e n são ambos true, assim como toda a expressão. Caso contrário, é false. E essa é apenas a definição de and!

Tudo isso foi inventado pela igreja de Alonzo, que inventou o cálculo Lambda.

Answer 2

No cálculo lambda, um booleano é representado por uma função que leva dois argumentos, um para o sucesso e outro para falha. Os argumentos são chamados continuações, porque eles continuam com o restante da computação; O verdadeiro booleano chama a continuação do sucesso e o falso booleano chama a continuação da falha. Essa codificação é chamada de codificação da igreja, e a idéia é que um booleano é muito parecido com uma "função se-then-else".

Então podemos dizer

true  = \s.\f.s
false = \s.\f.f

Onde s significa sucesso, f significa falha, e a barra de barriga é um lambda ASCII.

Agora espero que você possa ver para onde isso está indo. Como codificamos and? Bem, em c poderíamos expandi -lo para

n && m = n ? m : false

Só estas são funções, então

(n && m) s f = (n ? m : false) s f = n ? (m s f) : (false s f) = n ? (m s f) : f

Mas, o construto ternário, quando codificado no cálculo lambda, é apenas aplicação de função, então temos

(n && m) s f = (n m false) s f = n (m s f) (false s f) = n (m s f) f

Então finalmente chegamos a

&& = \n . \m . \s . \f . n (m s f) f

E se renunciarmos às continuações de sucesso e fracasso a e b Voltamos ao seu original

&& = \n . \m . \a . \b . n (m a b) b

Como em outros cálculos no cálculo lambda, especialmente ao usar as codificações da igreja, Muitas vezes é mais fácil resolver as coisas com leis algébricas e raciocínio equacional, depois converta em lambdas no final.

Answer 3

Na verdade, é um pouco mais do que apenas o operador. É a versão do Lambda Cálculo de if m and n then a else b. Aqui está a explicação:

No Lambda Calculus True, é representado como uma função, levando dois argumentos* e retornando o primeiro. Falso é representado como função, tomando dois argumentos* e retornando o segundo.

A função que você mostrou acima leva quatro argumentos*. Pela aparência dele e n, deve ser booleanos e A e B, alguns outros valores. Se m for verdadeiro, ele avaliará seu primeiro argumento que é n a b. Isso, por sua vez, avaliará para A se n é verdadeiro e B se n for falso. Se m for falso, ele avaliará seu segundo argumento b.

Então, basicamente, a função retorna a se M e N forem verdadeiros e B de outra forma.

(*) Onde "levar dois argumentos" significa "argumentar e devolver uma função assumindo outro argumento".

Edite em resposta ao seu comentário:

and true false Como visto na página do wiki, funciona assim:

O primeiro passo é simplesmente substituir cada identificador por sua definição, ou seja, (λm.λn. m n m) (λa.λb. a) (λa.λb. b). Agora a função (λm.λn. m n m) é aplicado. Isso significa que toda ocorrência de m em m n m é substituído pelo primeiro argumento ((λa.λb. a)) e toda ocorrência de n é substituída pelo segundo argumento ((λa.λb. b)). Então nós conseguimos (λa.λb. a) (λa.λb. b) (λa.λb. a). Agora simplesmente aplicamos a função (λa.λb. a). Como o corpo desta função é simplesmente um, ou seja, o primeiro argumento, isso avalia (λa.λb. b), ou seja false (Como λx.λy. y significa false).