NDLI: A new decidability technique for ground term rewriting systems with applications

Please wait, while we are loading the content...

ACM Transactions on Computational Logic (TOCL) : Volume 17

ACM Transactions on Computational Logic (TOCL) : Volume 16

ACM Transactions on Computational Logic (TOCL) : Volume 15

ACM Transactions on Computational Logic (TOCL) : Volume 14

ACM Transactions on Computational Logic (TOCL) : Volume 13

ACM Transactions on Computational Logic (TOCL) : Volume 12

ACM Transactions on Computational Logic (TOCL) : Volume 11

ACM Transactions on Computational Logic (TOCL) : Volume 10

ACM Transactions on Computational Logic (TOCL) : Volume 9

ACM Transactions on Computational Logic (TOCL) : Volume 8

ACM Transactions on Computational Logic (TOCL) : Volume 7

ACM Transactions on Computational Logic (TOCL) : Volume 6

Issue 4, October 2005

Issue 3, July 2005

Issue 2, April 2005

Issue 1, January 2005

A classification of symbolic transition systems

Making abstract domains condensing

On equivalence and canonical forms in the LF type theory

A new decidability technique for ground term rewriting systems with applications

A modal logic framework for multi-agent belief fusion

Eternity variables to prove simulation of specifications

ACM Transactions on Computational Logic (TOCL) : Volume 5

ACM Transactions on Computational Logic (TOCL) : Volume 4

ACM Transactions on Computational Logic (TOCL) : Volume 3

ACM Transactions on Computational Logic (TOCL) : Volume 2

ACM Transactions on Computational Logic (TOCL) : Volume 1

A new decidability technique for ground term rewriting systems with applications

Content Provider	ACM Digital Library
Author	Hayrapetyan, Ara Verma, Rakesh
Copyright Year	2005
Abstract	Programming language interpreters, proving equations (e.g. $x^{3}$ = $\textit{x}$ implies the ring is Abelian), abstract data types, program transformation and optimization, and even computation itself (e.g., turing machine) can all be specified by a set of rules, called a rewrite system. Two fundamental properties of a rewrite system are the confluence or Church--Rosser property and the unique normalization property. In this article, we develop a standard form for ground rewrite systems and the concept of standard rewriting. These concepts are then used to: prove a pumping lemma for them, and to derive a new and direct decidability technique for decision problems of ground rewrite systems. To illustrate the usefulness of these concepts, we apply them to prove: (i) polynomial size bounds for witnesses to violations of unique normalization and confluence for ground rewrite systems containing unary symbols and constants, and (ii) polynomial height bounds for witnesses to violations of unique normalization and confluence for arbitrary ground systems. Apart from the fact that our technique is direct in contrast to previous decidability results for both problems, which were indirectly obtained using tree automata techniques, this approach also yields tighter bounds for rewrite systems with unary symbols than the ones that can be derived with the indirect approach. Finally, as part of our results, we give a polynomial-time algorithm for checking whether a rewrite system has the unique normalization property for all subterms in the rules of the system.
Starting Page	102
Ending Page	123
Page Count	22
File Format	PDF
ISSN	15293785
e-ISSN	1557945X
DOI	10.1145/1042038.1042042
Volume Number	6
Issue Number	1
Journal	ACM Transactions on Computational Logic (TOCL)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2005-01-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Confluence Decision procedures Pumping lemma Rewriting Standard forms Unique normalization
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Logic Computational Mathematics Computer Science

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

ANew Decidability Technique for Ground Term Rewriting Systems with Applications

Layer Systems for Proving Confluence

Simultaneous checking of completeness and ground confluence for algebraic specifications

Classes of term rewrite systems with polynomial confluence problems

Deciding the confluence of ordered term rewrite systems

Decidability of the confluence of ground term rewriting systems

Decidability of the confluence of ground term rewriting systems

Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus

Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms

A new decidability technique for ground term rewriting systems with applications

Similar Documents

ANew Decidability Technique for Ground Term Rewriting Systems with Applications

Layer Systems for Proving Confluence

Simultaneous checking of completeness and ground confluence for algebraic specifications

Classes of term rewrite systems with polynomial confluence problems

Deciding the confluence of ordered term rewrite systems

Decidability of the confluence of ground term rewriting systems

Decidability of the confluence of ground term rewriting systems

Least upper bounds on the size of confluence and church-rosser diagrams in term rewriting and λ-calculus

Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms

A new decidability technique for ground term rewriting systems with applications