Paper Info
Title
Axiomatic Rewriting Theory VI Residual Theory Revisited
Abstract
Residual theory is the algebraic theory of confluence for the 驴-calculus, and more generally conflict-free rewriting systems (=without critical pairs). The theory took its modern shape in L茅vy's PhD thesis, after Church, Rosser and Curry's seminal steps. There, L茅vy introduces a permutation equivalence between rewriting paths, and establishes that among all confluence diagrams P 驴 N 驴 Q completing a span P 驴 M 驴 Q, there exists a minimum such one, modulo permutation equivalence. Categorically, the diagram is called a pushout.In this article, we extend L茅vy's residual theory, in order to enscope "border-line" rewriting systems, which admit critical pairs but enjoy a strong Church-Rosser property (=existence of pushouts.) Typical examples are the associativity rule and the positive braid rewriting systems. Finally, we show that the resulting theory reformulates and clarifies L茅vy's optimality theory for the 驴-calculus, and its so-called "extraction procedure".
Year
DOI
Venue
2002
10.1007/3-540-45610-4_4
RTA
Keywords
Field
DocType
phd thesis,associativity rule,critical pair,residual theory,axiomatic rewriting theory vi,algebraic theory,resulting theory reformulates,permutation equivalence,modulo permutation equivalence,span p,optimality theory,residual theory revisited,association rule
Discrete mathematics,Lambda calculus,Axiomatic system,Axiom,Algorithm,Critical pair,Equivalence (measure theory),Confluence,Algebraic theory,Rewriting,Mathematics
Conference
Volume
ISSN
ISBN
2378
0302-9743
3-540-43916-1
Citations 
PageRank 
References 
11
0.71
21
Authors
1
Name
Order
Citations
PageRank
Paul-andré Melliès139230.70