Skip to content

Instantly share code, notes, and snippets.

@deeglaze

deeglaze/mini-church.sch

Last active December 29, 2015 11:58
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 deeglaze/7666854 to your computer and use it in GitHub Desktop.
Save deeglaze/7666854 to your computer and use it in GitHub Desktop.
Download ZIP
Minimal language CFA problem. Unary untyped lambda calculus. Can you get this is always true?
Raw
mini-church.sch
;; 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