Checking Overlaps of Nominal Rewriting Rules

Autor:	Ana Cristina Rocha-Oliveira, Maribel Fernández, Mauricio Ayala-Rincón, Murdoch J. Gabbay
Rok vydání:	2016
Předmět:	Discrete mathematics binding General Computer Science Unification Relation (database) 0102 computer and information sciences 02 engineering and technology nominal syntax 01 natural sciences rewriting Theoretical Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Semi-Thue system Confluence confluence ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0202 electrical engineering electronic engineering information engineering Computer Science::Programming Languages 020201 artificial intelligence & image processing Rewriting Computer Science(all) Mathematics
Zdroj:	LSFA
ISSN:	1571-0661
DOI:	10.1016/j.entcs.2016.06.004
Popis:	Nominal rewriting generalises first-order rewriting by providing support for the specification of binding operators. In this paper, we give sufficient conditions for (local) confluence of closed nominal rewriting theories, based on the analysis of rule overlaps. More precisely, we show that closed nominal rewriting rules where all proper critical pairs are joinable are locally confluent. We also show how to refine the notion of rule overlap to derive confluence of the closed rewriting relation. The conditions that we define are easy to check using a nominal unification algorithm.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1819a88cf847e9cfb6d05e213b0f57ee https://doi.org/10.1016/j.entcs.2016.06.004 Zobrazit plný text záznamu Full Text from ScienceDirect