{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:54:34Z","timestamp":1781927674363,"version":"3.54.5"},"reference-count":26,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2022,3,17]],"date-time":"2022-03-17T00:00:00Z","timestamp":1647475200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques based on van Oostrom\u2019s decreasing diagrams that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. As shown in a previous paper of the two middle authors, confluence of a terminating set of left-linear rewrite rules is obtained when their critical pairs are joinable, beta-rewrite steps being disallowed. The present paper concentrates on the case where arbitrary beta-rewrite steps are allowed for joining critical pairs. The rewrite relation used for analyzing confluence may rewrite arbitrarily many non-overlapping redexes in a single step. This relation gives rise to critical pairs that overlap both horizontally, as with parallel rewriting, but also vertically, forming chains of successive overlaps. Practical examples of use of this technique are analyzed.<\/jats:p>","DOI":"10.1017\/s0960129522000044","type":"journal-article","created":{"date-parts":[[2022,3,17]],"date-time":"2022-03-17T11:49:43Z","timestamp":1647517783000},"page":"898-933","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":4,"title":["Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs"],"prefix":"10.1017","volume":"32","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gaspard","family":"F\u00e9rey","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4790-9927","authenticated-orcid":false,"given":"Jean-Pierre","family":"Jouannaud","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6725-8167","authenticated-orcid":false,"given":"Jiaxiang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2022,3,17]]},"reference":[{"key":"S0960129522000044_ref4","unstructured":"Felgenhauer, B. (2013). Rule labeling for confluence of left-linear term rewrite systems. In: IWC, 23\u201327."},{"key":"S0960129522000044_ref2","unstructured":"Assaf, A. , Dowek, G. , Jouannaud, J.-P. and Liu, J. (2018). Untyped confluence in dependent type theories. Draft hal-01515505, INRIA, January 2018. Presented at HOR 2016, Porto. Available from http:\/\/dedukti.gforge.inria.fr\/."},{"key":"S0960129522000044_ref9","unstructured":"Goguen, H. (1994). The metatheory of UTT. In: Dybjer, P., Nordstr\u00f6m, B. and Smith, J. M. (eds.) Types for Proofs and Prog- rams, International Workshop TYPES\u201994, B\u00c5stad, Sweden, June 6\u201310, 1994, Selected Papers, Lecture Notes in Computer Science, vol. 996, Springer, 60\u201382."},{"key":"S0960129522000044_ref7","unstructured":"F\u00e9rey, G. (2021). Higher-Order Confluence and Universe Embedding in the Logical Framework. Phd thesis, ENS Paris-Saclay, France."},{"key":"S0960129522000044_ref14","unstructured":"Klop, J. W. (1980). Combinatory Reduction Systems. Phd thesis, CWI Tracts."},{"key":"S0960129522000044_ref23","unstructured":"Terese. (2003). Term rewriting systems. In: Bezem, M., Klop, J. W. and de Vrijer, R. (eds.) Cambridge Tracts in Theoretical Computer Science, Cambridge University Press."},{"key":"S0960129522000044_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00173-9"},{"key":"S0960129522000044_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-014-9316-y"},{"key":"S0960129522000044_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.08.030"},{"key":"S0960129522000044_ref18","unstructured":"Liu, J. , Jouannaud, J.-P. and Ogawa, M. (2015). Confluence of layered rewrite systems. In: Kreutzer, S. (ed.) 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, September 7\u201310, 2015, Berlin, Germany, LIPIcs, vol. 41, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 423\u2013440."},{"key":"S0960129522000044_ref12","first-page":"395","author":"Huet","year":"1991"},{"key":"S0960129522000044_ref21","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151658"},{"key":"S0960129522000044_ref19","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00143-6"},{"key":"S0960129522000044_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)00023-K"},{"key":"S0960129522000044_ref20","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"S0960129522000044_ref10","first-page":"1","article-title":"How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation","volume":"1","author":"Hamana","year":"2017","journal-title":"PACMPL"},{"key":"S0960129522000044_ref15","author":"Knuth","year":"1970"},{"key":"S0960129522000044_ref16","unstructured":"Kop, C. (2020). WANDA - a higher-order termination tool (system description). In: Ariola, Z. M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29\u2013July 6, 2020, Paris, France (Virtual Conference), LIPIcs, vol. 167, Schloss Dagstuhl - Leibniz-Zentrum f\u00dcr Informatik, 36:1\u201336:19."},{"key":"S0960129522000044_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"S0960129522000044_ref8","unstructured":"Ferey, G. and Jouannaud, J.-P. (2019). Confluence in untyped higher-order theories by means of critical pairs. Draft. hal-03126102, INRIA, March 2019. Available from http:\/\/dedukti.gforge.inria.fr\/."},{"key":"S0960129522000044_ref1","unstructured":"Appel, C. , van Oostrom, V. and Simonsen, J. G. (2010). Higher-order (non-)modularity. In: Lynch, C. (ed.) Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11\u201313, 2010, Edinburgh, Scottland, UK, LIPIcs, vol. 6, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 17\u201332."},{"key":"S0960129522000044_ref17","first-page":"337","author":"Liu","year":"2014"},{"key":"S0960129522000044_ref22","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"S0960129522000044_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/2710017"},{"key":"S0960129522000044_ref3","unstructured":"Dowek, G. et al. (2016). The Dedukti system. Available from http:\/\/dedukti.gforge.inria.fr\/."},{"key":"S0960129522000044_ref6","unstructured":"Felgenhauer, B. and van Oostrom, V. (2013). Proof orders for decreasing diagrams. In: van Raamsdonk, F. (ed.) RTA, LIPIcs, vol. 21, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 174\u2013189."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129522000044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,22]],"date-time":"2023-02-22T08:15:49Z","timestamp":1677053749000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129522000044\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,17]]},"references-count":26,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["S0960129522000044"],"URL":"https:\/\/doi.org\/10.1017\/s0960129522000044","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,3,17]]},"assertion":[{"value":"\u00a9 The Author(s), 2022. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution, and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}