Reasoning about Layered, Wildcard and Product Patterns

We study the extensional version of the simply typed -calculus with product types and fixpoints enriched with layered, wildcard and product patterns. Extensionality is expressed by the surjective pairing axiom and a generalization of the j-conversion to patterns. We obtain a confluent reduction system by turning the extensional axioms as expansion rules, and then adding some restrictions to these expansions in order to avoid reduction loops. Confluence is proved by composition of modular properties of the extensional and non-extensional subsystems of the reduction calculus. 1 Introduction Pattern-matching function definitions is one of the most popular features of functional languages, allowing to specify the behavior of functions by cases, according to the form of their arguments. Left-hand sides of function definitions are usually expressed using Layered, Wildcard and Product Patterns (LWPP), as for example the following Caml Light [ea93] program where the function cons new pair ta..