Higher-order unification via combinators. Dougherty, D. J.\ Theoretical Computer Science, 114(2):273--298, 1993. Paper abstract bibtex We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type-variables, so that a solution may involve typesubstitution as well as term-substitution. the problem is first translated into the problem of unification with respect to extensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms.
@article{ a_tcs93,
author = {Daniel J.\ Dougherty},
title = {Higher-order unification via combinators},
journal = {Theoretical Computer Science},
volume = {114},
number = {2},
pages = {273--298},
day = {21},
year = {1993},
abstract = {We present an algorithm for unification in the
simply typed lambda calculus which enumerates
complete sets of unifiers using a finitely
branching search space. In fact, the types of
terms may contain type-variables, so that a
solution may involve typesubstitution as well
as term-substitution. the problem is first
translated into the problem of unification with
respect to extensional equality in combinatory
logic, and the algorithm is defined in terms of
transformations on systems of combinatory
terms. These transformations are based on a new
method (itself based on systems) for deciding
extensional equality between typed combinatory
logic terms. },
url = {tcs93.pdf}
}
Downloads: 0
{"_id":{"_str":"51f6934359ced8df44000e3b"},"__v":1,"authorIDs":[],"author_short":["Dougherty, D.<nbsp>J.\\"],"bibbaseid":"dougherty-higherorderunificationviacombinators-1993","bibdata":{"html":"<div class=\"bibbase_paper\"> \n\n\n<span class=\"bibbase_paper_titleauthoryear\">\n\t<span class=\"bibbase_paper_title\"><a name=\"a_tcs93\"> </a>Higher-order unification via combinators.</span>\n\t<span class=\"bibbase_paper_author\">\nDougherty, D. J.\\</span>\n\t<!-- <span class=\"bibbase_paper_year\">1993</span>. -->\n</span>\n\n\n\n<i>Theoretical Computer Science</i>,\n\n114(2):273--298.\n\n 1993.\n\n\n\n\n<br class=\"bibbase_paper_content\"/>\n\n<span class=\"bibbase_paper_content\">\n \n \n <!-- <i -->\n <!-- onclick=\"javascript:log_download('dougherty-higherorderunificationviacombinators-1993', 'http://web.cs.wpi.edu/~dd/publications/tcs93.pdf')\">DEBUG -->\n <!-- </i> -->\n\n <a href=\"http://web.cs.wpi.edu/~dd/publications/tcs93.pdf\"\n onclick=\"javascript:log_download('dougherty-higherorderunificationviacombinators-1993', 'http://web.cs.wpi.edu/~dd/publications/tcs93.pdf')\">\n <img src=\"http://bibbase.org/img/filetypes/pdf.png\"\n\t alt=\"Higher-order unification via combinators [.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_tcs93')\"\n class=\"bibbase link\">\n <!-- <img src=\"http://bibbase.org/img/filetypes/bib.png\" -->\n\t<!-- alt=\"Higher-order unification via combinators [bib]\" -->\n\t<!-- class=\"bibbase_icon\" -->\n\t<!-- style=\"width: 24px; height: 24px; border: 0px; vertical-align: text-top\"><span class=\"bibbase_icon_text\">Bibtex</span> -->\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_tcs93')\">\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_tcs93\"\n style=\"display:none\">\n <pre>@article{ a_tcs93,\n author = {Daniel J.\\ Dougherty},\n title = {Higher-order unification via combinators},\n journal = {Theoretical Computer Science},\n volume = {114},\n number = {2},\n pages = {273--298},\n day = {21},\n year = {1993},\n abstract = {We present an algorithm for unification in the\n simply typed lambda calculus which enumerates\n complete sets of unifiers using a finitely\n branching search space. In fact, the types of\n terms may contain type-variables, so that a\n solution may involve typesubstitution as well\n as term-substitution. the problem is first\n translated into the problem of unification with\n respect to extensional equality in combinatory\n logic, and the algorithm is defined in terms of\n transformations on systems of combinatory\n terms. These transformations are based on a new\n method (itself based on systems) for deciding\n extensional equality between typed combinatory\n logic terms. },\n url = {tcs93.pdf}\n}</pre>\n</div>\n\n\n<div class=\"well well-small bibbase\" id=\"abstract_a_tcs93\"\n style=\"display:none\">\n We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type-variables, so that a solution may involve typesubstitution as well as term-substitution. the problem is first translated into the problem of unification with respect to extensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms.\n</div>\n\n\n</div>\n","downloads":0,"bibbaseid":"dougherty-higherorderunificationviacombinators-1993","urls":{"Paper":"http://web.cs.wpi.edu/~dd/publications/tcs93.pdf"},"role":"author","abstract":"We present an algorithm for unification in the simply typed lambda calculus which enumerates complete sets of unifiers using a finitely branching search space. In fact, the types of terms may contain type-variables, so that a solution may involve typesubstitution as well as term-substitution. the problem is first translated into the problem of unification with respect to extensional equality in combinatory logic, and the algorithm is defined in terms of transformations on systems of combinatory terms. These transformations are based on a new method (itself based on systems) for deciding extensional equality between typed combinatory logic terms.","author":["Dougherty, Daniel J.\\"],"author_short":["Dougherty, D.<nbsp>J.\\"],"bibtex":"@article{ a_tcs93,\n author = {Daniel J.\\ Dougherty},\n title = {Higher-order unification via combinators},\n journal = {Theoretical Computer Science},\n volume = {114},\n number = {2},\n pages = {273--298},\n day = {21},\n year = {1993},\n abstract = {We present an algorithm for unification in the\n simply typed lambda calculus which enumerates\n complete sets of unifiers using a finitely\n branching search space. In fact, the types of\n terms may contain type-variables, so that a\n solution may involve typesubstitution as well\n as term-substitution. the problem is first\n translated into the problem of unification with\n respect to extensional equality in combinatory\n logic, and the algorithm is defined in terms of\n transformations on systems of combinatory\n terms. These transformations are based on a new\n method (itself based on systems) for deciding\n extensional equality between typed combinatory\n logic terms. },\n url = {tcs93.pdf}\n}","bibtype":"article","day":"21","id":"a_tcs93","journal":"Theoretical Computer Science","key":"a_tcs93","number":"2","pages":"273--298","title":"Higher-order unification via combinators","type":"article","url":"tcs93.pdf","volume":"114","year":"1993"},"bibtype":"article","biburl":"http://web.cs.wpi.edu/~dd/publications/index.bib","downloads":0,"search_terms":["higher","order","unification","via","combinators","dougherty"],"title":"Higher-order unification via combinators","year":1993,"dataSources":["HB5RrPb3Y5aikRoLH"]}