Computations over λ-terms
In Chapter 1 we observed that first-order terms can be used as data structures to represent a variety of symbolic objects. The higher-order language developed in Chapter 5 allows λ-abstraction to be used to build terms of higher-order type. We discussed briefly in that chapter how such terms can be used to encode data structures containing bindings, such as functional difference lists. We now explore in greater detail the uses of λ-terms in encoding data objects that contain bindings and show that the hohh language provides elegant and declarative means for describing a range of computations over such representations.
There are many commonly used mathematical expressions ...