Skip to content

Instantly share code, notes, and snippets.

@deeglaze
Last active December 29, 2015 11:58
Show Gist options
  • Save deeglaze/7666854 to your computer and use it in GitHub Desktop.
Save deeglaze/7666854 to your computer and use it in GitHub Desktop.
Minimal language CFA problem. Unary untyped lambda calculus. Can you get this is always true?
;; multiplication distributes over addition test: (2 * (1 + 3)) = ((2 * 1) + (2 * 3))
((lambda (plus)
((lambda (mult)
((lambda (pred)
((lambda (sub)
((lambda (church0)
((lambda (church1)
((lambda (church2)
((lambda (church3)
((lambda (true)
((lambda (false)
((lambda (church0?)
((lambda (Y)
((lambda (church=?)
((church=? ((mult church2) ((plus church1) church3)))
((plus ((mult church2) church1)) ((mult church2) church3))))
(Y
(lambda (church=?)
(lambda (e1)
(lambda (e2)
(((church0? e1) ;; IF
(lambda (thendummy) (church0? e2)))
(lambda (elsedummy1)
(((church0? e2) ;; IF
false)
(lambda (elsedummy2) ((church=? ((sub e1) church1)) ((sub e2) church1))))))))))))
(lambda (yf)
((lambda (yg) (yg yg))
(lambda (yx) (yf (λ (yv) ((yx yx) yv))))))))
(lambda (z) ((z (lambda (zx) false)) true))))
(lambda (fa) (lambda (fb) (fb (lambda (bdummy) bdummy))))))
(lambda (ta) (lambda (tb) (ta (lambda (adummy) adummy))))))
(lambda (f3) (lambda (x3) (f3 (f3 (f3 x3)))))))
(lambda (f2) (lambda (x2) (f2 (f2 x2))))))
(lambda (f1) (lambda (x1) (f1 x1)))))
(lambda (f0) (lambda (x0) x0))))
(lambda (s1)
(lambda (s2)
((s2 pred) s1)))))
(lambda (n)
(lambda (rf)
(lambda (rx)
(((n (lambda (g) (lambda (h) (h (g rf)))))
(lambda (ignored) rx))
(lambda (id) id)))))))
(lambda (m1)
(lambda (m2)
(lambda (mf) (m2 (m1 mf)))))))
(lambda (p1)
(lambda (p2)
(lambda (pf)
(lambda (x) ((p1 pf) ((p2 pf) x)))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment