JFLP: Volume 1997, Article 4

The Journal of Functional and Logic Programming

Volume 1997

Article 4

Published by The MIT Press . Copyright 1997 Massachusetts Institute of Technology.

Your institution may already be a subscriber to JFLP. If not, please subscribe for legitimate access to all journal articles.

Reasoning about Redundant Patterns

Delia Kesner

13 June 1997

Abstract

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.

The following versions of the article are available:

• Preformatted versions of the article (compressed with gzip )
  • DVI (gzip'ped 60 kb)
  • PostScript (gzip'ped 118 kb)
• Source materials for custom formatting
  • LaTeX ( JFLP-A97-04.tex , gzip'ped 30 kb)
  • BIBTeX ( JFLP-A97-04.bib , gzip'ped 3 kb)
  • Parameter settings for custom formatting ( cjropts.tex , 117 bytes)

You can find this article also on the ftp-server of The MIT Press (access may be faster from some sites).

Self citation

    @article{jflp97-04,
      author={Delia Kesner},
      title={Reasoning about Redundant Patterns},
      journal={Journal of Functional and Logic Programming},
      volume={1997},
      number={4},
      publisher={The MIT Press},
      month={June},
      year={1997}
    }

Main page