• An initial algebra approach to...

Result: An initial algebra approach to term rewriting systems with variable binders

Title:
An initial algebra approach to term rewriting systems with variable binders
Authors:
HAMANA, Makoto
Source:
Second ACM SIGPLAN workshop MEchanized Reasoning about Languages with varIable and Names (MERΛIN 2003)Higher-order and symbolic computation. 19(2-3):231-262
Publisher Information:
Heidelberg: Springer, 2006.
Publication Year:
2006
Physical Description:
print, 55 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences et techniques communes, Sciences and techniques of general use, Mathematiques, Mathematics, Algèbre, Algebra, Catégories, algèbre homologique, Category theory, homological algebra, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Algorithmique. Calculabilité. Arithmétique ordinateur, Algorithmics. Computability. Computer arithmetics, Théorie programmation, Programming theory, Calcul symbolique, Symbolic computation, Cálculo simbólico, Equation ordre 1, First order equation, Ecuación orden 1, Foncteur, Functor, Ordre 1, First order, Orden 1, Système réécriture, Rewriting systems, Logique équationnelle, Equational logic, Réécriture terme, Syntaxe abstraite avec liaison variable, Abstract syntax with variable binding, Syntaxe abstraite ordre élevé, Higher-order abstract syntax, Système réécriture terme, Sémantique algèbre initiale, Initial algebra semantics, Term rewriting systems, Terminaison
Document Type:
Conference Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Department of Computer Science, Gunma University, Japan
ISSN:
1388-3690
Access URL:
http://pascal-francis.inist.fr/vibad/index.php?action=search&terms=18084221
Rights:
Copyright 2006 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems

Mathematics
Accession Number:
edscal.18084221
Database:
PASCAL Archive

Further Information

We present an extension of first-order term rewriting systems. It involves variable binding in the term language. We develop systems called binding term rewriting systems (BTRSs) in a stepwise manner. First we present the term language, then formulate equational logic. Finally, we define rewriting systems. This development is novel because we follow the initial algebra approach in an extended notion of Σ-algebras in various functor categories. These are based on Fiore-Plotkin-Turi's presheaf semantics of variable binding and Lüth-Ghani's monadic semantics of term rewriting systems. We characterise the terms, equational logic and rewrite systems for BTRSs as initial algebras in suitable categories. Then, we show an important rewriting property of BTRSs: orthogonal BTRSs are confluent. Moreover, by using the initial algebra semantics, we give a complete characterisation of termination of BTRSs. Finally, we discuss our design choice of BTRSs from a semantic perspective.