epicmonkey (epicmonkey) wrote,
epicmonkey
epicmonkey

Beta reduction

Внезапно, оказалось, что 500Мб недостаточно, чтобы записать всю последовательность вычислений для наибольшего общего делителя четырёх и шести. Так что ниже простое сравнение по обычному порядку.

(((λx. (λy. ((λn. ((n (λx. (λx. (λy. y)))) (λx. (λy. x)))) (((λm. (λn.
((n (λn. (λf. (λx. (((n (λg. (λh. (h (g f))))) (λp. x)) (λp. p))))))
m))) x) y)))) (λf. (λx. (f (f (f (f x))))))) (λf. (λx. (f (f
x)))))

((λx1. ((λx2. ((x2 (λx3. (λx4. (λx5. x5)))) (λx3. (λx4. x3)))) (((λx2.
(λx3. ((x3 (λx4. (λx5. (λx6. (((x4 (λx7. (λx8. (x8 (x7 x5))))) (λx7.
x6)) (λx7. x7)))))) x2))) (λx2. (λx3. (x2 (x2 (x2 (x2 x3))))))) x1)))
(λf. (λx. (f (f x)))))

((λx2. ((x2 (λx3. (λx4. (λx5. x5)))) (λx3. (λx4. x3)))) (((λx2. (λx3.
((x3 (λx4. (λx5. (λx6. (((x4 (λx7. (λx8. (x8 (x7 x5))))) (λx7. x6))
(λx7. x7)))))) x2))) (λx2. (λx3. (x2 (x2 (x2 (x2 x3))))))) (λx2. (λx3.
(x2 (x2 x3))))))

(((((λx1. (λx3. ((x3 (λx4. (λx5. (λx6. (((x4 (λx7. (λx8. (x8 (x7
x5))))) (λx7. x6)) (λx7. x7)))))) x1))) (λx1. (λx3. (x1 (x1 (x1 (x1
x3))))))) (λx1. (λx3. (x1 (x1 x3))))) (λx1. (λx3. (λx4. x4)))) (λx1.
(λx3. x1)))

((((λx2. ((x2 (λx3. (λx4. (λx5. (((x3 (λx6. (λx7. (x7 (x6 x4)))))
(λx6. x5)) (λx6. x6)))))) (λx3. (λx4. (x3 (x3 (x3 (x3 x4)))))))) (λx1.
(λx3. (x1 (x1 x3))))) (λx1. (λx3. (λx4. x4)))) (λx1. (λx3. x1)))

(((((λx1. (λx3. (x1 (x1 x3)))) (λx1. (λx3. (λx4. (((x1 (λx5. (λx6. (x6
(x5 x3))))) (λx5. x4)) (λx5. x5)))))) (λx1. (λx3. (x1 (x1 (x1 (x1
x3))))))) (λx1. (λx3. (λx4. x4)))) (λx1. (λx3. x1)))

((((λx2. ((λx3. (λx4. (λx5. (((x3 (λx6. (λx7. (x7 (x6 x4))))) (λx6.
x5)) (λx6. x6))))) ((λx3. (λx4. (λx5. (((x3 (λx6. (λx7. (x7 (x6
x4))))) (λx6. x5)) (λx6. x6))))) x2))) (λx1. (λx3. (x1 (x1 (x1 (x1
x3))))))) (λx1. (λx3. (λx4. x4)))) (λx1. (λx3. x1)))

((((λx1. (λx3. (λx4. (((x1 (λx5. (λx6. (x6 (x5 x3))))) (λx5. x4))
(λx5. x5))))) ((λx1. (λx3. (λx4. (((x1 (λx5. (λx6. (x6 (x5 x3)))))
(λx5. x4)) (λx5. x5))))) (λx1. (λx3. (x1 (x1 (x1 (x1 x3)))))))) (λx1.
(λx3. (λx4. x4)))) (λx1. (λx3. x1)))

(((λx2. (λx3. (((((λx4. (λx5. (λx6. (((x4 (λx7. (λx8. (x8 (x7 x5)))))
(λx7. x6)) (λx7. x7))))) (λx4. (λx5. (x4 (x4 (x4 (x4 x5))))))) (λx4.
(λx5. (x5 (x4 x2))))) (λx4. x3)) (λx4. x4)))) (λx1. (λx3. (λx4. x4))))
(λx1. (λx3. x1)))

