Next: Properties of LT
Up: classnote 14
Previous: Plan
We obtain a surface syntax for
lambda terms
by defining
constructor
names:
creates an application while 
creates
an abstraction. Although constructor names are arbitrary,
it is important to choose good mnemonic names.
We also need
discriminators
for determining the kind of 
-terms:
In addition, given a -term, we would like to be able to take it
apart. This is accomplished by providing destructors. Consider
the destructor 
, which returns the function part of an application.
Intuitively,
It is easily verified that 
.
As defined, is not a total function on 
. We can extend
to a total function 
in one of two ways. One approach is to
make return an arbitrary result when given a -term which
is not an application:
Alternatively, we can raise an exception for invalid inputs:
However, this requires that we extend the lambda calculus to 
.
Besides , there are three other destructors that are of use:
It is easily verified that:
