{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T00:23:45Z","timestamp":1718670225607},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"3","funder":[{"DOI":"10.13039\/501100001824","name":"Czech Science Foundation","doi-asserted-by":"crossref","award":["22-06414L"],"id":[{"id":"10.13039\/501100001824","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Linz Institute of Technology","award":["LIT-2019-7-YOU-213"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,7,31]]},"abstract":"\n Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further develop proof generalization techniques and other transformations. So far, investigations concerned with anti-unification (AU) over \u03bb-terms and similar type theories have focused on developing algorithms for well-studied variants. These variants forbid the nesting of generalization variables, restrict the structure of their arguments, and are\n unitary<\/jats:italic>\n . Extending these methods to more expressive variants is important to applications. We consider the case of nested generalization variables and show that the AU problem is\n nullary<\/jats:italic>\n (using\n capture-avoiding<\/jats:italic>\n substitutions), even when the arguments to free variables are severely restricted.\n <\/jats:p>","DOI":"10.1145\/3654798","type":"journal-article","created":{"date-parts":[[2024,3,28]],"date-time":"2024-03-28T13:12:58Z","timestamp":1711631578000},"page":"1-12","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"http:\/\/orcid.org\/0000-0002-6352-603X","authenticated-orcid":false,"given":"David M.","family":"Cerna","sequence":"first","affiliation":[{"name":"Czech Academy of Sciences, Institute of Computer Science, Praha, Czech Republic and Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-1196-3799","authenticated-orcid":false,"given":"Michal","family":"Buran","sequence":"additional","affiliation":[{"name":"Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria"}]}],"member":"320","published-online":{"date-parts":[[2024,6,17]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.01.006"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.29007\/fkrh"},{"key":"e_1_3_2_4_2","unstructured":"Mauricio Ayala-Rincon David M. Cerna Andres Felipe Gonzalez Barragan and Temur Kutsia. 2023. Equational Anti-Unification over Absorption Theories. arxiv:2310.11136 [cs.LO]"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/3360585"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139032636","volume-title":"Lambda Calculus with Types","author":"Barendregt Hendrik Pieter","year":"2013","unstructured":"Hendrik Pieter Barendregt, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus with Types. Cambridge University Press, Cambridge, UK."},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.future.2017.07.024"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9383-3"},{"key":"e_1_3_2_9_2","first-page":"9:1\u20139:17","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","author":"Baumgartner Alexander","year":"2018","unstructured":"Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. 2018. Term-graph anti-unification. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018. Dagstuhl, Oxford, UK, 9:1\u20139:17. DOI:10.4230\/LIPIcs.FSCD.2018.9"},{"key":"e_1_3_2_10_2","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions","author":"Bertot Yves","year":"2013","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. Springer Science & Business Media, Germany."},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571207"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3359060"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2020.10.020"},{"key":"e_1_3_2_14_2","series-title":"LIPIcs","first-page":"10:1\u201310:19","volume-title":"4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019","volume":"131","author":"Cerna David M.","year":"2019","unstructured":"David M. Cerna and Temur Kutsia. 2019. A generic framework for higher-order generalizations. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019(LIPIcs, Vol. 131). Dagstuhl, Dortmund, Germany, 10:1\u201310:19. DOI:10.4230\/LIPIcs.FSCD.2019.10"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129520000110"},{"key":"e_1_3_2_16_2","series-title":"LIPIcs","first-page":"26:1\u201326:20","volume-title":"5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020","volume":"167","author":"Cerna David M.","year":"2020","unstructured":"David M. Cerna and Temur Kutsia. 2020. Unital anti-unification: Type and algorithms. In 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020(LIPIcs, Vol. 167), Zena M. Ariola (Ed.). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Paris, France (Virtual Conference), 26:1\u201326:20. DOI:10.4230\/LIPIcs.FSCD.2020.26"},{"key":"e_1_3_2_17_2","first-page":"6563","volume-title":"Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China","author":"Cerna David M.","year":"2023","unstructured":"David M. Cerna and Temur Kutsia. 2023. Anti-unification and generalization: A survey. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China. ijcai.org, Macao, SAR, China, 6563\u20136573. DOI:10.24963\/IJCAI.2023\/736"},{"key":"e_1_3_2_18_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"CADE","author":"Moura Leonardo Mendon\u00e7a de","year":"2015","unstructured":"Leonardo Mendon\u00e7a de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The lean theorem prover (system description). In CADE(Lecture Notes in Computer Science, Vol. 9195), Amy P. Felty and Aart Middeldorp (Eds.). Springer, Berlin, 378\u2013388."},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3474624.3474650"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2015.01.002"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-04299-8"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9285-6"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10472-021-09774-y"},{"key":"e_1_3_2_24_2","first-page":"435","volume-title":"17th USENIX Symposium on Networked Systems Design and Implementation, NSDI","author":"Mehta Sonu","year":"2020","unstructured":"Sonu Mehta, Ranjita Bhagwan, Rahul Kumar, Chetan Bansal, Chandra Shekhar Maddila, Balasubramanyan Ashok, Sumit Asthana, Christian Bird, and Aditya Kumar. 2020. Rex: Preventing bugs and misconfiguration in large services using correlated change analysis. In 17th USENIX Symposium on Networked Systems Design and Implementation, NSDI, Ranjita Bhagwan and George Porter (Eds.). USENIX Association, Santa Clara, CA, USA, 435\u2013448."},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1109\/LICS.1991.151632","volume-title":"[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science","author":"Pfenning F.","year":"1991","unstructured":"F. Pfenning. 1991. Unification and anti-unification in the calculus of constructions. In [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science. IEEE, Amsterdam, The Netherlands, 74\u201385. DOI:10.1109\/LICS.1991.151632"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/1614431.1614437"},{"issue":"1","key":"e_1_3_2_27_2","first-page":"153","article-title":"A note on inductive generalization","volume":"5","author":"Plotkin Gordon D.","year":"1970","unstructured":"Gordon D. Plotkin. 1970. A note on inductive generalization. Machine Intell. 5, 1 (1970), 153\u2013163.","journal-title":"Machine Intell."},{"issue":"1","key":"e_1_3_2_28_2","first-page":"135","article-title":"Transformational systems and the algebraic structure of atomic formulas","volume":"5","author":"Reynolds John C.","year":"1970","unstructured":"John C. Reynolds. 1970. Transformational systems and the algebraic structure of atomic formulas. Machine Intel. 5, 1 (1970), 135\u2013151.","journal-title":"Machine Intel."},{"key":"e_1_3_2_29_2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/b12055","volume-title":"Inductive Synthesis of Functional Programs, Universal Planning, Folding of Finite Programs, and Schema Abstraction by Analogical Reasoning","author":"Schmid Ute","year":"2003","unstructured":"Ute Schmid. 2003. Inductive Synthesis of Functional Programs, Universal Planning, Folding of Finite Programs, and Schema Abstraction by Analogical Reasoning. Lecture Notes in Computer Science, Vol. 2654. Springer,Germany. DOI:10.1007\/b12055"},{"key":"e_1_3_2_30_2","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","first-page":"7:1\u20137:22","volume-title":"7th International Conference on Formal Structures for Computation and Deduction (FSCD \u201922)","volume":"228","author":"Schmidt-Schau\u00df Manfred","year":"2022","unstructured":"Manfred Schmidt-Schau\u00df and Daniele Nantes-Sobrinho. 2022. Nominal anti-unification with atom-variables. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD \u201922)(Leibniz International Proceedings in Informatics (LIPIcs), Vol. 228), Amy P. Felty (Ed.). Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 7:1\u20137:22. DOI:10.4230\/LIPIcs.FSCD.2022.7"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3654798","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,17]],"date-time":"2024-06-17T11:37:00Z","timestamp":1718624220000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3654798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,17]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,7,31]]}},"alternative-id":["10.1145\/3654798"],"URL":"https:\/\/doi.org\/10.1145\/3654798","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,17]]},"assertion":[{"value":"2022-12-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-03-14","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
