A Brief Introduction to the Lambda Calculus

Por • 19 sep, 2018 • Sección: Ambiente

Stuart A. Kurtz

Introduction When you first learned about functions, they were most likely introduced as abstractions of expressions. For example, consider the expression 2 + 3, which can be immediately evaluated by the rules of elementary arithmetic to give value 5. We can abstract, i.e., generalize the notion of “adding 3 to 2” to that of “adding 3 to something,” giving rise the function f : x 7→ x + 3. We can then apply this function to other arguments, e.g., f(4) = 4 + 3 = 7. This style of function definition is intentional—functions are defined by specifying an intended means of evaluation. Later, you may have been encouraged to think of functions extensionally, i.e., as sets of ordered pairs, e.g. f = {(x, y) : y = x + 3}. Such an approach conveys substantial metamathematical advantages, but it comes at a terrible cost—functions are no longer things that you can compute with. The lambda calculus [Chu41] returns to the notion of functions as abstractions of expressions. Abstraction is accomplished by the eponymous lambda (λ), by means of which we could define the function f as λx. x + 3. An abstraction may be applied to an argument,


Post to Twitter

Escribe un comentario