In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. It was introduced by Alonzo Church in the 1930s as part of an investigation into the foundations of mathematics.