Skip to main content
SpringerLink
Log in

On the Relation between Sized-Types Based Termination and Semantic Labelling

  • Conference paper
Computer Science Logic (CSL 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5771))

Included in the following conference series:

Abstract

We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expressions and Girard’s reducibility candidates, and applies on systems using constructor matching only. On the other hand, semantic labelling transforms a rewrite system by annotating each function symbol with the semantics of its arguments, and applies to any rewrite system.

First, we introduce a simplified version of SBT for the simply-typed lambda-calculus. Then, we give new proofs of the correctness of SBT using semantic labelling, both in the first and in the higher-order case. As a consequence, we show that SBT can be extended to systems using matching on defined symbols (e.g. associative functions).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abel, A.: Semi-continuous sized types and termination. Logical Methods in Computer Science 4(2), 1–33 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  2. Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14(1), 97–141 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  3. Blanqui, F.: Decidability of type-checking in the calculus of algebraic constructions with size annotations. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 135–150. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  5. Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 24–39. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  6. Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15(1), 37–92 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  7. Blanqui, F., Riba, C.: Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 105–119. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  8. Blanqui, F., Roux, C.: On the relation between sized-types based termination and semantic labelling, full version (2009), www-rocq.inria.fr/~blanqui/

  9. Doornbos, H., von Karger, B.: On the union of well-founded relations. Logic Journal of the IGPL 6(2), 195–201 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  10. Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. of LICS 1999 (1999)

    Google Scholar 

  11. Giménez, E.: Un Calcul de Constructions infinies et son application à la vérification de systèmes communiquants. PhD thesis, ENS Lyon, France (1996)

    Google Scholar 

  12. Girard, J.-Y.: Interprétation fonctionelle et élimination des coupures dans l’arithmetique d’ordre supérieur. PhD thesis, Université Paris VII, France (1972)

    Google Scholar 

  13. Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Proc. of PPDP 2007 (2007)

    Google Scholar 

  14. Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 135–149. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  15. Hirokawa, N., Middeldorp, A.: Predictive labeling. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 313–327. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. of POPL 1996 (1996)

    Google Scholar 

  17. Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems. Theoretical Computer Science 121, 279–308 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  18. Mendler, N.P.: Inductive Definition in Type Theory. PhD thesis. Cornell University, United States (1987)

    Google Scholar 

  19. Middeldorp, A., Ohsaki, H., Zantema, H.: Transforming termination by self-labelling. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104. Springer, Heidelberg (1996)

    Google Scholar 

  20. Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. In: Schroeder-Heister, P. (ed.) ELP 1989. LNCS, vol. 475. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  21. Xi, H.: Dependent types for program termination verification. In: Proc. of LICS 2001 (2001)

    Google Scholar 

  22. Zantema, H.: Termination of term rewriting by semantic labelling. Fundamenta Informaticae 24, 89–105 (1995)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FIT 3-604, Tsinghua University, Haidian District, Beijing, 100084, China

    Frédéric Blanqui

  2. LORIA, Pareo team, Campus Scientifique, BP 239, 54506, Vandoeuvre-lès-Nancy, Cedex, France

    Cody Roux

Authors
  1. Frédéric Blanqui
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Cody Roux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematische Grundlagen der Informatik, RWTH Aachen, 52056, Aachen, Germany

    Erich Grädel

  2. CENTRIA and Departamento de Matemática, Universidade Nova de Lisboa, 2829-516, Caparica, Portugal

    Reinhard Kahle

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Blanqui, F., Roux, C. (2009). On the Relation between Sized-Types Based Termination and Semantic Labelling. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04027-6_13

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04026-9

  • Online ISBN: 978-3-642-04027-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation