{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T11:25:08Z","timestamp":1672572308102},"reference-count":47,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5755,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1993,6]]},"abstract":"<jats:p>Least fixpoints are constructed for finite coproducts of definable endofunctors of Cartesian closed categories that have weak polynomial products and joint equalizers of arbitrary families of pairs of parallel arrows. Both conditions hold in PER, the category whose objects are partial equivalence relations on N, and whose arrows are partial recursive functions. Weak polynomial products exist in any cartesian closed category with a finite number of objects as well as in any model of second order polymorphic lambda calculus: that is, in the proof theory of any second order positive intuitionistic propositional calculus, but such a category need not have equalizers. However, any finite coproduct of definable endofunctors of a cartesian closed category <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000190_xs1D49E\" \/> with weak polynomial products will have a least fixpoint in a larger category <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000190_inline1\" \/> with equalizers whose objects are right ideals (or sieves) of <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000190_xs1D49E\" \/> modulo certain congruence relations, and whose arrows are induced from <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" mimetype=\"image\" xlink:type=\"simple\" xlink:href=\"S0960129500000190_xs1D49E\" \/>.<\/jats:p>","DOI":"10.1017\/s0960129500000190","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T04:01:47Z","timestamp":1236139307000},"page":"229-257","source":"Crossref","is-referenced-by-count":5,"title":["Least fixpoints of endofunctors of cartesian closed categories"],"prefix":"10.1017","volume":"3","author":[{"given":"J.","family":"Lambek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000190_ref001","first-page":"199","article-title":"Remarks on fixpoints of functors","volume":"56","author":"Ad\u00e1mek","year":"1977","journal-title":"Springer LNCS"},{"key":"S0960129500000190_ref007","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90151-7"},{"key":"S0960129500000190_ref003","first-page":"212","article-title":"Free dynamics and algebraic dynamics","volume":"56","author":"Arbib","year":"1977","journal-title":"Springer LNCS"},{"key":"S0960129500000190_ref014","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(86)90044-7"},{"key":"S0960129500000190_ref035","unstructured":"Narayanan B. R. (1988) A general framework for models of type polymorphism, Ph.D. Thesis, Department of Computer and Information Science, Syracuse University."},{"key":"S0960129500000190_ref029","volume-title":"Introduction to higher order intuitionistic logic","author":"Lambek","year":"1986"},{"key":"S0960129500000190_ref034","volume-title":"Studies in Proof Theory I","author":"Martin-L\u00f6","year":"1984"},{"key":"S0960129500000190_ref042","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370825"},{"key":"S0960129500000190_ref039","first-page":"408","article-title":"Towards a theory of type structure","volume":"19","author":"Reynolds","year":"1974","journal-title":"Springer LNCS"},{"key":"S0960129500000190_ref036","first-page":"12","article-title":"Polymorphism is set theoretic constructively","volume":"283","author":"Pitts","year":"1987","journal-title":"Springer LNCS"},{"key":"S0960129500000190_ref038","volume-title":"Cat\u00e9gories et lambda-calcul","author":"Prout\u00e9","year":"1988"},{"key":"S0960129500000190_ref015","volume-title":"Proofs and types","author":"Girard","year":"1989"},{"key":"S0960129500000190_ref021","first-page":"133","article-title":"Un th\u00e9or\u00e8me sur les fonctions d\u2019ensembles","volume":"6","author":"Knaster","year":"1928","journal-title":"Ann. Soc. Polon. Math"},{"key":"S0960129500000190_ref024","first-page":"52","article-title":"Deductive systems and categories III","volume":"274","author":"Lambek","year":"1972","journal-title":"Springer LNM"},{"key":"S0960129500000190_ref047","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"S0960129500000190_ref016","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-51722-7_2"},{"key":"S0960129500000190_ref006","volume-title":"Categories, types and structures","author":"Asperti","year":"1991"},{"key":"S0960129500000190_ref027","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370824"},{"key":"S0960129500000190_ref012","volume-title":"A compendium of continuous lattices","author":"Gierz","year":"1986"},{"key":"S0960129500000190_ref046","first-page":"761","article-title":"The category-theoretic solution of recursive domain equations","volume":"11","author":"Smyth","year":"1982","journal-title":"S1AM Journal of Computing"},{"key":"S0960129500000190_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(74)90003-5"},{"key":"S0960129500000190_ref045","doi-asserted-by":"publisher","DOI":"10.2307\/2273831"},{"key":"S0960129500000190_ref026","first-page":"375","volume-title":"To H.B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"Lambek","year":"1980"},{"key":"S0960129500000190_ref002","volume-title":"Automata and algebras in categories","author":"Ad\u00e1mek","year":"1989"},{"key":"S0960129500000190_ref041","first-page":"140","volume-title":"Logical foundations of functional programming","author":"Reynolds","year":"1989"},{"key":"S0960129500000190_ref004","doi-asserted-by":"publisher","DOI":"10.1137\/1016026"},{"key":"S0960129500000190_ref033","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001298"},{"key":"S0960129500000190_ref005","unstructured":"Asperti A. G. (1990) Categorical topics in computer science, Ph.D. Thesis TD-7\/90, University of Pisa, Dipartimento di Informatica."},{"key":"S0960129500000190_ref008","volume-title":"Lattice theory","author":"Birkhoff","year":"1948"},{"key":"S0960129500000190_ref009","volume-title":"Combinatory logic","author":"Curry","year":"1958"},{"key":"S0960129500000190_ref043","first-page":"97","article-title":"Continuous lattices","volume":"274","author":"Scott","year":"1972","journal-title":"Springer LNM"},{"key":"S0960129500000190_ref040","first-page":"145","article-title":"Polymorphism is not set-theoretic","volume":"173","author":"Reynolds","year":"1984","journal-title":"Springer LNCS"},{"key":"S0960129500000190_ref010","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/106\/1057818"},{"key":"S0960129500000190_ref011","doi-asserted-by":"publisher","DOI":"10.1017\/S0004972700044828"},{"key":"S0960129500000190_ref013","volume-title":"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"S0960129500000190_ref017","first-page":"479","volume-title":"To H.B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"Howard","year":"1980"},{"key":"S0960129500000190_ref018","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90165-E"},{"key":"S0960129500000190_ref019","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90018-8"},{"key":"S0960129500000190_ref020","volume-title":"Introduction to metamathematics","author":"Kleene","year":"1952"},{"key":"S0960129500000190_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/BF01110627"},{"key":"S0960129500000190_ref023","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1970-065-6"},{"key":"S0960129500000190_ref028","first-page":"200","article-title":"Fixpoints revisited","volume":"363","author":"Lambek","year":"1989","journal-title":"Springer LNCS"},{"key":"S0960129500000190_ref030","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1969.tb01194.x"},{"key":"S0960129500000190_ref037","doi-asserted-by":"crossref","unstructured":"Pitts A. M. (1989) Non-trivial power types can't be subtypes of polymorphic types, U. of Cambridge, Computer Laboratory, Technical Report No. 159.","DOI":"10.1109\/LICS.1989.39154"},{"key":"S0960129500000190_ref031","first-page":"134","article-title":"Diagonal arguments and cartesian closed categories","volume":"92","author":"Lawvere","year":"1969","journal-title":"Springer LNM"},{"key":"S0960129500000190_ref032","volume-title":"Some aspects of impredicavity, Notes on Weyl\u2019s philosophy of mathematics and today\u2019s type theory","author":"Longo","year":"1988"},{"key":"S0960129500000190_ref044","first-page":"403","volume-title":"To H.B. Curry: essays on combinatory logic, lambda calculus and formalism","author":"Scott","year":"1980"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000190","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T18:50:38Z","timestamp":1557946238000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000190\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,6]]},"references-count":47,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,6]]}},"alternative-id":["S0960129500000190"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000190","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,6]]}}}