8 - Function Definitions and Values

Summary

In the language ℒ{num str} we may perform calculations such as the doubling of a given expression, but we cannot express doubling as a concept in itself. To capture the general pattern of doubling, we abstract away from the particular number being doubled by using a variable to stand for a fixed, but unspecified, number to express the doubling of an arbitrary number. Any particular instance of doublingmay then be obtained by substituting a numeric expression for that variable. In general an expression may involve many distinct variables, necessitating that we specify which of several possible variables is varying in a particular context, giving rise to a function of that variable.

In this chapter we consider two extensions of ℒ{num str} with functions. The first, and perhaps most obvious, extension is by adding function definitions to the language. A function is defined by binding a name to an abt with a bound variable that serves as the argument of that function. A function is applied by substituting a particular expression (of suitable type) for the bound variable, obtaining an expression.

The domain and range of defined functions are limited to the types nat and str, as these are the only types of expression. Such functions are called first-order functions, in contrast to higher-order functions, which permit functions as arguments and results of other functions. Because the domain and range of a function are types, this requires that we introduce function types whose elements are functions.