Lambda calculus
Let expressions are related to Lambda calculus. Lambda calculus has a simple syntax and semantics, and is good for describing Lambda lifting. It is convenient to describe lambda lifting as a translations from "lambda" to a "let" expression, and lambda dropping as the reverse. This is because "let" expressions allow mutual recursion, which is, in a sense, more lifted than is supported in lambda calculus. Lambda calculus does not support mutual recursion and only one function may be defined at the outermost global scope.