교회 숫자 : Lambda 미적분학에서 0 인코딩 방법은 무엇입니까?

Question

나는 Lambda 미적분학을 배우고 있지만 숫자 0의 인코딩을 이해할 수없는 것 같습니다.

어때 "함수와 두 번째 값을 취하고 인수에 0 회 기능을 적용하는 함수"제로? 0을 인코딩하는 다른 방법이 있습니까? 여기에 누군가가 0 인코딩을 도울 수 있습니까?

Answer 1

"함수를 취하고 두 번째 값을 취하고 인수에 0 회 함수를 적용하는 함수"는 물론 0이 아닙니다. 그것은 부호화 0의. 일반 람다 미적분학을 다룰 때 어떤 방식 으로든 숫자 (및 기타 원시 유형)를 인코딩해야하며 이러한 각 유형에 대해 몇 가지 요구 사항이 있습니다. 예를 들어, 자연 숫자에 대한 하나의 요구 사항은 주어진 숫자에 1을 추가 할 수 있고, 다른 하나는 더 큰 숫자와 0을 구별 할 수 있어야합니다 (더 알고 싶다면 "Peano Arithmetic"을 찾으십시오). Dario가 인용 한 인기 인코딩은이 두 가지를 제공하며, 무언가를 수행하는 함수로 정수 N을 나타냅니다 ( f 인수) n Times- 이것은 자연을 사용하는 일종의 자연스러운 방법입니다.

예를 들어, 목록을 나타낼 수 있으면 N을 N 항목 목록으로 표시 할 수 있습니다. 이 인코딩에는 장단점이 있지만 위의 인코딩은 가장 인기있는 것입니다.

Answer 2

보다 위키 백과:

0 ≡ λf.λx. x
1 ≡ λf.λx. f x
2 ≡ λf.λx. f (f x)
3 ≡ λf.λx. f (f (f x))
...
n ≡ λf.λx. fn x

Answer 3

람다 미적분학을 배우면 이미 λxy.y를 알고있을 것입니다. arg1 * arg2*가 줄어 듭니다 arg2, x는 아무것도 대체하고 나머지 (λy.y)는 신원 함수입니다.

다른 많은 방법으로 0을 쓸 수 있지만 (즉, 다른 컨벤션을 생각해 낼 수 있지만 λxy.y를 사용하는 데 좋은 이유가 있습니다. 예를 들어, 제로가 첫 번째 자연 숫자가되기를 원하므로 후속 기능을 적용하면 1, 2, 3 등이 나타납니다. 기능 λabc.b (ABC)를 사용하면 λxy.x (y)가됩니다. ), λxy.x (x (y)), λxy.x (x (x (y)) 등, 즉, 정수 시스템을 얻습니다.

또한, 첨가와 관련하여 0이 중립 요소가되기를 원합니다. 후속 기능 S : = λabc.b (ABC)를 사용하면 정의 할 수 있습니다. N+* m* AS N 에스 중, 즉, N 후속 기능의 적용을 시간에 적용합니다 중. 우리의 Zero λxy.y는 이것을 모두 0 s입니다 중 그리고 중 S 0 감소 중.