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

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

---

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

(\ 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.(b(λcd.(c(λe.(d(λfg.(f(efg)))e))))(λc.(c(λde.e)))(λc.(a(b(λdef.(d(λg.(egf))))(λd.d)(λde.(ed)))(b(λde.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)

If your sharing is restricted to complete subterms as it is the case in Haskell, you may have only one occurrence of \z.z, but the two beta-redexes here will be distinct: one is (\z.z) x and the other one is (\z.z) ((\z.z) x), and since they are not equal terms they cannot be shared. If the sharing of partial subterms is allowed, then it becomes possible to share the partial term (\z.z) [] (that is not just the function \z.z, but "the function \z.z applied to something), which evaluates in one step to just something, whatever this argument is. Hence you can have a graph in which only one node represents the two applications of \z.z to two distinct arguments, and in which these two applications can be reduced in just one step. Remark that there is a cycle on this node, since the argument of the "first occurrence" is precisely the "second occurrence". Finally, with optimal sharing you can go from (a graph representing) \x. (\z.z) ((\z.z) x)) to (a graph representing) the result \x.x in just one step of beta-reduction (plus some bookkeeping). This is basically what happens in your optimal evaluator (and the graph representation is also what prevents space explosion).

For slightly extended explanations, you can look at the paper Weak Optimality, and the Meaning of Sharing (what you are interested in is the introduction and the section 4.1, and maybe some of the bibliographic pointers at the end).

Coming back at your example, the coding of arithmetic functions working on Church integers is one of the "well-known" mines of examples where optimal evaluators can perform better than mainstream languages (in this sentence, well-known actually means that a handful of specialists are aware of these examples). For more such examples, take a look at the paper Safe Operators: Brackets Closed Forever by Asperti and Chroboczek (and by the way, you will find here interesting lambda-terms that are not EAL-typeable; so I’m encouraging you to take a look at oracles, starting with this Asperti/Chroboczek paper).

As you said yourself, this kind of encoding is utterly unpractical, but they still represent a nice way of understanding what is going on. And let me conclude with a challenge for further investigation: will you be able to find an example on which optimal evaluation on these supposedly bad encodings is actually on par with traditional evaluation on a reasonable data representation? (as far as I know this is a real open question).

---

This isn't an anwser but it's a suggestion of where you might start looking.

There's a trivial way to calculate modular exponentiations in little space, specifically by rewriting

(a * x ^ y) % z

as

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

If an evaluator evaluates like this and keeps the accumulating parameter a in normal form then you will avoid using too much space. If indeed your evaluator is optimal then presumably it must not do any more work than this one, so in particular can't use more space than the time this one takes to evaluate.

I'm not really sure what an optimal evaluator really is so I'm afraid I can't make this more rigorous.

참고URL : https://stackoverflow.com/questions/31707614/why-are-%ce%bb-calculus-optimal-evaluators-able-to-compute-big-modular-exponentiation