람다 미적분학과 교회 숫자 혼동

Question

나는 람다 미적분학과 교회 숫자의 기초를 이해하려고 노력하고있다. 나는 많은 독서와 연습을 해왔지만, 나는 어떤 기능이 어떻게 작동하는지 보려고 애 쓰고있는 것 같다.

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

로

교회 숫자가 표현 될 수있다 :

λm. λn. n m 

모든 내가 원하는 :

가

λf. λx. f x 

교회 부호 (m ^N)의 지수 함수로서 주어질 수있다 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이라는 이름은 의미가 없습니다. 그것들이 어떻게 사용되는지는 중요합니다. 하나의 교회 숫자는

λf. λx. f x 

그리고 당신은 x 봐라에 f-x2 및 x1의 이름을 변경

λx2. (λx1. x2 x1) 

있다! 당신은

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