((λx1. (((((λx3. (λx4. (λx5. (((x3 (λx6. (λx7. (x7 (x6 x4))))) (λx6.
x5)) (λx6. x6))))) (λx3. (λx4. (x3 (x3 (x3 (x3 x4))))))) (λx3. (λx4.
(x4 (x3 (λx5. (λx6. (λx7. x7)))))))) (λx3. x1)) (λx3. x3))) (λx1.
(λx3. x1)))

(((((λx2. (λx3. (λx4. (((x2 (λx5. (λx6. (x6 (x5 x3))))) (λx5. x4))
(λx5. x5))))) (λx2. (λx3. (x2 (x2 (x2 (x2 x3))))))) (λx2. (λx3. (x3
(x2 (λx4. (λx5. (λx6. x6)))))))) (λx2. (λx3. (λx4. x3)))) (λx2. x2))

((((λx1. (λx3. ((((λx4. (λx5. (x4 (x4 (x4 (x4 x5)))))) (λx4. (λx5. (x5
(x4 x1))))) (λx4. x3)) (λx4. x4)))) (λx2. (λx3. (x3 (x2 (λx4. (λx5.
(λx6. x6)))))))) (λx2. (λx3. (λx4. x3)))) (λx2. x2))

(((λx2. ((((λx3. (λx4. (x3 (x3 (x3 (x3 x4)))))) (λx3. (λx4. (x4 (x3
(λx5. (λx6. (x6 (x5 (λx7. (λx8. (λx9. x9)))))))))))) (λx3. x2)) (λx3.
x3))) (λx2. (λx3. (λx4. x3)))) (λx2. x2))

(((((λx1. (λx3. (x1 (x1 (x1 (x1 x3)))))) (λx1. (λx3. (x3 (x1 (λx4.
(λx5. (x5 (x4 (λx6. (λx7. (λx8. x8)))))))))))) (λx1. (λx3. (λx4. (λx5.
x4))))) (λx1. x1)) (λx2. x2))

((((λx2. ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8. (λx9.
x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8.
(λx9. x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7.
(λx8. (λx9. x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5
(λx7. (λx8. (λx9. x9))))))))))) x2))))) (λx1. (λx3. (λx4. (λx5.
x4))))) (λx1. x1)) (λx2. x2))

((((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6. (λx7. (λx8.
x8))))))))))) ((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6. (λx7.
(λx8. x8))))))))))) ((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6.
(λx7. (λx8. x8))))))))))) ((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4
(λx6. (λx7. (λx8. x8))))))))))) (λx1. (λx3. (λx4. (λx5. x4))))))))
(λx1. x1)) (λx2. x2))

(((λx2. (x2 (((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8.
(λx9. x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7.
(λx8. (λx9. x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5
(λx7. (λx8. (λx9. x9))))))))))) (λx3. (λx4. (λx5. (λx6. x5)))))))
(λx3. (λx4. (x4 (x3 (λx5. (λx6. (λx7. x7)))))))))) (λx1. x1)) (λx2.
x2))

(((λx1. x1) (((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6. (λx7.
(λx8. x8))))))))))) ((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6.
(λx7. (λx8. x8))))))))))) ((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4
(λx6. (λx7. (λx8. x8))))))))))) (λx1. (λx3. (λx4. (λx5. x4)))))))
(λx1. (λx3. (x3 (x1 (λx4. (λx5. (λx6. x6))))))))) (λx2. x2))

((((λx2. (λx3. (x3 (x2 (λx4. (λx5. (x5 (x4 (λx6. (λx7. (λx8.
x8))))))))))) ((λx2. (λx3. (x3 (x2 (λx4. (λx5. (x5 (x4 (λx6. (λx7.
(λx8. x8))))))))))) ((λx2. (λx3. (x3 (x2 (λx4. (λx5. (x5 (x4 (λx6.
(λx7. (λx8. x8))))))))))) (λx2. (λx3. (λx4. (λx5. x4))))))) (λx2.
(λx3. (x3 (x2 (λx4. (λx5. (λx6. x6)))))))) (λx2. x2))

(((λx1. (x1 (((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8.
(λx9. x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7.
(λx8. (λx9. x9))))))))))) (λx3. (λx4. (λx5. (λx6. x5)))))) (λx3. (λx4.
(x4 (x3 (λx5. (λx6. (λx7. x7)))))))))) (λx2. (λx3. (x3 (x2 (λx4. (λx5.
(λx6. x6)))))))) (λx2. x2))

