We begin a new chapter where we will study the foundations of programming
languages. -calculus is the core of languages like ML,
Lisp etc. We study
-Calculus in the context of the
mathematics in Chapter 2 - the theory of inductive definitions.
.
With this defintion we get the induction principle for free. We ``compute'' on this type using primitive recursive function defintions.
To understand the intuitive semantics of -terms, we
represent them using mnemonics.
u is a variable
application of function f
to argument a
-abstraction with variable
v and body b
Note that ``-term'' refers to all the above three.