[algorithm] λ 미적분 최적 평가자가 공식없이 큰 모듈 식 지수를 계산할 수있는 이유는 무엇입니까?

교회 번호는 자연수를 함수로 인코딩 한 것입니다.

(\ f x  (f x))             -- church number 1
(\ f x  (f (f (f x))))     -- church number 3
(\ f x  (f (f (f (f x))))) -- church number 4

깔끔하게, 당신은 단지 그들을 적용하여 두 교회 번호를 지수화 할 수 있습니다. 즉, 4 대 2를 적용하면 교회 번호 16또는 을 얻습니다 2^4. 분명히, 그것은 실용적이지 않습니다. 교회 수는 선형적인 양의 기억이 필요하며 실제로는 매우 느립니다. 10^10GHCI가 신속하게 올바르게 응답하는 것과 같은 컴퓨팅 은 오래 걸리고 컴퓨터의 메모리에 맞지 않을 수 있습니다.

최근에 최적의 λ 평가자를 실험하고 있습니다. 내 테스트에서 실수로 최적의 λ 계산기에 다음을 입력했습니다.

10 ^ 10 % 13

지수가 아닌 곱셈이어야합니다. 손가락을 움직여 영원히 실행되는 프로그램을 절망에 빠뜨리기 전에 내 요청에 대답했습니다.

3
{ iterations: 11523, applications: 5748, used_memory: 27729 }

real    0m0.104s
user    0m0.086s
sys     0m0.019s

“버그 알림”이 깜박이면서 Google에 가서 확인했습니다 10^10%13 == 3. 그러나 λ- 계산기는 그 결과를 찾지 못했으며 10 ^ 10을 거의 저장할 수 없습니다. 나는 과학을 위해 그것을 강조하기 시작했다. 그것은 즉시 나에게 대답 20^20%13 == 3, 50^50%13 == 4, 60^60%3 == 0. 내가 사용했다 외부 도구를 하기 때문에, 그 결과를 확인하기 위해 하스켈 자체가 (때문에 정수 오버 플로우)를 계산할 수 없습니다 (당신은 물론, 정수하지 INTS를 사용하는 경우입니다!). 그것을 한계로 밀어 넣은 결과는 다음과 200^200%31같습니다.

5
{ iterations: 10351327, applications: 5175644, used_memory: 23754870 }

real    0m4.025s
user    0m3.686s
sys 0m0.341s

만약 우리가 우주의 각 원자에 대해 하나의 우주 사본을 가지고 있고 우리가 가진 각 원자에 대한 컴퓨터를 가지고 있다면 교회 번호를 저장할 수 없었습니다 200^200. 이것은 내 맥이 정말 강력한 지 의문을 제기했습니다. 최적의 평가자가 불필요한 분기를 건너 뛰고 Haskell이 게으른 평가와 같은 방식으로 정답에 도달했을 수 있습니다. 이를 테스트하기 위해 λ 프로그램을 Haskell에 컴파일했습니다.

data Term = F !(Term -> Term) | N !Double
instance Show Term where {
    show (N x) = "(N "++(if fromIntegral (floor x) == x then show (floor x) else show x)++")";
    show (F _) = "(λ...)"}
