Result: Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding

Title:
Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding
Authors:
Source:
Mathematical Structures in Computer Science. 32:542-573
Publisher Information:
Cambridge University Press (CUP), 2022.
Publication Year:
2022
Document Type:
Academic journal Article
Language:
English
ISSN:
1469-8072
0960-1295
DOI:
10.1017/s0960129522000287
Rights:
Cambridge Core User Agreement
Accession Number:
edsair.doi...........7db10c668e6d2048a134a2e58adf580a
Database:
OpenAIRE

Further Information

By using algebraic structures in a presheaf category over finite sets, following Fiore, Plotkin and Turi, we develop sound and complete models of second-order rewriting systems called second-order computation systems (CSs). Restricting the algebraic structures to those equipped with well-founded relations, we obtain a complete characterisation of terminating CSs. We also extend the characterisation to rewriting on meta-terms using the notion of $\Sigma$ -monoid.