Reasoning about redundant patterns. (English) Zbl 0924.68047

Summary: The extensional version of the simply typed lambda-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 eta-conversion to patterns. Two different confluent reduction systems, called lwp and lw 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, while product patterns are unnecessary in lwp. 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.


68N17 Logic programming
Full Text: Link