Reasoning about Redundant Patterns.
Delia Kesner · 1997
The extensional version of the simply typed -calculus with product types enriched with layered, wildcard, and product patterns is studied. Extensionality is expressed by the surjective pairing axiom and a generalization of the j-conversion to patterns. Two different confluent reduction systems, called lwp \\Gamma! and lw \\Gamma! respectively, are obtained by turning the extensional axioms as expansion rules, and then adding some restrictions to these expansions to avoid reduction loops. It is shown that only layered and wildcard patterns are redundant in lw \\Gamma!, while product patterns are unnecessary in lwp \\Gamma!. Confluence of both reduction systems is proven by the composition of modular properties of the systems' extensional and nonextensional parts. Recursion is also added to both systems by keeping the modularity of the confluence property.