- The lambda in lambda calculus is the greek letter λ used to introduce, or abstract, arguments for binding in an expression.
- A lambda abstraction is an anonymous function or lambda term. (λx.x + 1) The head of the expression, λx., abstracts out the term x + 1. We can apply it to any x and recompute different results for each x we applied the lambda to.
- Application is how one evaluates or reduces lambdas, this binds the argument to whatever the lambda was applied to. Computations are performed in lambda calculus by applying lambdas to arguments until you run out of arguments to apply lambdas to. (λx.x)1 This example reduces to 1, the identity λx.x was applied to the value 1, x was bound to 1, and the lambda's body is x, so it just kicks the 1 out. In a sense, applying the λx.x consumed it. We reduced the amount of structure we had.
- Lambda calculus is a formal system for expressing programs in terms of abstraction and application.
- Normal order is a commmon evaluation strategy in lambda calculi. Normal order means evaluating (ie, applying or beta reducing) the leftmost outermost labdas first, evaluating terms nested within after you've run out of arguments to apply. Normal order isn't how Haskell code is evaluated. It's call-by-need instead.