Lambda-calculus with patterns

Abstract

The original lambed-calculus can be used to represent a function, via a lambda-term, and to interpret the result of applying a function to an argument. However, there are some functions which cannot be represented by lambda-terms. By adding patterns, which will be used to specify the form of the argument accepted, and to extract subterms of the argument, and by modifying the definition of terms to allow a kind of "definition by cases" we can construct a new lambda-calculus. This new lambda-calculus can describe a larger class of functions, yet still satisfies all the basic properties of the original lambda-calculus, including the Church-Rosser theorem.