람다의 미적분학에서 scc에 대한 나의 대체 정의가 맞습니까?

Question

scc은 교회 번호 n을 받아 교회 번호를 반환하는 연결자 (후임자)입니다.

c_0 = λs. λz. z; 
c_1 = λs. λz. s z; 
c_2 = λs. λz. s (s z); 
c_3 = λs. λz. s (s (s z)); 
... 

SCC 정의 할 수 있습니다 :

scc' = λn. λs. c_1 s n; 

해당 :

scc = λn. λs. λz. s (n s z); 

가 정의되어

우리는 다음과 같이 교회 숫자가 정의되어 있음을 염두에두고? scc'는 교회 부호인가되어,

이 결과 베타 환원

foo = scc' c_2 
    = (λn. λs. s n) c_2 
    = s c_2 
    = s (s (s z)) 
    = c_3 

Answer 1

번호 :

scc' = λn. λs. c_1 s n; 
    = λn. λs. (λs. λz. s z) s n 
    = λn. λs. (λz. s z) n 
    = λn. λs. s n 

보다 일반적으로는 부호있는 교회 x

x = λn. λs. x s n 

은 유도에 의해 입증 될 수 있거나 단지 η 수축의 이중 적용이라는 것을 관찰함으로써 입증 될 수있다.

EDIT :이 기능이 어떻게 작동하는지 설명하려면 확장하십시오.

교회 숫자가 정확한지 어떻게 알 수 있습니까? 음, 숫자와 기본 산술로 람다 미적분을 확장했다고 상상해보십시오. 그럼 난 당신이 succesor 기능은 다음과 같습니다

fromChurch c_0 
    = (λc. c (λn. n + 1) 0) (λs. λz. z) 
    = (λs. λz. z) (λn. n + 1) 0) 
    = (λz. z) 0 
    = 0 
fromChurch c_1 
    = (λc. c (λn. n + 1) 0) (λs. λz. s z) 
    = (λs. λz. s z) (λn. n + 1) 0 
    = (λz. (λn. n + 1) z) 0 
    = (λn. n + 1) 0 
    = 0 + 1 
    = 1 
fromChurch c_2 
    = (λc. c (λn. n + 1) 0) (λs. λz. s (s z)) 
    = (λs. λz. s (s z)) (λn. n + 1) 0 
    = (λz. (λn. n + 1) ((λn. n + 1) z) 0 
    = (λn. n + 1) ((λn. n + 1) 0) 
    = ((λn. n + 1) 0) + 1 
    = (0 + 1) + 1 
    = 2 

기대 fromChurch이 방법으로 숫자에 교회 숫자로 변환 주장

fromChurch = λc. c (λn. n + 1) 0 

다음 함수를 정의한다 (참고, 당신은 λs 누락되었다) 여기

scc = λn. λs. λz. s (n s z) 

는 succesor function

에 대한 정확성의 조건

fromChurch (scc x) 
    = (λc. c (λn. n + 1) 0) ((λn. λs. λz. s (n s z)) x) 
    = (λn. λs. λz. s (n s z)) x (λn. n + 1) 0 
    = (λs. λz. s (x s z)) (λn. n + 1) 0 
    = (λz. (λn. n + 1) (x (λn. n + 1) z)) 0 
    = (λn. n + 1) (x (λn. n + 1) 0) 
    = (x (λn. n + 1) 0) + 1 
    = ((λc. c (λn. n + 1) 0) x) + 1 
    = (fromChurch x) + 1 

참고 마지막 단계의 두 번째 단계는 베타 감소 대신 베타 확장이었습니다.

요점은 scc은 실제로 정수 값이 1 인 교회 숫자를 계산한다는 것입니다.

반면에 λn. λs. c_1 s n은 교회 숫자에서 교회 숫자까지의 기능이 아닙니다 ... 단지 교회 숫자입니다. 사실 교회 숫자 값은 1입니다. 결코 후계자를 취하지는 않습니다.

편집 2 :

감소 순서는 당신이 제공

foo = scc' c_2 
= (λn. λs. s n) c_2 
= s c_2 
= s (s (s z)) 
= c_3 

는

(λn. λs. s n) c_2 
= λs. s c_2 

아주 정확하지 않습니다 및 λs. s c_2 따라서 c_3 같지 않은 정상적인 형태이며, 때문에 그 수행 .