Lambda Calculus with Patterns


The lambda phi-calculus is an extension of the lambda-calculus with a pattern matching facility. The form of the argument of a function can be specified and hence lambda phi-calculus is more convenient than ordinary lambda-calculus. We explore the basic theory of lambda-calculus, investigating properties such as confluence. In doing so, we find some requirements for patterns that guarantee confluence. Our work can be seen as giving some foundations for implementations of functional programming languages.