Special Issue – 13th Computing: The Australasian Theory Symposium (CATS 2007)No Access

TERMINATION OF ABSTRACT REDUCTION SYSTEMS

JEREMY E. DAWSON

Logic and Computation Program, NICTA, Locked Bag 8001, Canberra ACT 2601, Australia

RSISE (Bldg 115) Australian National University, Canberra ACT 0200, Australia

Search for more papers by this author

and

RAJEEV GORÉ

RSISE (Bldg 115) Australian National University, Canberra ACT 0200, Australia

Search for more papers by this author

https://doi.org/10.1142/S0129054109006450Cited by:0 (Source: Crossref)

Abstract

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

Keywords:

References

Y. Akama, A λ-to-CL Translation for Strong Normalization, Proc. Typed Lambda Calculi and Applications (TLCA'97)1210, LNCS (1997) pp. 1–10. Google Scholar
T. Altenkirch and J. Chapman , Tait in one big step , Proc. MSFP 2006, Electronic Workshops in Computing ( 2006 ) . Google Scholar
T. Arts and J. Giesl, The oretical Computer Science 236, 133 (2000), DOI: 10.1016/S0304-3975(99)00207-8. Web of Science, Google Scholar
F Baader and T Nipkow. Term Rewriting and All That. CUP, 1998 . Google Scholar
C. Borralleras, M. Ferreira and A. Rubio, Complete Monotonic Semantic Path Orderings, Proc. CADE-171831, LNCS (2000) pp. 346–364. Google Scholar
W. Buchholz, Annals of Pure and Applied Logic 75, 57 (1995), DOI: 10.1016/0168-0072(94)00056-9. Crossref, Web of Science, Google Scholar
J. E. Dawson and R. Goré, A New Machine-checked Proof of Strong Normalisation for Display Logic, Computing: The Australasian Theory Symposium78, Electronic Notes in Theoretical Computer Science (2003) pp. 16–35. Google Scholar
J. E. Dawson and R. Goré, A General Theorem on Termination of Rewriting, Proc. Computer Science Logic (CSL 2004)3210, LNCS (2004) pp. 100–114. Google Scholar
J E Dawson. Isabelle code, http://web.rsise.anu.edu.au/~jeremy/isabelle . Google Scholar
N. Dershowitz, 33 Examples of Termination, Proc. French Spring School of Theoretical Computer Science (1993)909, LNCS (1995) pp. 16–25. Google Scholar
N. Dershowitz and D. A. Plaisted, Handbook of Automated Reasoning, eds. Alan Robinson and Andrei Voronkov (Elsevier, 2001) pp. 535–610. Crossref, Google Scholar
N. Dershowitz, Termination Dependencies (Extended Abstract), Proc. Sixth Int'l Workshop on Termination (WST '03), ed. A. Rubio (2003) pp. 27–30. Google Scholar
N. Dershowitz and C. Hoot, Natural Termination 142 (TCS, 1995) pp. 179–207. Google Scholar
H. Doornbos and B. Von Karger, L. J. of the IGPL 6, 195 (1998), DOI: 10.1093/jigpal/6.2.195. Crossref, Google Scholar
M. A. E. Dummett , Elements of intuitionism ( Clarendon Press , 1977 ) . Google Scholar
M.-L. Fernández, G. Godoy and A. Rubio, Recursive Path Orderings Can Also Be Incre mental, Proc. LPAR20053835, LNCS (2005) pp. 230–245. Google Scholar
O. Fissore , I. Gnaedig and H. Kirchner , Termination of Rewriting with Local Strategies , Electronic Notes in Theoretical Computer Science 58 ( 2001 ) . Google Scholar
J. Giesl, T. Arts and E. Ohlebusch, Journal of Symbolic Computation 34(1), 21 (2002), DOI: 10.1006/jsco.2002.0541. Crossref, Web of Science, Google Scholar
J.-Y. Girard , Y. Lafont and P. Taylor , Proofs and Types ( CUP , 1990 ) . Google Scholar
I. Gnaedig and H. Kirchner, Narrowing, Abstraction and Constraints for Proving Properties of Reduction Relations, LNCS 4600 (Springer, 2007) pp. 44–67. Crossref, Google Scholar
J. Goubault-Larrecq, Well-founded recursive relations, Proc. CSL'20012142, LNCS (2001) pp. 484–497. Google Scholar
N. Hirokawa and A. Middeldorp, Dependency Pairs Revisited, Proc. Rewriting Techniques and Applications (RTA-04)3091, LNCS (2004) pp. 249–268. Google Scholar
S. C. Kleene and R. E. Vesley , The foundations of intuitionistic mathematics: especially in relation to recursive functions ( North-Holland , 1965 ) . Google Scholar
Y. Toyama, J. W. Klop and H. P. Barendregt, J of the ACM 42(6), 1275 (1995), DOI: 10.1145/227683.227689. Crossref, Web of Science, Google Scholar