Skip to content

Instantly share code, notes, and snippets.

@bleis-tift
Created May 8, 2019 01:04
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bleis-tift/632c2163088ca7ed459a1acb39973174 to your computer and use it in GitHub Desktop.
Save bleis-tift/632c2163088ca7ed459a1acb39973174 to your computer and use it in GitHub Desktop.
[|(λv.λv2.v2) ((λv.v v) (λv.v v))|]
1. app2 -> λk1.[|λv.λv2.v2|] (λf1.[|(λv.v v) (λv.v v)|] (λa1.f1 a1 k1))
2. lam -> λk1.(λk2.k2 (λv.[|λv2.v2|])) (λf1.[|(λv.v v) (λv.v v)|] (λa1.f1 a1 k1))
3. lam -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.[|v2|])))) (λf1.[|(λv.v v) (λv.v v)|] (λa1.f1 a1 k1))
4. val -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.[|(λv.v v) (λv.v v)|] (λa1.f1 a1 k1))
5. app2 -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.[|λv.v v|] (λf5.[|λv.v v|] (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
6. lam -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.[|v v|])) (λf5.[|λv.v v|] (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
7. app2 -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.[|v|] (λf7.[|v|] (λa7.f7 a7 k7))))) (λf5.[|λv.v v|] (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
8. val -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.(λk8.k8 v) (λf7.[|v|] (λa7.f7 a7 k7))))) (λf5.[|λv.v v|] (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
9. val -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.(λk8.k8 v) (λf7.(λk9.k9 v) (λa7.f7 a7 k7))))) (λf5.[|λv.v v|] (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
10.lam -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.(λk8.k8 v) (λf7.(λk9.k9 v) (λa7.f7 a7 k7))))) (λf5.(λk10.k10 (λv.[|v v|])) (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
11.app2 -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.(λk8.k8 v) (λf7.(λk9.k9 v) (λa7.f7 a7 k7))))) (λf5.(λk10.k10 (λv.(λk11.[|v|] (λf11.[|v|] (λa11.f11 a11 k11))))) (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
12.val -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.(λk8.k8 v) (λf7.(λk9.k9 v) (λa7.f7 a7 k7))))) (λf5.(λk10.k10 (λv.(λk11.(λk12.k12 v) (λf11.[|v|] (λa11.f11 a11 k11))))) (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
13.val -> λk1.(λk2.k2 (λv.(λk3.k3 (λv2.(λk4.k4 v2))))) (λf1.(λk5.(λk6.k6 (λv.(λk7.(λk8.k8 v) (λf7.(λk9.k9 v) (λa7.f7 a7 k7))))) (λf5.(λk10.k10 (λv.(λk11.(λk12.k12 v) (λf11.(λk13.k13 v) (λa11.f11 a11 k11))))) (λa5.f5 a5 k5))) (λa1.f1 a1 k1))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment