bib/in-the-wild/omega.bib

0001
0002 % Chew's theorem.
0003 @INPROCEEDINGS{Chew:81,
0004     AUTHOR = "P. Chew",
0005     TITLE = "Unique normal forms in term rewriting systems with repeated
0006                 variables",
0007     BOOKTITLE = "Proc. the 13th ACM STOC",
0008     YEAR = 1981,
0009     PAGES = "7--18",
0010     }
0011
0012 % UN of CL + PC
0013 @TECHREPORT{deVrijer:90,
0014     AUTHOR = "R. C. de Vrijer",
0015     TITLE = "Unique normal forms for combinatory logic with parallel
0016                 conditional, a case study in conditional rewriting",
0017     INSTITUTION = "Institute for Language, Logic and Information,
0018                   University of Amsterdam",
0019     NUMBER = "CT-90-09",
0020     YEAR = 1990
0021     }
0022
0023 % Incomplete proof
0024 @INPROCEEDINGS{Ogawa:92,
0025     AUTHOR = "M. Ogawa",
0026     TITLE = "Chew's theorem revisited - uniquely normalizing property of
0027              non-linear term rewriting systems",
0028     BOOKTITLE = "Proc. the International symposium on algorithms and
0029         computation",
0030     PAGES = "309--318",
0031     YEAR = 1992,
0032     NOTE = "LNCS 650"
0033     }
0034
0035
0036 @MISC{OpenProblems,
0037     Title = "Open Problems in Rewriting",
0038     HOWPUBLISHED = "http://www.lri.fr/~rtaloop/index.html"
0039     }
0040
0041 % Problem 79 was posed.
0042 @TECHREPORT{Mizuhito:89,
0043     AUTHOR = "M. Ogawa and S. Ono",
0044     TITLE = "On the Uniquely Converging Property of Nonlinear Term
0045              Rewriting Systems",
0046     INSTITUTION = "IEICE COMP89-7",
0047     YEAR = 1989
0048     }
0049
0050 % Unification with infinite terms
0051 @INPROCEEDINGS{Martelli:84,
0052     AUTHOR = "A. Martelli and G. Rossi",
0053     TITLE = "Efficient unification with infinite terms in logic programming",
0054     BOOKTITLE = "the International conference on fifth generation computer
0055                  systems",
0056     YEAR = 1984,
0057     PAGES = "202--209",
0058     }
0059
0060
0061 % A non-$E$-overlapping and non-duplicating TRS is UN. Furthermore,
0062 % A non-$E$-overlapping and right-ground TRS is CR.
0063 % The statement, a non-$E$-overlapping and right-linear TRS is CR, has a gap.
0064 % (Corollary 3)
0065 @INPROCEEDINGS{ToyamaOyamaguchi:94,
0066     AUTHOR = "Y. Toyama and M. Oyamaguchi",
0067     TITLE = "Church-{R}osser property and unique normal form property of
0068              non-duplicating term rewriting systems",
0069     BOOKTITLE = "Proc. the 4th CTRS",
0070     YEAR = 1994,
0071     PAGES = "316--331",
0072     NOTE = "LNCS 968"
0073     }
0074
0075
0076 % A non-$E$-overlapping and right-ground TRS is CR.
0077 @ARTICLE{OyamaguchiOhta:93,
0078     AUTHOR = "M. Oyamaguchi and Y. Ohta",
0079     TITLE = "On the confluent property of right-ground term rewriting
0080              systems",
0081     JOURNAL = "Trans. IEICE",
0082     VOLUME = "76-D-I",
0083     NUMBER = 2,
0084     PAGES = "39--45",
0085     YEAR = 1993,
0086     Note = "({\it in Japanese})"
0087     }
0088
0089 % A non-$E$-overlapping and simple-right-linear TRS is CR. See Problem 58.
0090 @ARTICLE{OyamaguchiOhtaToyama:95,
0091     AUTHOR = "M. Oyamaguchi and Y. Ohta and Y. Toyama",
0092     TITLE = "On the confluent property of simple-right-linear term rewriting
0093         systems",
0094     JOURNAL = "Trans. IEICE",
0095     VOLUME = "78-D-I",
0096     NUMBER = 3,
0097     PAGES = "263--268",
0098     YEAR = 1995,
0099     NOTE = "({\it in Japanese})"
0100     }
0101
0102
0103 % A non-$E$-overlapping and strongly depth-preserving TRS is CR.
0104 @ARTICLE{GomiOyamaguchiOhta:96a,
0105     AUTHOR = "H. Gomi and M. Oyamaguchi and Y. Ohta",
0106     TITLE = "On  the  Church-Rosser property of non-E-overlapping and strongly
0107         depth-preserving term rewriting systems",
0108     JOURNAL = "Trans. IPSJ",
0109     VOLUME = 37,
0110     NUMBER = 12,
0111     PAGES = "2147--2160",
0112     YEAR = 1996
0113     }
0114
0115 % A non-$E$-overlapping and strongly depth-preserving TRS is CR.
0116 @TECHREPORT{GomiOyamaguchiOhta:96b,
0117     AUTHOR = "H. Gomi and M. Oyamaguchi and Y. Ohta",
0118     TITLE = "On  the  Church-Rosser property of non-E-overlapping and
0119         weight-preserving TRS's",
0120     INSTITUTION = "RIMS Research Report",
0121     NUMBER = 950,
0122     PAGES = "167--173",
0123     YEAR = 1996
0124     }
0125
0126 % Include GomiOyamaguchiOhta:96b.
0127 @ARTICLE{GomiOyamaguchiOhta:98,
0128     AUTHOR = "H. Gomi and M. Oyamaguchi and Y. Ohta",
0129     TITLE = "On  the  Church-Rosser property of root-E-overlapping and strongly
0130         depth-preserving term rewriting systems",
0131     JOURNAL = "Trans. IPSJ",
0132     VOLUME = 39,
0133     NUMBER = 4,
0134     PAGES = "992--1005",
0135     YEAR = 1998
0136     }
0137
0138
0139 % A non-$\omega$-overlapping and depth-preserving TRS is non-$E$-overlapping.
0140 @ARTICLE{MatsuuraOyamaguchiOhtaOgawa:98,
0141     AUTHOR = "K. Matsuura and M. Oyamaguchi and Y. Ohta and M. Ogawa",
0142     TITLE = "On the E-overlapping property of nonlinear term rewriting
0143         systems",
0144     JOURNAL = "Trans. IEICE",
0145     VOLUME = "80 D-I",
0146     NUMBER = 11,
0147     PAGES = "847--855",
0148     YEAR = 1997,
0149     NOTE = "({\it in Japanese})"
0150     }
0151
0152
0153
0154 % Persistence (wrt reduction), weaker than non-$E$-overlapping (wrt conversion)
0155 % Key Claim 8 (pp.365) is suspicious.
0156 @INPROCEEDINGS{Verma:95,
0157     AUTHOR = "R.M. Verma",
0158     TITLE = "Unique Normal Forms and Confluence of Rewrite Systems:
0159         Persistence",
0160     BOOKTITLE = "Proc. IJCAI-95",
0161     YEAR = 1995,
0162     PAGES = "362--368",
0163     VOLUME = 1
0164     }
0165
0166 % Gap in Key lemma 6. A non-$\omega$-overlapping and non-duplicating TRS is UN.
0167 @INPROCEEDINGS{Verma:97,
0168     AUTHOR = "R.M. Verma",
0169     TITLE = "Unique Normal Forms for Nonlinear Term Rewriting Systems:
0170         Root Overlaps",
0171     BOOKTITLE = "Proc. Fundamentals of Computation Theory, FCT'97",
0172     YEAR = 1997,
0173     PAGES = "452--462",
0174     NOTE = "LNCS 1279"
0175     }
0176
0177
0178 % Higher-order rewrite systems, Lambda calculus with nonlinear rules
0179 % Counter example to CR, UN of Lambda with D.
0180 @MISC{KlopThesis:80,
0181     TITLE = "Combinatory reduction systems",
0182     AUTHOR = "J. W. Klop",
0183     NOTE = "Mathematical Centre Tracts Nr.127, Centre for Mathematics
0184             and Computer Science, Amsterdam, 1980.",
0185     }
0186
0187 % UN of Lambda with surjective pairing.
0188 @ARTICLE{KlopVrijer:89,
0189     AUTHOR = "J. W. Klop and R. C. de Vrijer",
0190     TITLE = "Unique normal forms for lambda calculus with surjective pairing",
0191     JOURNAL = "Information and Computation",
0192     VOLUME = 80,
0193     PAGES = "97--113",
0194     YEAR = 1989
0195     }
0196
0197 % Conservative extension of Lambda with surjective pairing.
0198 @INPROCEEDINGS{deVrijer:89,
0199     AUTHOR = "R. C. de Vrijer",
0200     TITLE = "Extending the Lambda calculus with Surjective Pairing
0201                 is Conservative",
0202     BOOKTITLE = "Proc. the 4th IEEE LICS",
0203     YEAR = 1989,
0204     PAGES = "204--215"
0205     }
0206
0207 % Extension of Klop's non-CR examples of lambda calculus + Dxx -> M rules.
0208 @ARTICLE{Bunder:85,
0209     AUTHOR = "Bunder, M.W.",
0210     TITLE = "An extension of {K}lop's counterexample to the {C}hurch-{R}osser
0211         property to $lambda$-calculus with other ordered pair combinators",
0212     JOURNAL = "Theoretical Computer Science",
0213     VOLUME = 39,
0214     NUMBER = 2,
0215     PAGES = "337--342",
0216     YEAR = 1985
0217     }
0218
0219 % Yet another counter exmaple of CR.
0220 @ARTICLE{CurienHardin:94,
0221     AUTHOR = "P.-L. Curien and T. Hardin",
0222     TITLE = "Theoretical Pearl: {Y}et yet a counterexample for $\lambda + SP$",
0223     JOURNAL = "Journal of Functional Programming",
0224     VOLUME = 4,
0225     NUMBER = 1,
0226     PAGES = "113--115",
0227     YEAR = 1994
0228     }
0229