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))