In mathematical logic, the lambda calculus (also written as ?-calculus') is a formal system for expressing computation based on function abstraction and application using variable binding and substitution. Untyped