Lambda de cálculo e da igreja numerais confusão

Question

Eu estou tentando compreender as noções básicas de cálculo lambda e numerais Igreja. Tenho vindo a fazer um monte de leitura e praticando, mas parece-me manter a ficar preso com tentando ver como algumas funções de trabalho.

O exemplo que eu estou preso em é a seguinte. Talvez alguém pode explicar onde eu tenho errado ido.

O numeral Igreja para 1 pode ser representada como:

λf. λx. f x

A função exponenciação em numerais Church (m ⁿ ) pode ser dada como:

λm. λn. n m

Tudo que eu quero fazer é mostrar que, ao aplicar a função de exponenciação a 1 e 1, eu voltar 1, a partir de 1 ¹ = 1. eu estou fazendo isso, então eu entendo melhor como estes funções funcionam. Meu trabalho é o seguinte e eu ficar preso a cada vez:

// Exp (1 1)
(λm. λn. n m) (λf1. λx1. f1 x1) (λf2. λx2. f2 x2)
// Substitute for m
(λn. n (λf1. λx1. f1 x1)) (λf2. λx2. f2 x2)
// Substitute for n
(λf2. λx2. f2 x2) (λf1. λx1. f1 x1)
// Substitute for f2
(λx2. (λf1. λx1. f1 x1) x2)
// Substitute for f1
λx2. (λx1. x2 x1)

E lá eu estou preso. Perdi tanto f de, deixado com x só, e eu não tenho 1 volta. Onde estou indo errado?

Answer 1

Para onde estou indo errado?

Em nenhum lugar! Você Terminou. Lembre-se, os nomes das variáveis ??não são importantes; é a estrutura que é importante. O f nomes ou x2 não são significativos. Isso só importa como eles são usados. O numeral Igreja para 1 é

λf. λx. f x

e você tem

λx2. (λx1. x2 x1)

Rename x2 para f e x1 para x e voilà! Você tem

λf. (λx. f x)
= λf. λx. f x