infixl 0 #
(F f) # x = f x
churchNum = F(\(N n)->F(\f->F(\x->if n<=0 then x else (f#(churchNum#(N(n-1))#f#x)))))
expMod    = (F(\v0->(F(\v1->(F(\v2->((((((churchNum # v2) # (F(\v3->(F(\v4->(v3 # (F(\v5->((v4 # (F(\v6->(F(\v7->(v6 # ((v5 # v6) # v7))))))) # v5))))))))) # (F(\v3->(v3 # (F(\v4->(F(\v5->v5)))))))) # (F(\v3->((((churchNum # v1) # (churchNum # v0)) # ((((churchNum # v2) # (F(\v4->(F(\v5->(F(\v6->(v4 # (F(\v7->((v5 # v7) # v6))))))))))) # (F(\v4->v4))) # (F(\v4->(F(\v5->(v5 # v4))))))) # ((((churchNum # v2) # (F(\v4->(F(\v5->v4))))) # (F(\v4->v4))) # (F(\v4->v4))))))) # (F(\v3->(((F(\(N x)->F(\(N y)->N(x+y)))) # v3) # (N 1))))) # (N 0))))))))
main = print $ (expMod # N 5 # N 5 # N 4)

이것은 1( 5 ^ 5 % 4)를 올바르게 출력 하지만 위에 아무것도 던지면 10^10가설이 없어 질 것입니다.

내가 사용하는 최적의 평가자는 지수 계수 수학의 모든 종류가 포함되지 않은 긴 160 선, 최적화되지 않은 자바 스크립트 프로그램입니다 – 내가 똑같이 간단 사용되는 람다 계산법 계수 기능 :

ab.(bcd.(ce.(dfg.(f(efg)))e))))(λc.(cde.e)))(λc.(a(bdef.(dg.(egf))))(λd.d)(λde.(ed)))(bde.d)(λd.d)(λd.d))))))

특정 모듈 식 산술 알고리즘이나 공식을 사용하지 않았습니다. 그렇다면 최적의 평가자가 어떻게 정답에 도달 할 수 있습니까?



답변

이 현상은 공유 베타 감소 단계의 양에서 비롯되며, Haskell 스타일의 게으른 평가 (또는 이와 관련하여 멀지 않은 일반적인 값별 호출)와 Vuillemin-Lévy-Lamping-에서 크게 다를 수 있습니다. Kathail-Asperti-Guerrini- (et al…) “최적의”평가. 이것은 일반적인 기능으로,이 특정 예에서 사용할 수있는 산술 공식과는 완전히 독립적입니다.

공유 란 하나의 “노드”가 사용자가 나타내는 실제 람다 용어의 몇 가지 유사한 부분을 설명 할 수있는 람다 용어를 나타냅니다. 예를 들어, 용어를 나타낼 수 있습니다

\x. x ((\y.y)a) ((\y.y)a)

(지시 된 비순환) 그래프를 사용하여을 나타내는 하위 그래프가 한 번만 나타나고 (\y.y)a해당 하위 그래프를 대상으로하는 두 개의 가장자리가 있습니다. 하스켈 용어로, 당신은 한 번만 평가하는이 썽크와이 썽크에 대한 두 개의 포인터를 가지고 있습니다.

Haskell 스타일 메모는 완전한 하위 용어 공유를 구현합니다. 이 공유 수준은 방향성 비순환 그래프로 나타낼 수 있습니다. 최적 공유에는이 제한이 없습니다. “부분”하위 용어도 공유 할 수 있으며 이는 그래프 표현의 순환을 의미 할 수 있습니다.

이 두 가지 공유 수준의 차이점을 보려면 용어를 고려하십시오.

\x. (\z.z) ((\z.z) x)

이 하스켈의 경우와 같이 사용자의 공유가 완전한 하위 용어로 제한되어있는 경우, 당신은 단 하나 개의 발생이있을 수 \z.z있지만,이 베타 – redexes 여기 구별되어야한다 : 하나는 (\z.z) x다른 하나는 (\z.z) ((\z.z) x), 그들이 동등한 조건이 아니기 때문에 공유 할 수 없습니다. 일부 하위 용어의 공유가 허용되면, 그것은 부분적인 용어를 공유 할 수있게된다 (\z.z) [](다만 함수가 아니다 \z.z, 그러나 “기능이 \z.z적용 ) 만에 한 단계로 평가합니다 뭔가 이 인수가 무엇이든. 따라서 하나의 노드 만 두 응용 프로그램을 나타내는 그래프를 가질 수 있습니다.\z.z이 두 가지 응용을 단 한 단계만으로 줄일 수 있습니다. “첫 번째 발생”의 인수는 정확히 “두 번째 발생”이므로이 노드에는주기가 있습니다. 마지막으로 최적의 공유 기능을 사용하면 베타 축소의 한 단계 (일부 부기)로 \x. (\z.z) ((\z.z) x))결과를 ( 그래프를 나타내는 그래프에서) (그래프를 나타내는 그래프로) 이동할 수 있습니다 \x.x. 이것은 기본적으로 최적의 평가 기에서 발생하는 것입니다 (그래프 표현도 공간 폭발을 방지합니다).

약간 확장 된 설명은 약한 최적화와 공유의 의미 라는 종이를 볼 수 있습니다 (관심있는 부분은 소개와 섹션 4.1 및 끝 부분에있는 참고 문헌입니다).

예를 들어서, 교회 정수에서 작동하는 산술 함수의 코딩은 최적의 평가자가 주류 언어보다 더 잘 수행 할 수있는 예제의 “잘 알려진”광산 중 하나입니다 (이 문장에서 잘 알려진 사실은 소수의 전문가는 이러한 예를 알고 있습니다). 더 많은 예제를 보려면 Asperti와 Chroboczek의 ‘ Safe Operators : Brackets Closed Forever’ 를 참조하십시오 (그리고 여기서는 EAL 유형이 아닌 흥미로운 람다 용어를 찾을 수 있습니다). 이 Asperti / Chroboczek 용지로 시작하는 oracles를 살펴보십시오).

당신이 말했듯이, 이런 종류의 인코딩은 실제로는 실용적이지 않지만 여전히 무슨 일이 일어나고 있는지 이해하는 좋은 방법을 나타냅니다. 그리고 더 심도있는 조사로 결론을 내릴 것입니다. 이러한 잘못된 인코딩에 대한 최적의 평가가 실제로 합리적인 데이터 표현에 대한 전통적인 평가와 동등한 예를 찾을 수 있습니까? (내가 아는 한 이것은 실제 공개 질문입니다).


답변

이것은 성가신 것이 아니지만 어디에서 찾아 볼 수 있는지에 대한 제안입니다.

작은 공간에서, 특히 다시 작성하여 모듈 식 지수를 계산하는 간단한 방법이 있습니다.

(a * x ^ y) % z

같이

(((a * x) % z) * x ^ (y - 1)) % z

평가자가 이와 같이 평가하고 누적 매개 변수 a를 일반 형식으로 유지하면 너무 많은 공간을 사용하지 않아도됩니다. 실제로 평가자 최적이라면 아마도이 작업보다 더 많은 작업을 수행해서는 안되므로, 특히이 작업을 평가하는 데 걸리는 시간보다 더 많은 공간을 사용할 수 없습니다.

최적의 평가자가 실제로 무엇인지 확실하지 않으므로 더 엄격하게 만들 수 없습니다.


답변