Skip to content

Instantly share code, notes, and snippets.

@pedrofurla
Created November 10, 2016 13:01
Show Gist options
  • Save pedrofurla/481f2811faed8a728c3f3cc46eb80c4b to your computer and use it in GitHub Desktop.
Save pedrofurla/481f2811faed8a728c3f3cc46eb80c4b to your computer and use it in GitHub Desktop.
Some silly lambda calculus
+1 \n.\f.\z.f (n f z)
+2 \n.\f.\z.f (f (n f z))
1 = \f.\z.f z
2 = \f.\z.f ( f z )
+ == \n\m\f\z. n f ( m f z )
+ 1 1 == \f\z. (\f\z.f z) f ( f z )
== \f\z. (\f\z. )
== \f\z. f ( f z )
X*3 == X + X + X
== (\n\m\f\z. n f ( m f z )) ((\n\m\f\z. n f ( m f z )) X X) X
== (\n\m\f\z. n f ( m f z )) X ((\n\m\f\z. n f ( m f z )) X X)
== sum X (sum X X)
== sum X (sum X (sum X Z))
== sum (sum X X) X
== sum (sum (sum X X) X) Z
f $ f $ f z
times == \n\m\f\z. n (\m'\f\z. m f (m' f z)) f
\z.(+2) ((+2) z)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment