{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:12:17Z","timestamp":1759637537840},"reference-count":24,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":5298,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1994,9]]},"abstract":"<jats:p>We add extensional equalities for the functional and product types to the typed \u03bb-calculus with, in addition to products and terminal object, sums and bounded recursion (a version of recursion that does not allow recursive calls of infinite length). We provide a confluent and strongly normalizing (thus decidable) rewriting system for the calculus that stays confluent when allowing unbounded recursion. To do this, we turn the extensional equalities into <jats:italic>expansion<\/jats:italic> rules, and not into contractions as is done traditionally. We first prove the calculus to be weakly confluent, which is a more complex and interesting task than for the usual \u03bb-calculus. Then we provide an effective mechanism to simulate expansions without expansion rules, so that the strong normalization of the calculus can be derived from that of the underlying, traditional, non-extensional system. These results give us the confluence of the full calculus, but we also show how to deduce confluence directly form our simulation technique without using the weak confluence property.<\/jats:p>","DOI":"10.1017\/s0960129500000505","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:00:39Z","timestamp":1236157239000},"page":"315-362","source":"Crossref","is-referenced-by-count":18,"title":["Simulating expansions without expansions"],"prefix":"10.1017","volume":"4","author":[{"given":"Roberto Di","family":"Cosmo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"key":"S0960129500000505_ref015","unstructured":"Jay C. B. and Ghani N. (1992) The virtues of eta-expansion. Technical Report ECS-LFCS-92\u2013243, LFCS, University of Edimburgh."},{"key":"S0960129500000505_ref012","volume-title":"Proofs and Types","author":"Girard","year":"1990"},{"key":"S0960129500000505_ref011","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieure, Th\u00e8se de doctorat d\u2019\u00e9tat, Universit\u00e9 de Paris VII."},{"key":"S0960129500000505_ref009","doi-asserted-by":"crossref","unstructured":"Dougherty D. J. (1993) Some lambda calculi with categorical sums and products. In: Proc. of the Fifth International Conference on Rewriting Techniques and Applications (RTA).","DOI":"10.1007\/3-540-56868-9_12"},{"key":"S0960129500000505_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"S0960129500000505_ref007","unstructured":"Di Cosmo R. and Kesner D. (1993b) Simulating expansions without expansions. Technical Report LIENS-93\u201311\/INRIA 1911, LIENS-DMI and INRIA."},{"key":"S0960129500000505_ref019","first-page":"83","article-title":"Closed categories and the theory of proofs","volume":"68","author":"Mints","year":"1977","journal-title":"Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V.A. Steklova AN SSSR"},{"key":"S0960129500000505_ref004","volume-title":"Combinatory Logic","author":"Curry","year":"1958"},{"key":"S0960129500000505_ref017","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(76)90009-8"},{"key":"S0960129500000505_ref020","unstructured":"Mints G. (1979) Teorija categorii i teoria dokazatelstv. I. Aktualnye problemy logiki i metodologii nauky 252\u2013278"},{"key":"S0960129500000505_ref024","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093636767"},{"key":"S0960129500000505_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54233-7_142"},{"key":"S0960129500000505_ref016","article-title":"Combinatory reduction systems","volume":"27","author":"Klop","year":"1980","journal-title":"Mathematical Center Tracts"},{"key":"S0960129500000505_ref002","volume-title":"The Lambda Calculus; Its syntax and Semantics (revised edition)","author":"Barendregt","year":"1984"},{"key":"S0960129500000505_ref005","unstructured":"Cubric D. (1992) On free ccc. Distributed on the types mailing list."},{"key":"S0960129500000505_ref006","doi-asserted-by":"crossref","unstructured":"Di Cosmo R. and Kesner D. (1993a) A confluent reduction for the extensional typed \u03bb-calculus with pairs, sums, recursion and terminal object. In: Lingas, A. (ed.) Intern. Conf. on Automata, Languages and Programming (ICALP). Springer-Verlag Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-56939-1_109"},{"key":"S0960129500000505_ref001","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037094"},{"key":"S0960129500000505_ref008","unstructured":"Dougherty D. J. (1990) Some reduction properties of a lambda calculus with coproducts and recursive types. Technical report, Wesleyan University, E-mail: ddougherty@eagle.wesleyan.edu."},{"key":"S0960129500000505_ref013","unstructured":"Huet G. (1976) R\u00e9solution d\u2019\u00e9quations dans les langages d\u2019ordre 1,2,\u2026,\u03c9, Th\u00e8se d\u2019Etat, Universit\u00e9 Paris VII."},{"key":"S0960129500000505_ref014","unstructured":"Jay C. B. (1992) Long \u03b2\u03b7 normal forms and confluence (and its revised version). Technical Report ECS-LFCS-91\u2013183, LFCS, University of Edimburgh."},{"key":"S0960129500000505_ref018","volume-title":"An introduction to higher order categorical logic","author":"Lambek","year":"1986"},{"key":"S0960129500000505_ref021","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883461"},{"key":"S0960129500000505_ref023","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90029-8"},{"key":"S0960129500000505_ref010","unstructured":"Gallier J. (1993) On the correspondence between proofs and \u03bb-terms. (Available by anonymous ftp from ftp.cis.upenn.edu.)"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000505","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T02:48:07Z","timestamp":1557888487000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000505\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,9]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994,9]]}},"alternative-id":["S0960129500000505"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000505","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,9]]}}}