Proof Terms for Infinitary Rewriting

详细信息    查看全文

• 作者：Carlos Lombardi (16) (17) (18)
  Alejandro Ríos (16) (18)
  Roel de Vrijer (19)
  
• 关键词：infinitary rewriting ; proof terms ; permutation equivalence
• 刊名：Lecture Notes in Computer Science
• 出版年：2014
• 出版时间：2014
• 年：2014
• 卷：8560
• 期：1
• 页码：303-318
• 全文大小：280 KB
• 参考文献：1. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
  2. Courcelle, B.: Fundamental properties of infinite trees. Theor. Comput. Sci.?25, 95-69 (1983) CrossRef
  3. Endrullis, J., Hansen, H.H., Hendriks, D., Polonsky, A., Silva, A.: A coinductive treatment of infinitary rewriting. Presented at WIR 2013, First International Workshop on Infinitary Rewriting, Eindhoven, Netherlands (June 2013)
  4. Huet, G.P., Lévy, J.J.: Computations in orthogonal rewriting systems, i and ii. In: Computational Logic - Essays in Honor of Alan Robinson, pp. 395-14 (1991)
  5. Kennaway, R., Klop, J.W., Sleep, M.R., de Vries, F.J.: Transfinite reductions in orthogonal term rewriting systems. Inf. Comput.?119(1), 18-8 (1995) CrossRef
  6. Ketema, J.: Reinterpreting compression in infinitary rewriting. In: 23rd International Conference on Rewriting Techniques and Applications, RTA. LIPIcs, vol.?15, pp. 209-24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)
  7. Klop, J.W., de Vrijer, R.C.: Infinitary normalization. In: We Will Show Them: Essays in Honour of Dov Gabbay, vol.?2, pp. 169-92. College Publications (2005)
  8. Lombardi, C., Ríos, A., de Vrijer, R.: Proof terms for infinitary rewriting, progress report (2014), http://arxiv.org/abs/1402.2245
  9. van Oostrom, V., de Vrijer, R.: Four equivalent equivalences of reductions. Electronic Notes in Theoretical Computer Science?70(6), 21-1 (2002) CrossRef
  10. Suppes, P.: Axiomatic Set Theory. D. van Nostrand, Princeton, USA (1960)
  11. Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol.?55. Cambridge University Press, Cambridge (2003)
  
• 作者单位：Carlos Lombardi (16) (17) (18)
  Alejandro Ríos (16) (18)
  Roel de Vrijer (19)
  
  16. Universidad Nacional de Quilmes, Argentina
  17. PPS (Université Paris-Diderot and CNRS), France
  18. Universidad de Buenos Aires, Argentina
  19. VU University Amsterdam, The Netherlands
  
• ISSN：1611-3349

文摘

We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. Transfinite reductions can be faithfully represented as infinitary proof terms, unique up to infinitary associativity. We use proof terms to define equivalence of transfinite reductions on the basis of permutation equations. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.