{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T12:32:19Z","timestamp":1648989139713},"reference-count":0,"publisher":"World Scientific Pub Co Pte Lt","issue":"03","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int. J. Found. Comput. Sci."],"published-print":{"date-parts":[[1992,9]]},"abstract":"<jats:p> We present a unification algorithm for the \u03bb\u03a0-calculus, the lambda calculus with first-order dependent function types. Our algorithm is an extension of Huet\u2019s algorithm for the simply-typed lambda calculus to first-order dependent function types. <\/jats:p><jats:p> In the simply-typed lambda calculus one attempts to unify a pair of terms of the same type; in the \u03bb\u03a0-calculus types are dependent on terms so one must unify not only terms, but their types as well. Accordingly, we identify a suitable notion of similarity of types, and only attempt to unify a pair of terms of similar type: if the types are not similar then they are not unifiable. Since Huet\u2019s algorithm does not enumerate all of the unifiers of a given pair of terms, the strategy of first unifying pairs of types \u2014 by identifying suitable pairs of subterms for unification \u2014 is not complete. Accordingly, we must unify terms and their types simultaneously, taking care to maintain all of the conditions that are necessary to ensure the well-formedness of the resulting calculated substitution. <\/jats:p><jats:p> Our notion of substitution is an algebraic one: substitutions are morphisms of \u03bb\u03a0-contexts. However, in order to define our algorithm we must work with psubstitutions and pcontexts \u2014 substitutions and contexts, respectively, in which variables are replaced by terms of similar, not \u03b2(\u03b7)-equal, type. <\/jats:p>","DOI":"10.1142\/s012905419200019x","type":"journal-article","created":{"date-parts":[[2004,11,25]],"date-time":"2004-11-25T00:50:24Z","timestamp":1101343824000},"page":"333-378","source":"Crossref","is-referenced-by-count":8,"title":["A UNIFICATION ALGORITHM FOR THE \u03bb\u03a0-CALCULUS"],"prefix":"10.1142","volume":"03","author":[{"given":"DAVID","family":"PYM","sequence":"first","affiliation":[{"name":"University of Edinburgh, Laboratory for Foundations of Computer Science, Department of Computer Science, The King\u2019s Buildings, Edinburgh EH9 3JZ, Scotland, U.K"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"219","published-online":{"date-parts":[[2011,11,20]]},"container-title":["International Journal of Foundations of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S012905419200019X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,7]],"date-time":"2019-08-07T00:51:45Z","timestamp":1565139105000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/abs\/10.1142\/S012905419200019X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,9]]},"references-count":0,"journal-issue":{"issue":"03","published-online":{"date-parts":[[2011,11,20]]},"published-print":{"date-parts":[[1992,9]]}},"alternative-id":["10.1142\/S012905419200019X"],"URL":"https:\/\/doi.org\/10.1142\/s012905419200019x","relation":{},"ISSN":["0129-0541","1793-6373"],"issn-type":[{"value":"0129-0541","type":"print"},{"value":"1793-6373","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,9]]}}}