Higher-order semantic labelling for inductive datatype systems

ABSTRACT

We give a novel transformation for proving termination of higher-order rewrite systems in the format of Inductive Data Type Systems (IDTSs) by Blanqui, Jouannaud and Okada. The transformation called higher-order semantic labelling attaches algebraic semantics of the arguments to each function symbol. We systematically define the labelling and show that labelled systems give termination models in the frame-work of Fiore, Plotkin and Turi's binding algebras. As applications, we give simple proofs of termination of the explicit substitution system λ X and currying transformation via higher-order semantic labelling. Moreover, we prove a new result of modularity of termination of IDTSs by introducing the notion of solid IDTSs. We prove that termination is preserved under the disjoint union of an IDTS and a higher-order program scheme.

REFERENCES

• 1: Frédéric Blanqui, Termination and Confluence of Higher-Order Rewrite Systems, Proceedings of the 11th International Conference on Rewriting Techniques and Applications, p.47-61, July 10-12, 2000
• 2: F. Blanqui. (HO)RPO revisited. Technical Report 5972, INRIA, 2006. Research report.
• 3: Frédéric Blanqui , Jean-Pierre Jouannaud , Mitsuhiro Okada, Inductive-data-type systems, Theoretical Computer Science, v.272 n.1-2, p.41-68, February 6, 2002 [doi>10.1016/S0304-3975(00)00347-9 ]
• 4: Roel Bloo , Herman Geuvers, Explicit substitution on the edge of strong normalization, Theoretical Computer Science, v.211 n.1-2, p.375-395, Jan. 28, 1999 [doi>10.1016/S0304-3975(97)00183-7 ]
• 5: R. Bloo and K. H. Rose. Preservation of strong normalisation in named lambda calculi with explicit substitution and garbage collection. In CSN-95: Computer Science in the Netherlands, pages 62--72, 1995.
• 6: Cristina Borralleras , Albert Rubio, A Monotonic Higher-Order Semantic Path Ordering, Proceedings of the Artificial Intelligence on Logic for Programming, p.531-547, December 03-07, 2001
• 7: Bruno Courcelle, Recursive applicative program schemes, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 8: N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae, 34:381--391, 1972.
• 9: Joëlle Despeyroux , Amy P. Felty , André Hirschowitz, Higher-Order Abstract Syntax in Coq, Proceedings of the Second International Conference on Typed Lambda Calculi and Applications, p.124-138, April 10-12, 1995
• 10: Marcelo Fiore, Semantic analysis of normalisation by evaluation for typed lambda calculus, Proceedings of the 4th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.26-37, October 06-08, 2002, Pittsburgh, PA, USA [doi>10.1145/571157.571161]
• 11: Marcelo Fiore , Gordon Plotkin , Daniele Turi, Abstract Syntax and Variable Binding, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.193, July 02-05, 1999
• 12: Neil Ghani , Tarmo Uustalu , Makoto Hamana, Explicit substitutions and higher-order syntax, Higher-Order and Symbolic Computation, v.19 n.2-3, p.263-282, September 2006 [doi>10.1007/s10990-006-8748-4]
• 13: M. Hamana. Free S-monoids: A higher-order syntax with metavariables. In Asian Symposium on Programming Languages and Systems (APLAS 2004), LNCS 3302, pages 348--363, 2004.
• 14: M. Hamana. Universal algebra for termination of higher-order rewriting. In Proceedings of 16th International Conference on Rewriting Techniques and Applications (RTA'05), LNCS 3467, pages 135--149. Springer, 2005.
• 15: Dan Dougherty , Pierre Lescanne, Reductions, intersection types, and explicit substitutions, Mathematical Structures in Computer Science, v.13 n.1, p.55-85, February 2003 [doi>10.1017/S0960129502003821]
• 16: J. -P. Jouannaud , A. Rubio, The Higher-Order Recursive Path Ordering, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.402, July 02-05, 1999
• 17: J.-P. Jouannaud and A. Rubio. Higher-order orderings for normal rewriting. In Proc. of RTA '06, LNCS 4098, pages 387--399, 2006.
• 18: Jean-Pierre Jouannaud , Albert Rubio, Polymorphic higher-order recursive path orderings, Journal of the ACM (JACM), v.54 n.1, p.1-es, March 2007 [doi>10.1145/1206035.1206037]
• 19: S. Katsumata. A generalisation of pre-logical predicates to simply typed formal systems. In ICALP, pages 831--845, 2004.
• 20: Richard Kennaway , Jan Willem Klop , Ronan Sleep , Fer-Jan De Vries, Comparing curried and uncurried rewriting, Journal of Symbolic Computation, v.21 n.1, p.15-39, Jan. 1996 [doi>10.1006/jsco.1996.0002 ]
• 21: J. W. Klop. Combinatory Reduction Systems. PhD thesis, CWI, Amsterdam, 1980. volume 127 of Mathematical Centre Tracts.
• 22: Jan Willem Klop , Vincent van Oostrom , Femke van Raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, v.121 n.1-2, p.279-308, Dec. 6, 1993 [doi>10.1016/0304-3975(93)90091-7 ]
• 23: Stéphane Lengrand , Pierre Lescanne , Dan Dougherty , Mariangiola Dezani-Ciancaglini , Steffen van Bakel, Intersection types for explicit substitutions, Information and Computation, v.189 n.1, p.17-42, 25 February 2004 [doi>10.1016/j.ic.2003.09.004]
• 24: Pierre Lescanne , Jocelyne Rouyer-Degli, Explicit Substitutions with de Bruijn's Levels, Proceedings of the 6th International Conference on Rewriting Techniques and Applications, p.294-308, April 05-07, 1995
• 25: S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, New York, 1971.
• 26: Marino Miculan , Ivan Scagnetto, A framework for typed HOAS and semantics, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.184-194, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888269]
• 27: Aart Middeldorp , Hitoshi Ohsaki , Hans Zantema, Transforming Termination by Self-Labelling, Proceedings of the 13th International Conference on Automated Deduction: Automated Deduction, p.373-387, August 03, 1996
• 28: T. Nipkow. Higher-order critical pairs. In Proc. 6th IEEE Symp. Logic in Computer Science, pages 342--349, 1991.
• 29: V. van Oostrom. Confluence for Abstract and Higher-Order Rewriting. PhD thesis, Vrije Universiteit, Amsterdam, 1994.
• 30: V. van Oostrom. Counterexamples to higher-order modularity. Draft, 2005.
• 31: Jaco van de Pol, Termination Proofs for Higher-order Rewrite Systems, Selected Papers from the First International Workshop on Higher-Order Algebra, Logic, and Term Rewriting, p.305-325, September 23-24, 1993
• 32: Femke van Raamsdonk, On Termination of Higher-Order Rewriting, Proceedings of the 12th International Conference on Rewriting Techniques and Applications, p.261-275, May 22-24, 2001
• 33: Miki Tanaka , John Power, A unified category-theoretic formulation of typed binding signatures, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, p.13-24, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088454.1088457]
• 34: Terese. Term Rewriting Systems. Number 55 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2003.
• 35: H. Zantema. Termination of term rewriting by semantic labelling. Fundamenta Informaticae, 24(1/2):89--105, 1995.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.2 Grammars and Other Rewriting Systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics; Denotational semantics; Algebraic approaches to semantics

General Terms:
Languages, Theory

Keywords:
categorical semantics, higher-order abstract syntax, higher-order rewriting, initial algebra semantics, modularity, termination