람다 미적분학 및 교회 숫자 혼란

Question

나는 람다 미적분학과 교회 숫자의 기본 사항을 이해하려고 노력하고 있습니다. 나는 많은 독서와 연습을 해왔지만 일부 기능이 어떻게 작동하는지 보려고 노력하는 데 계속 멈추는 것 같습니다.

내가 붙어있는 예는 다음과 같습니다. 아마도 누군가 내가 내가 잘못한 곳을 설명 할 수있을 것입니다.

1의 교회 숫자는 다음과 같이 표현 될 수 있습니다.

λf. λx. f x

교회 숫자의 지수 함수 (m^N)는 다음과 같이 주어질 수 있습니다.

λm. λn. n m

내가하고 싶은 것은 지수 함수를 1과 1에 적용함으로써 1이기 때문에 1을 돌려 받는다는 것을 보여줍니다.¹ = 1. 저는이 작업을 수행하고 있으므로 이러한 기능이 어떻게 작동하는지 더 잘 이해합니다. 내 작업은 다음과 같습니다. 매번 갇히게됩니다.

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

그리고 거기에 나는 붙어 있습니다. 나는 둘 다 잃었다 f남은 x단지, 나는 1 번을 얻지 못했습니다. 내가 어디로 잘못 가고 있습니까?

Answer 1

내가 어디로 잘못 가고 있습니까?

아무데도! 당신은 끝났습니다. 변수 이름은 중요하지 않습니다. 중요한 구조입니다. 이름 f 또는 x2 의미가 없습니다. 그들이 어떻게 사용되는지에만 중요합니다. 1의 교회 숫자는입니다

λf. λx. f x

그리고 당신이 가진 것은

λx2. (λx1. x2 x1)

이름 바꾸기 x2 에게 f 그리고 x1 에게 x 그리고 Voilà! 당신은 가지고 있습니다

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