About
When it comes to reasoning about programs, you may have heard of alpha and beta equivalence and possibly even eta equivalence, but you probably never heard of lambda equivalence and you won't find it with Google Search.
To learn about this exciting new technique please join us as the illustrious Jay Sulzberger presents Lambda Equivalence for the very first time!
Meta Abstract
"On FizzBuzz, including an Introduction to the Dream of Homotopy Type Theory"
or
"On the Several Differences between Lisp and the Lambda Calculus"
or
"The Paradigm Case of Curry-Howard [that is, for the Simply Typed Lambda Calculus] Helps Tell When Two Proofs of a Given Proposition are Really The Same."
References
When are two proofs the same?:
http://mathoverflow.net/questions/3776/when-are-two-proofs-of-the-same-theorem-really-different-proofs
http://math.stackexchange.com/questions/1242043/when-are-two-proofs-the-same
https://gowers.wordpress.com/2007/10/04/when-are-two-proofs-essentially-the-same/
https://homotopytypetheory.org/
https://homotopytypetheory.org/2016/09/26/hottsql-proving-query-rewrites-with-univalent-sql-semantics/
https://en.wikipedia.org/wiki/Cryptomorphism
Gian-Carlo Rota's note on Alonzo Church:
https://www.princeton.edu/mudd/finding_aids/mathoral/pmcxrota.htm
Physics, Topology, Logic and Computation: A Rosetta Stone by John C. Baez and Mike Stay:
https://arxiv.org/abs/0903.0340
Lectures on the Curry-Howard Isomorphism, May 1998 not final version by M. H. B. Sorenson and P. Urzyczyn:
<a>ftp://ftp.cs.cmu.edu/user/ftp/user/rwh/www/home/course/logic/www-old/handouts\</a> /curry-howard.pdf
Tom Stuart's delightful "Programming with Nothing": http://codon.com/programming-with-nothing
J. R. Hindley's 1997 book Basic Simple Type Theory:
https://mathtrielhighschool.files.wordpress.com/2011/08/number-theory.pdf
On FizzBuzz:
https://en.wikipedia.org/wiki/Fizz_buzzFizz
https://www.rosettacode.org/wiki/FizzBuzz
Bio
Jay Sulzberger has an honorary PhD in Mathematics from the Hogwarts School of Witchcraft and Wizardry where he now serves as a board member. He worked at the the IBM Research Center for countless decades. He has been the resident Mathematician at Lisp NYC since 2002. His brilliance and wisdom are infinitely unenumerable. His favorite theorem is Bell's Theorem. He has proven on numerous occasions, using no more than three napkins, that Haskell is a lie.
Comments
