2026-07-24T11:35:00Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17999 2024-03-06T11:00:49Z ddc:004 open_access

Cost-Size Semantics for Call-By-Value Higher-Order Rewriting Kop, Cynthia Vale, Deivid Call-by-Value Evaluation Complexity Theory Higher-Order Rewriting Higher-order rewriting is a framework in which higher-order programs can be described by transformation rules on expressions. A computation occurs by transforming an expression into another using such rules. This step-by-step computation model induced by rewriting naturally gives rise to a notion of complexity as the number of steps needed to reduce expressions to a normal form, i.e., an expression that cannot be reduced further. The study of complexity analysis focuses on the development of automatable techniques to provide bounds to this number. In this paper, we consider a form of higher-order rewriting with a call-by-value evaluation strategy, so as to model call-by-value programs. We provide a cost-size semantics: a class of algebraic interpretations to map terms to tuples which bound both the reduction cost and the size of normal forms. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Cynthia Kop and Deivid Vale 2023 Is Part Of LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2023.15 urn:nbn:de:0030-drops-179993 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.15 eng https://creativecommons.org/licenses/by/4.0/legalcode