람다 미적분학 및 교회 숫자 혼란
-
20-08-2019 - |
문제
나는 람다 미적분학과 교회 숫자의 기본 사항을 이해하려고 노력하고 있습니다. 나는 많은 독서와 연습을 해왔지만 일부 기능이 어떻게 작동하는지 보려고 노력하는 데 계속 멈추는 것 같습니다.
내가 붙어있는 예는 다음과 같습니다. 아마도 누군가 내가 내가 잘못한 곳을 설명 할 수있을 것입니다.
1의 교회 숫자는 다음과 같이 표현 될 수 있습니다.
λf. λx. f x
교회 숫자의 지수 함수 (mN)는 다음과 같이 주어질 수 있습니다.
λm. λn. n m
내가하고 싶은 것은 지수 함수를 1과 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 번을 얻지 못했습니다. 내가 어디로 잘못 가고 있습니까?
해결책
내가 어디로 잘못 가고 있습니까?
아무데도! 당신은 끝났습니다. 변수 이름은 중요하지 않습니다. 중요한 구조입니다. 이름 f
또는 x2
의미가 없습니다. 그들이 어떻게 사용되는지에만 중요합니다. 1의 교회 숫자는입니다
λf. λx. f x
그리고 당신이 가진 것은
λx2. (λx1. x2 x1)
이름 바꾸기 x2
에게 f
그리고 x1
에게 x
그리고 Voilà! 당신은 가지고 있습니다
λf. (λx. f x)
= λf. λx. f x
제휴하지 않습니다 StackOverflow