Skip to content
Tuber
imo

Tuber

An interpreter that evaluates λ-calculations step by step.
Play in Browser GitHub

これは何？

Tuber は型無しラムダ計算をステップごとに簡約するインタプリタです。
Tuber は Rust で実装されたライブラリであり、Web ブラウザから実行可能なインターフェースとして skiMogul があります。

型無しラムダ計算はチューリング完全であることが知られています。
例えば Tuber を使って 2 + 3 == 5 → true を確かめると以下のようなステップが表示されます。

EQ(ADD(2, 3), 5)

skiMogulで実行

 
EQ(ADD(2, 3), 5)
→ AND(GTE(ADD(2, 3), 5), LTE(ADD(2, 3), 5))
→ GTE(ADD(2, 3), 5, LTE(ADD(2, 3), 5), FALSE)
→ IS_ZERO(SUB(5, ADD(2, 3)), LTE(ADD(2, 3), 5), FALSE)
→ SUB(5, ADD(2, 3), _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ ADD(2, 3, PRED, 5, _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => 2(f, 3(f, x)))(PRED, 5, _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ (x => 2(PRED, 3(PRED, x)))(5, _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ 2(PRED, 3(PRED, 5), _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => f(f(x)))(PRED, 3(PRED, 5), _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ (x => PRED(PRED(x)))(3(PRED, 5), _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ PRED(PRED(3(PRED, 5)), _ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => PRED(3(PRED, 5), (g, h) => h(g(f)), u => x, u => u))(_ => FALSE, TRUE, LTE(ADD(2, 3), 5), FALSE)
→ (x => PRED(3(PRED, 5), (g, h) => h(g(_ => FALSE)), u => x, u => u))(TRUE, LTE(ADD(2, 3), 5), FALSE)
→ PRED(3(PRED, 5), (g, h) => h(g(_ => FALSE)), u => TRUE, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => 3(PRED, 5, (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g(_ => FALSE)), u => TRUE, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (x => 3(PRED, 5, (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => x, u => u))(u => TRUE, u => u, LTE(ADD(2, 3), 5), FALSE)
→ 3(PRED, 5, (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => f(f(f(x))))(PRED, 5, (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (x => PRED(PRED(PRED(x))))(5, (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ PRED(PRED(PRED(5)), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => PRED(PRED(5), (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (x => PRED(PRED(5), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => x, u => u))((u, u) => TRUE, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ PRED(PRED(5), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (u, u, u) => TRUE, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => PRED(5, (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (u, u, u) => TRUE, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (x => PRED(5, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), u => x, u => u))((u, u, u) => TRUE, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ PRED(5, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => 5((g, h) => h(g(f)), u => x, u => u))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (x => 5((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), u => x, u => u))((u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ 5((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((f, x) => f(f(f(f(f(x))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (x => ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(x))))))((u, u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)))), u => u, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE))), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(u => u, u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE))), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE))), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(u => u, u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(u => u, u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE))))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))))))((g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g(_ => FALSE)))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE))))), u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)))))(u => u, u => u, LTE(ADD(2, 3), 5), FALSE)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE))), u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))))))((g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g((g, h) => h(g(_ => FALSE)))))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE))))), (g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)))))((g, h) => h(g(_ => FALSE)), u => u, LTE(ADD(2, 3), 5), FALSE)
→ ((g, h) => h(g(_ => FALSE)))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE))), u => u, LTE(ADD(2, 3), 5), FALSE)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE)))(u => u, LTE(ADD(2, 3), 5), FALSE)
→ (u => u)(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE), LTE(ADD(2, 3), 5), FALSE)
→ ((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE, LTE(ADD(2, 3), 5), FALSE)
→ ((u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE, LTE(ADD(2, 3), 5), FALSE)
→ ((u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE, LTE(ADD(2, 3), 5), FALSE)
→ ((u, u) => TRUE)((g, h) => h(g(_ => FALSE)), _ => FALSE, LTE(ADD(2, 3), 5), FALSE)
→ (u => TRUE)(_ => FALSE, LTE(ADD(2, 3), 5), FALSE)
→ TRUE(LTE(ADD(2, 3), 5), FALSE)
→ ((x, y) => x)(LTE(ADD(2, 3), 5), FALSE)
→ (y => LTE(ADD(2, 3), 5))(FALSE)
→ LTE(ADD(2, 3), 5)
→ IS_ZERO(SUB(ADD(2, 3), 5))
→ SUB(ADD(2, 3), 5, _ => FALSE, TRUE)
→ 5(PRED, ADD(2, 3), _ => FALSE, TRUE)
→ ((f, x) => f(f(f(f(f(x))))))(PRED, ADD(2, 3), _ => FALSE, TRUE)
→ (x => PRED(PRED(PRED(PRED(PRED(x))))))(ADD(2, 3), _ => FALSE, TRUE)
→ PRED(PRED(PRED(PRED(PRED(ADD(2, 3))))), _ => FALSE, TRUE)
→ ((f, x) => PRED(PRED(PRED(PRED(ADD(2, 3)))), (g, h) => h(g(f)), u => x, u => u))(_ => FALSE, TRUE)
→ (x => PRED(PRED(PRED(PRED(ADD(2, 3)))), (g, h) => h(g(_ => FALSE)), u => x, u => u))(TRUE)
→ PRED(PRED(PRED(PRED(ADD(2, 3)))), (g, h) => h(g(_ => FALSE)), u => TRUE, u => u)
→ ((f, x) => PRED(PRED(PRED(ADD(2, 3))), (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g(_ => FALSE)), u => TRUE, u => u)
→ (x => PRED(PRED(PRED(ADD(2, 3))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => x, u => u))(u => TRUE, u => u)
→ PRED(PRED(PRED(ADD(2, 3))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u)
→ ((f, x) => PRED(PRED(ADD(2, 3)), (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g((g, h) => h(g(_ => FALSE)))), (u, u) => TRUE, u => u, u => u)
→ (x => PRED(PRED(ADD(2, 3)), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => x, u => u))((u, u) => TRUE, u => u, u => u)
→ PRED(PRED(ADD(2, 3)), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (u, u, u) => TRUE, u => u, u => u, u => u)
→ ((f, x) => PRED(ADD(2, 3), (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (u, u, u) => TRUE, u => u, u => u, u => u)
→ (x => PRED(ADD(2, 3), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), u => x, u => u))((u, u, u) => TRUE, u => u, u => u, u => u)
→ PRED(ADD(2, 3), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (u, u, u, u) => TRUE, u => u, u => u, u => u, u => u)
→ ((f, x) => ADD(2, 3, (g, h) => h(g(f)), u => x, u => u))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (u, u, u, u) => TRUE, u => u, u => u, u => u, u => u)
→ (x => ADD(2, 3, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), u => x, u => u))((u, u, u, u) => TRUE, u => u, u => u, u => u, u => u)
→ ADD(2, 3, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, u => u)
→ ((f, x) => 2(f, 3(f, x)))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, u => u)
→ (x => 2((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), 3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), x)))((u, u, u, u, u) => TRUE, u => u, u => u, u => u, u => u, u => u)
→ 2((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), 3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE), u => u, u => u, u => u, u => u, u => u)
→ ((f, x) => f(f(x)))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), 3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE), u => u, u => u, u => u, u => u, u => u)
→ (x => ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(x)))(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE), u => u, u => u, u => u, u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE)), u => u, u => u, u => u, u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(u => u, u => u, u => u, u => u, u => u)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), u => u, u => u, u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), u => u, u => u, u => u, u => u)
→ (h => h(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), u => u, u => u, u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), u => u, u => u, u => u, u => u)
→ (h => h(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(u => u, u => u, u => u, u => u)
→ (u => u)(3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), u => u, u => u, u => u)
→ 3((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ ((f, x) => f(f(f(x))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))), (u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ (x => ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(x))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE)), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), u => u, u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), u => u, u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(u => u, u => u, u => u)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE))))), u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE), (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))))))((g, h) => h(g((g, h) => h(g(_ => FALSE)))), u => u, u => u)
→ ((g, h) => h(g((g, h) => h(g(_ => FALSE)))))(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE))))), u => u, u => u)
→ (h => h(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)))))(u => u, u => u)
→ (u => u)(((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE))), u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((u, u, u, u, u) => TRUE, (g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))))((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u)
→ ((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE))))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))))))((g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), u => u)
→ ((g, h) => h(g((g, h) => h(g(_ => FALSE)))))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE))))), (g, h) => h(g(_ => FALSE)), u => u)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)))))((g, h) => h(g(_ => FALSE)), u => u)
→ ((g, h) => h(g(_ => FALSE)))(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE))), u => u)
→ (h => h(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE)))(u => u)
→ (u => u)(((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE))
→ ((u, u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))))), (g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE)
→ ((u, u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g((g, h) => h(g(_ => FALSE)))))), (g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE)
→ ((u, u, u) => TRUE)((g, h) => h(g((g, h) => h(g(_ => FALSE)))), (g, h) => h(g(_ => FALSE)), _ => FALSE)
→ ((u, u) => TRUE)((g, h) => h(g(_ => FALSE)), _ => FALSE)
→ (u => TRUE)(_ => FALSE)
→ TRUE

簡約の結果が TRUE になっていることがわかります。

Tuber でできること

  • ラムダ式を簡約する
  • ラムダ式に名前をつけて参照する (名前付き関数)
  • 名前付き関数を含む式をラムダ式に展開する
  • ラムダ式を ski コンビネータの組み合わせに変換する
  • ラムダ式を iota コンビネータの組み合わせに変換する

Tuber を構成する概念

  • 識別子: Identifier
  • 式: Expression
    • 変数: Variable
    • シンボル: Symbol
    • 関数適用: Application
    • ラムダ抽象: Lambda
  • 名前付き関数とコンテキスト: Function & Context
  • コマンド: Command
    • 簡約: Reduce
    • 関数定義: Define
    • 展開: Expand
    • コンテキストへの問い合わせ: Query