Skip to main content
SpringerLink
Log in

Minimal relative normalization in orthogonal expression reduction systems

  • Conference paper
  • First Online:
Foundations of Software Technology and Theoretical Computer Science (FSTTCS 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1180))

Abstract

In previous papers, the authors studied normalization relative to desirable sets S of ‘partial results’, where it is shown that such sets must be stable. For example, the sets of normal forms, head-normal-forms, and weak head-normal-forms in the λ-calculus, are all stable. They showed that, for any stable S, S-needed reductions are S-normalizing. This paper continues the investigation into the theory of relative normalization. In particular, we prove existence of minimal normalizing reductions for regular stable sets of results. All the above mentioned sets are regular. We give a sufficient and necessary criterion for a normalizing reduction (w.r.t. a regular stable S) to be minimal. Finally, we establish a relationship between relative minimal and optimal reductions, revealing a conflict between minimality and optimality: for regular stable sets of results, a term need not possess a reduction that is minimal and optimal at the same time.

This work was supported by the Engineering and Physical Sciences Research Council of Great Britain under grant GR/H41300

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abramsky S., Ong C.-H. L. Full abstraction in the lazy lambda calculus. Inf.& Comp., 105:159–267, 1993.

    Google Scholar 

  2. Antoy S., Echahed R., Hanus M. A needed narrowing strategy. In: Proc. of POPL'94, Portland, Oregon, 1994.

    Google Scholar 

  3. Antoy S. and Middeldorp A. A Sequential Reduction Strategy. In Proc. of ALP'94, Springer LNCS, vol. 850, p. 168–185, 1994.

    Google Scholar 

  4. Asperti A., Laneve C. Interaction Systems I: the theory of optimal reductions. MSCS, 11:1–48, Cambridge University Press, 1993.

    Google Scholar 

  5. Barendregt H. P. The Lambda Calculus, its Syntax and Semantics. North-Holland, 1984.

    Google Scholar 

  6. Barendregt H. P., Kennaway J. R., Klop J. W., Sleep M. R. Needed Reduction and spine strategies for the lambda calculus. Inf.& Comp., 75(3):191–231, 1987.

    Google Scholar 

  7. Berry G., Lévy J.-J. Minimal and optimal computations of recursive programs. JACM 26, 1979, p. 148–175.

    Google Scholar 

  8. Boudol G. Computational semantics of term rewriting systems. In: Algebraic methods in semantics. Nivat M., Reynolds J.C., eds. Cambr. Univ. Press, 1985, p. 169–236.

    Google Scholar 

  9. Curry H. B., Feys R. Combinatory Logic. vol. 1, North-Holland, 1958.

    Google Scholar 

  10. Gardner P. Discovering needed reductions using type theory. In: Proc. of TACS'94, Springer LNCS, v. 789, M. Hagiya, J. C. Mitchell, eds. Sendai, 1994, p. 555–574.

    Google Scholar 

  11. Glauert J.R.W., Khasidashvili Z. Relative Normalization in Orthogonal Expression Reduction Systems. In: Proc. of CTRS'94, Springer LNCS, vol. 968, N. Dershowitz, N. Lindenstrauss, eds. Jerusalem, 1994, p. 144–165.

    Google Scholar 

  12. Glauert J.R.W., Khasidashvili Z. Minimal and optimal relative normalization in Expression Reduction Systems. Report SYS-C94-06, UEA, Norwich, 1994.

    Google Scholar 

  13. Glauert J.R.W., Khasidashvili Z. Relative normalization in deterministic residual structures. In: Proc. of CAAP'96, Springer LNCS, vol. 1059, H. Kirchner, ed. 1996, p. 180–195.

    Google Scholar 

  14. Gonthier G., Lévy J.-J., Melliès P.-A. An abstract Standardisation theorem. In: LICS'92, p. 72–81.

    Google Scholar 

  15. Huet G., Lévy J.-J. Computations in Orthogonal Rewriting Systems. In: Computational Logic, Essays in Honor of Alan Robinson, J.-L. Lassez and G. Plotkin, eds. MIT Press, 1991.

    Google Scholar 

  16. Kennaway J.R. Sequential evaluation strategy for parallel-or and related reduction systems. Annals of Pure and Applied Logic, 43:31–56, 1989.

    Google Scholar 

  17. Kennaway J. R., Sleep M. R. Neededness is hypernormalizing in regular combinatory reduction systems. Preprint, University of East Anglia, Norwich, 1989.

    Google Scholar 

  18. Kennaway J. R., Klop J. W., Sleep M. R., de Vries F.-J. Transfinite reductions in orthogonal term rewriting. Information and Computation, 119(1):18–38, 1995.

    Google Scholar 

  19. Khasidashvili Z. Β-reductions and Β-developments of λ-terms with the least number of steps. In: Proc. of the Int. Conference on Computer Logic COLOG'88, Tallinn 1988, Springer LNCS, v. 417, P. Martin-Löf and G. Mints, eds. 1990, p. 105–111.

    Google Scholar 

  20. Khasidashvili Z. The Church-Rosser theorem in Orthogonal Combinatory Reduction Systems. Report 1825, INRIA Rocquencourt, 1992.

    Google Scholar 

  21. Khasidashvili Z. Optimal normalization in orthogonal term rewriting systems. In: Proc. of RTA'93, Springer LNCS, vol. 690, C. Kirchner, ed. Montreal, 1993, p. 243–258.

    Google Scholar 

  22. Khasidashvili Z. On higher order recursive program schemes. In: Proc. of CAAP'94, Springer LNCS, vol. 787, S. Tison, ed. Edinburgh, 1994, p. 172–186.

    Google Scholar 

  23. Khasidashvili Z., van Oostrom V. Context-sensitive conditional expression reduction systems. Electronic Notes in Theoretical Computer Science, vol. 2, A. Corradini, U. Montanari, eds. Elsevier, 1995, p. 141–150.

    Google Scholar 

  24. Klop J. W. Combinatory Reduction Systems. Mathematical Centre Tracts n. 127, CWI, Amsterdam, 1980.

    Google Scholar 

  25. Klop J. W., van Oostrom V., van Raamsdonk F. Combinatory reduction systems: introduction and survey. In: To Corrado Böhm, TCS 121:279–308, 1993.

    Google Scholar 

  26. Lévy J.-J. An algebraic interpretation of the λΒK-calculus; and an application of a labelled λ-calculus. TCS 2(1):97–114, 1976.

    Google Scholar 

  27. Lévy J.-J. Réductions correctes et optimales dans le lambda-calcul, Thèse de l'Université de Paris VII, 1978.

    Google Scholar 

  28. Lévy J.-J. Optimal reductions in the Lambda-calculus. In: To H. B. Curry: Essays on Combinatory Logic, Lambda-calculus and Formalism, Hindley J. R., Seldin J. P. eds, Academic Press, 1980, p. 159–192.

    Google Scholar 

  29. Longo G. Set theoretic models of lambda calculus: theories, expansions and isomorphisms. Annals of pure and applied logic, 24:153–188, 1983.

    Google Scholar 

  30. Maranget L. Optimal derivations in weak λ-calculi and in orthogonal Term Rewriting Systems. In: Proc. POPL'91, p. 255–269.

    Google Scholar 

  31. Maranget L. La stratégie paresseuse. Thèse de l'Université de Paris VII, 1992.

    Google Scholar 

  32. Nipkow T. Orthogonal higher-order rewrite systems are confluent. In: Proc. of TLCA'93, Springer LNCS, vol. 664, Bazem M., Groote J.F., eds., 1993, p. 306–317.

    Google Scholar 

  33. Nöcker E. Efficient Functional Programming. Compilation and Programming Techniques. Ph. D. Thesis, Katholic University of Nijmegen, 1994.

    Google Scholar 

  34. Van Oostrom V. Confluence for Abstract and Higher-Order Rewriting. Ph.D. Thesis, Free University of Amsterdam, 1994.

    Google Scholar 

  35. Van Oostrom V. Higher order families. In proc. of RTA'96, Springer LNCS, vol. 1103, Ganzinger, H., ed., 1996, p. 392–407.

    Google Scholar 

  36. Van Oostrom V., van Raamsdonk F. Weak orthogonality implies confluence: the higher-order case. In: Proc. of LFCS'94, Springer LNCS, vol. 813, Narode A., Matiyasevich Yu. V. eds. St. Petersburg, 1994. p. 379–392.

    Google Scholar 

  37. Van Raamsdonk F. Confluence and normalisation for higher-order rewriting. Ph.D. Thesis, CWI Amsterdam, 1996.

    Google Scholar 

  38. Sekar R.C., Ramakrishnan I.V. Programming in Equational Logic: Beyond Strong Sequentiality. Information and Computation, 104(1):78–109, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Information Systems, UEA, NR4 7TJ, Norwich, England

    John Glauert & Zurab Khasidashvili

Authors
  1. John Glauert
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zurab Khasidashvili
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

V. Chandru V. Vinay

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Glauert, J., Khasidashvili, Z. (1996). Minimal relative normalization in orthogonal expression reduction systems. In: Chandru, V., Vinay, V. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1996. Lecture Notes in Computer Science, vol 1180. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-62034-6_53

Download citation

  • DOI: https://doi.org/10.1007/3-540-62034-6_53

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-62034-1

  • Online ISBN: 978-3-540-49631-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation