Adding Algebraic Rewriting to the Untyped Lambda Calculus

Adding Algebraic Rewriting to the Untyped Lambda Calculus. Dougherty, D. J.\ Information and Computation, 101(2):251--267, 1992.

Paper abstract bibtex

We investigate the system obtained by adding an algebraic rewriting system R to an untyped lambda calculus in which terms are formed using the function symbols from $R$ as constants. On certain classes of terms, called here \emphstable, we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result suggests a general method for proving confluence of typed beta-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.

@article{ a_iandc92,
  title = {Adding Algebraic Rewriting to the Untyped
                  Lambda Calculus},
  author = {Daniel J.\ Dougherty},
  pages = {251--267},
  journal = {Information and Computation},
  year = {1992},
  volume = {101},
  number = {2},
  abstract = {We investigate the system obtained by adding an
                  algebraic rewriting system R to an untyped
                  lambda calculus in which terms are formed using
                  the function symbols from $R$ as constants. On
                  certain classes of terms, called here \emph{stable},
                  we prove that the resulting calculus is
                  confluent if R is confluent, and terminating if
                  R is terminating. The termination result has
                  the corresponding theorems for several typed
                  calculi as corollaries. The proof of the
                  confluence result suggests a general method for
                  proving confluence of typed beta-reduction plus
                  rewriting; we sketch the application to the
                  polymorphic lambda calculus.},
  url = {iandc92.pdf}
}

Downloads: 0

{"_id":{"_str":"51f6934359ced8df44000e5f"},"__v":1,"authorIDs":[],"author_short":["Dougherty, D.<nbsp>J.\\"],"bibbaseid":"dougherty-addingalgebraicrewritingtotheuntypedlambdacalculus-1992","bibdata":{"html":"<div class=\"bibbase_paper\"> \n\n\n<span class=\"bibbase_paper_titleauthoryear\">\n\t<span class=\"bibbase_paper_title\"><a name=\"a_iandc92\"> </a>Adding Algebraic Rewriting to the Untyped Lambda Calculus.</span>\n\t<span class=\"bibbase_paper_author\">\nDougherty, D. J.\\</span>\n\t\n</span>\n\n\n\n<i>Information and Computation</i>,\n\n101(2):251--267.\n\n 1992.\n\n\n\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content\">\n \n \n \n \n \n\n <a href=\"http://web.cs.wpi.edu/~dd/publications/iandc92.pdf\"\n onclick=\"javascript:log_download('dougherty-addingalgebraicrewritingtotheuntypedlambdacalculus-1992', 'http://web.cs.wpi.edu/~dd/publications/iandc92.pdf')\">\n <img src=\"http://bibbase.org/img/filetypes/pdf.png\"\n\t alt=\"Adding Algebraic Rewriting to the Untyped Lambda Calculus [.pdf]\" \n\t class=\"bibbase_icon\"\n\t style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\" ><span class=\"bibbase_icon_text\">Paper</span></a> \n  \n \n \n <a href=\"javascript:showBib('a_iandc92')\"\n class=\"bibbase link\">\n \n\t\n\t\n\t\n BibTeX\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n  \n <a class=\"bibbase_abstract_link bibbase link\"\n href=\"javascript:showAbstract('a_iandc92')\">\n Abstract\n <i class=\"fa fa-caret-down\"></i></a>\n \n \n \n\n \n \n \n</span>\n\n<div class=\"well well-small bibbase\" id=\"bib_a_iandc92\"\n style=\"display:none\">\n <pre>@article{ a_iandc92,\n title = {Adding Algebraic Rewriting to the Untyped\n Lambda Calculus},\n author = {Daniel J.\\ Dougherty},\n pages = {251--267},\n journal = {Information and Computation},\n year = {1992},\n volume = {101},\n number = {2},\n abstract = {We investigate the system obtained by adding an\n algebraic rewriting system R to an untyped\n lambda calculus in which terms are formed using\n the function symbols from $R$ as constants. On\n certain classes of terms, called here \\emph{stable},\n we prove that the resulting calculus is\n confluent if R is confluent, and terminating if\n R is terminating. The termination result has\n the corresponding theorems for several typed\n calculi as corollaries. The proof of the\n confluence result suggests a general method for\n proving confluence of typed beta-reduction plus\n rewriting; we sketch the application to the\n polymorphic lambda calculus.},\n url = {iandc92.pdf}\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" id=\"abstract_a_iandc92\"\n style=\"display:none\">\n We investigate the system obtained by adding an algebraic rewriting system R to an untyped lambda calculus in which terms are formed using the function symbols from $R$ as constants. On certain classes of terms, called here \\emphstable, we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result suggests a general method for proving confluence of typed beta-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.\n</div>\n\n\n</div>\n","downloads":0,"bibbaseid":"dougherty-addingalgebraicrewritingtotheuntypedlambdacalculus-1992","urls":{"Paper":"http://web.cs.wpi.edu/~dd/publications/iandc92.pdf"},"role":"author","abstract":"We investigate the system obtained by adding an algebraic rewriting system R to an untyped lambda calculus in which terms are formed using the function symbols from $R$ as constants. On certain classes of terms, called here \\emphstable, we prove that the resulting calculus is confluent if R is confluent, and terminating if R is terminating. The termination result has the corresponding theorems for several typed calculi as corollaries. The proof of the confluence result suggests a general method for proving confluence of typed beta-reduction plus rewriting; we sketch the application to the polymorphic lambda calculus.","author":["Dougherty, Daniel J.\\"],"author_short":["Dougherty, D.<nbsp>J.\\"],"bibtex":"@article{ a_iandc92,\n title = {Adding Algebraic Rewriting to the Untyped\n Lambda Calculus},\n author = {Daniel J.\\ Dougherty},\n pages = {251--267},\n journal = {Information and Computation},\n year = {1992},\n volume = {101},\n number = {2},\n abstract = {We investigate the system obtained by adding an\n algebraic rewriting system R to an untyped\n lambda calculus in which terms are formed using\n the function symbols from $R$ as constants. On\n certain classes of terms, called here \\emph{stable},\n we prove that the resulting calculus is\n confluent if R is confluent, and terminating if\n R is terminating. The termination result has\n the corresponding theorems for several typed\n calculi as corollaries. The proof of the\n confluence result suggests a general method for\n proving confluence of typed beta-reduction plus\n rewriting; we sketch the application to the\n polymorphic lambda calculus.},\n url = {iandc92.pdf}\n}","bibtype":"article","id":"a_iandc92","journal":"Information and Computation","key":"a_iandc92","number":"2","pages":"251--267","title":"Adding Algebraic Rewriting to the Untyped Lambda Calculus","type":"article","url":"iandc92.pdf","volume":"101","year":"1992"},"bibtype":"article","biburl":"http://web.cs.wpi.edu/~dd/publications/index.bib","downloads":0,"search_terms":["adding","algebraic","rewriting","untyped","lambda","calculus","dougherty"],"title":"Adding Algebraic Rewriting to the Untyped Lambda Calculus","year":1992,"dataSources":["HB5RrPb3Y5aikRoLH"]}