람다 미적분학에서 입력이 신원 함수 일 때 참을 리턴하는 함수를 작성하는 방법은 무엇입니까?

Question

람다 미적분학에서 입력이 신원 함수 일 때 참을 리턴하는 함수를 작성하는 방법은 무엇입니까?

true로 교회에서 인코딩 한 값이 true라고 가정합니다.

작성하는 것이 쉬운 기능이어야하는 것처럼 보입니다. 그러나 내가 생각하는 모든 테스트에 대해 까다로운 입력은 그것을 능가 할 수 있습니다. 불가능한가요?

Answer 1

I := λx.x 
0 := λf.λx.x 
1 := λf.λx.f x 
TRUE := λx.λy.x 
FALSE := λx.λy.y 
PRED := λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u) 
ISZERO := λn.n (λx.FALSE) TRUE 

아이덴티티 함수 부호 교회 에타 당량이다. 아래의 Fn은 술어 기능을 통과 한 후 교회 숫자가 0으로 평가되지 않는 함수 (λf.λx.x)에 대해 FALSE을 반환합니다.

λx.(ISZERO (PRED x)) TRUE FALSE 

이 같은 동작 기능 BAD있을 수 있습니다 :

λx.(ISZERO (PRED x)) TRUE FALSE BAD := TRUE 
BAD != I