Abstract:A long time ago, I read an article about lambda calculus. It said this calculus is invented for reconstructing the system of mathematics. I was interested in the idea ``reconstructing the mathematical system.'' What does that mean? There are many lambda calculus introduction including Wikipedia. But, some of the procedure is hard to understand for me. Here is a memo about that. --- From the author's document