(((λx2. (λx3. (x3 (x2 (λx4. (λx5. (λx6. x6))))))) (((λx2. (λx3. (x3
(x2 (λx4. (λx5. (x5 (x4 (λx6. (λx7. (λx8. x8))))))))))) ((λx2. (λx3.
(x3 (x2 (λx4. (λx5. (x5 (x4 (λx6. (λx7. (λx8. x8))))))))))) (λx2.
(λx3. (λx4. (λx5. x4)))))) (λx2. (λx3. (x3 (x2 (λx4. (λx5. (λx6.
x6))))))))) (λx2. x2))

((λx1. (x1 ((((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8.
(λx9. x9))))))))))) ((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7.
(λx8. (λx9. x9))))))))))) (λx3. (λx4. (λx5. (λx6. x5)))))) (λx3. (λx4.
(x4 (x3 (λx5. (λx6. (λx7. x7)))))))) (λx3. (λx4. (λx5. x5)))))) (λx2.
x2))

((λx2. x2) ((((λx2. (λx3. (x3 (x2 (λx4. (λx5. (x5 (x4 (λx6. (λx7.
(λx8. x8))))))))))) ((λx2. (λx3. (x3 (x2 (λx4. (λx5. (x5 (x4 (λx6.
(λx7. (λx8. x8))))))))))) (λx2. (λx3. (λx4. (λx5. x4)))))) (λx2. (λx3.
(x3 (x2 (λx4. (λx5. (λx6. x6)))))))) (λx2. (λx3. (λx4. x4)))))

((((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6. (λx7. (λx8.
x8))))))))))) ((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4 (λx6. (λx7.
(λx8. x8))))))))))) (λx1. (λx3. (λx4. (λx5. x4)))))) (λx1. (λx3. (x3
(x1 (λx4. (λx5. (λx6. x6)))))))) (λx1. (λx3. (λx4. x4))))

(((λx2. (x2 (((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8.
(λx9. x9))))))))))) (λx3. (λx4. (λx5. (λx6. x5))))) (λx3. (λx4. (x4
(x3 (λx5. (λx6. (λx7. x7)))))))))) (λx1. (λx3. (x3 (x1 (λx4. (λx5.
(λx6. x6)))))))) (λx1. (λx3. (λx4. x4))))

(((λx1. (λx3. (x3 (x1 (λx4. (λx5. (λx6. x6))))))) (((λx1. (λx3. (x3
(x1 (λx4. (λx5. (x5 (x4 (λx6. (λx7. (λx8. x8))))))))))) (λx1. (λx3.
(λx4. (λx5. x4))))) (λx1. (λx3. (x3 (x1 (λx4. (λx5. (λx6. x6)))))))))
(λx1. (λx3. (λx4. x4))))

((λx2. (x2 ((((λx3. (λx4. (x4 (x3 (λx5. (λx6. (x6 (x5 (λx7. (λx8.
(λx9. x9))))))))))) (λx3. (λx4. (λx5. (λx6. x5))))) (λx3. (λx4. (x4
(x3 (λx5. (λx6. (λx7. x7)))))))) (λx3. (λx4. (λx5. x5)))))) (λx1.
(λx3. (λx4. x4))))

((λx1. (λx3. (λx4. x4))) ((((λx1. (λx3. (x3 (x1 (λx4. (λx5. (x5 (x4
(λx6. (λx7. (λx8. x8))))))))))) (λx1. (λx3. (λx4. (λx5. x4))))) (λx1.
(λx3. (x3 (x1 (λx4. (λx5. (λx6. x6)))))))) (λx1. (λx3. (λx4. x4)))))

(λx3. (λx4. x4))
Tags: lambda, theneverendingstory
Subscribe

  • Quicksort and lambda calculus

    Quicksort and lambda calculus. (define quicksort (lambda (l) ((Z (lambda (rec) (lambda (l) (((if (null l)) nil) ((lambda (p) ((lambda (xs)…

  • Basic lambda calculus

    Functions are "first class citizens" (Cristopher Strachey, mid-1960s). ; DISCLAIMER: THE DRAFT BELOW IS NOT INTENDED TO BE THE PURE LAMBDA…

  • Ultimate Guide Bricking a Karotz

    Ultimate guide bricking a Karotz WARNING: DON’T TRY THIS AT HOME UNLESS YOU UNDERSTAND EXACTLY WHAT YOU ARE DOING. SHUT UP AND…

  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments