1993.

Paper abstract bibtex

Paper abstract bibtex

We consider the simply typed $łambda$-calculus with primitive recursion operators and types corresponding to categorical products and coproducts. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence.

@conference{ c_rta93, author = {Daniel J.\ Dougherty}, title = {Some lambda calculi with categorical sums and products}, pages = {137--151}, isbn = {3-540-56868-9}, editor = {Claude Kirchner}, booktitle = {Proc.\ 5th International Conference on Rewriting Techniques and Applications ({RTA})}, series = {Lecture Notes in Computer Science}, volume = {690}, publisher = {Springer-Verlag}, address = {Berlin}, year = {1993}, abstract = { We consider the simply typed $łambda$-calculus with primitive recursion operators and types corresponding to categorical products and coproducts. The standard equations corresponding to extensionality and to surjectivity of pairing and its dual are oriented as expansion rules. Strong normalization and ground (base-type) confluence is proved for the full calculus; full confluence is proved for the calculus omitting the rule for strong sums. In the latter case, fixed-point constructors may be added while retaining confluence. }, url = {rta93.pdf} }

Downloads: 0