Jean-Pierre Jouannaud
Skip Abstract Section
Abstract
We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of Church’s simply typed λ-calculus and, on the other hand, any use of eta, as a reduction, as an expansion, or as an equation. The user’s rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.
- 1991. Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS’91). IEEE Computer Society.Google Scholar
- Hendrick Pieter Barendregt. 1993. Lambda calculus with types. In Handbook of Logic in Computer Science, Volume 2, Abramsky et al. (Eds.). Oxford University Press, 117--309.Google ScholarDigital Library
- Frédéric Blanqui. 2006. Higher-order dependency pairs. In Proceedings of the 8th International Workshop on Termination (WST’06).Google Scholar
- Frédéric Blanqui. 2007. Computability closure: Ten years later. In Rewriting, Computation and Proof (Lecture Notes in Computer Science), Hubert Comon-Lundh, Claude Kirchner, and Hélène Kirchner (Eds.), Vol. 4600. Springer, 68--88.Google Scholar
- Frédéric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. 1999. The calculus of algebraic constructions. In RTA (Lecture Notes in Computer Science), Paliath Narendran and Michaël Rusinowitch (Eds.), Vol. 1631. Springer, 301--316. Google ScholarDigital Library
- Frédéric Blanqui, Jean-Pierre Jouannaud, and Mitsuhiro Okada. 2002. Inductive-data-type systems. Theoretical Computer Science 272, 1--2 (2002), 41--68. Google ScholarDigital Library
- Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio. 2008. The computability path ordering: The end of a quest. In CSL (Lecture Notes in Computer Science), Michael Kaminski and Simone Martini (Eds.), Vol. 5213. Springer, 1--14. Google ScholarDigital Library
- Frédéric Blanqui, Jean-Pierre Jouannaud, and Albert Rubio. 2013. The Computability Path Ordering. (2013). Accepted for publication in Logical Methods for Computer Science.Google Scholar
- Miquel Bofill, Cristina Borralleras, Enric Rodrguez-Carbonell, and Albert Rubio. 2012. The recursive path and polynomial ordering for first-order and higher-order terms. Journal of Logic and Computation (2012). DOI: http://dx.doi.org/10.1093/logcom/exs027 Google ScholarDigital Library
- Cristina Borralleras and Albert Rubio. 2001. A monotonic higher-order semantic path ordering. In LPAR (Lecture Notes in Computer Science), Robert Nieuwenhuis and Andrei Voronkov (Eds.), Vol. 2250. Springer, 531--547. Google ScholarDigital Library
- Roberto Di Cosmo and Delia Kesner. 1994. Simulating expansions without expansions. Mathematical Structures in Computer Science 4, 3 (1994), 315--362.Google ScholarCross Ref
- Nachum Dershowitz. 1982. Orderings for term-rewriting systems. Theoretical Computer Science 17 (1982), 279--301.Google ScholarCross Ref
- Nachum Dershowitz and Jean-Pierre Jouannaud. 1990. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B). Elsevier, 243--320. Google ScholarDigital Library
- Carsten Fuhs and Cynthia Kop. 2012. Polynomial interpretations for higher-order rewriting. In RTA (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 176--192.Google Scholar
- Gérard P. Huet. 1980. Confluent reductions: Abstract properties and applications to term rewriting systems: Abstract properties and applications to term rewriting systems. Journal of the ACM 27, 4 (1980), 797--821. DOI: http://dx.doi.org/10.1145/322217.322230 Google ScholarDigital Library
- Jean-Pierre Jouannaud. 2005. Higher-order rewriting: Framework, confluence and termination. In Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday. Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel C. de Vrijer (Eds.). Lecture Notes in Computer Science, Vol. 3838. Springer, 224--250. Google ScholarDigital Library
- Jean-Pierre Jouannaud and Hélène Kirchner. 1986. Completion of a set of rules modulo a set of equations. SIAM Journal of Computing 15, 4 (1986), 1155--1194. Google ScholarDigital Library
- Jean-Pierre Jouannaud and Jianqi Li. 2012. Church-rosser properties of normal rewriting. In CSL (LIPIcs), Patrick Cégielski and Arnaud Durand (Eds.), Vol. 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 350--365.Google Scholar
- Jean-Pierre Jouannaud and Mitsuhiro Okada. 1991. A computation model for executable higher-order algebraic specification languages. In LICS. IEEE Computer Society, 350--361.Google Scholar
- Jean-Pierre Jouannaud and Albert Rubio. 1999. The higher-order recursive path ordering. In LICS. IEEE Computer Society, 402--411. Google ScholarDigital Library
- Jean-Pierre Jouannaud and Albert Rubio. 2006. Higher-order orderings for normal rewriting. In RTA (Lecture Notes in Computer Science), F. Pfenning (Ed.), Vol. 4098. Springer, 387--399. Google ScholarDigital Library
- Jean-Pierre Jouannaud and Albert Rubio. 2007. Polymorphic higher-order recursive path orderings. Journal of the ACM 54, 1 (2007), Article No. 2, 48. Google ScholarDigital Library
- Cynthia Kop. 2012. Higher Order Termination. Ph.D. Dissertation. VU University Amsterdam, Amsterdam, The Netherlands.Google Scholar
- Cynthia Kop and Femke van Raamsdonk. 2010. Higher-order dependency pairs with argument filterings. In Proceedings of the 11th International Workshop on Termination (WST’10).Google Scholar
- Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, and Frédéric Blanqui. 2009. Static dependency pair method based on strong computability for higher-order rewrite systems. IEICE Transactions on Information and Systems E92-D, 10 (2009), 2007--2015.Google Scholar
- Richard Mayr and Tobias Nipkow. 1998. Higher-order rewrite systems and their confluence. Theoretical Computer Science 192, 1 (1998), 3--29. Google ScholarDigital Library
- Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel C. de Vrijer (Eds.). 2005. Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, Vol. 3838. Springer. Google ScholarDigital Library
- Dale Miller. 1991. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logical Computing 1, 4 (1991), 497--536.Google ScholarCross Ref
- Tobias Nipkow. 1991. Higher-order critical pairs. In LICS. IEEE Computer Society, 342--349.Google Scholar
- Tobias Nipkow and Lawrence C. Paulson. 1992. Isabelle-91. In CADE (Lecture Notes in Computer Science), Deepak Kapur (Ed.), Vol. 607. Springer, 673--676. Google ScholarDigital Library
- Gerald E. Peterson and Mark E. Stickel. 1981. Complete sets of reductions for some equational theories. Journal of the ACM 28, 2 (1981), 233--264. Google ScholarDigital Library
- Jaco van de Pol. 1996. Termination of Higher-Order Rewrite Systems. Ph.D. Dissertation. Utrecht Universiteit, Utrecht, The Netherlands.Google Scholar
- Masahiko Sakai and Keiichirou Kusakari. 2005. On dependency pair method for proving termination of higher-order rewrite systems. IEICE Transactions on Information and Systems E88-D, 3 (2005), 583--593. Google ScholarDigital Library
- Masahiko Sakai, Yoshitsugu Watanabe, and Toshiki Sakabe. 2001. An extension of dependency pair method for proving termination of higher-order rewrite systems. IEICE Transactions on Information and Systems E84-D, 8 (2001), 1025--1032.Google Scholar
- Sho Suzuki, Keiichirou Kusakari, and Frédéric Blanqui. 2011. Argument filterings and usable rules in higher-order rewrite systems. IPSJ Transactions on Programming 4, 2 (2011), 1--12.Google Scholar
- Terese. 2003. Term rewriting systems. In Cambridge Tracts in Theoretical Computer Science, Marc Bezem, Jan Willem Klop, and Roel de Vrijer (Eds.). Cambridge University Press.Google Scholar
- Jaco van de Pol. 1993. Termination proofs for higher-order rewrite systems. In HOA (Lecture Notes in Computer Science), Jan Heering, Karl Meinke, Bernhard Möller, and Tobias Nipkow (Eds.), Vol. 816. Springer, 305--325. Google ScholarDigital Library
- Jaco van de Pol and Helmut Schwichtenberg. 1995. Strict functionals for termination proofs. In TLCA (Lecture Notes in Computer Science), Mariangiola Dezani-Ciancaglini and Gordon D. Plotkin (Eds.), Vol. 902. Springer, 350--364. Google ScholarDigital Library
- Femke van Raamsdonk. 2001. On termination of higher-order rewriting. In RTA (Lecture Notes in Computer Science), Aart Middeldorp (Ed.), Vol. 2051. Springer, 261--275. Google ScholarDigital Library
- Daria Walukiewicz-Chrzaszcz. 2003. Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming 13, 2 (2003), 339--414. Google ScholarDigital Library
Index Terms
- Normal Higher-Order Termination
Recommendations
Polymorphic higher-order recursive path orderings
This article extends the termination proof techniques based on reduction orderings to a higher-order setting, by defining a family of recursive path orderings for terms of a typed lambda-calculus generated by a signature of polymorphic higher-order ...
Relating Higher-order and First-order Rewriting
We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory. In particular, we obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting ...
Primitive recursion for higher-order abstract syntax
Higher-order abstract syntax is a central representation technique in logical frameworks which maps variables of the object language into variables of the meta-language. It leads to concise encodings, but is incompatible with functions defined by ...
Comments