Chew's theorem revisited — uniquely normalizing property of nonlinear term rewriting systems

  • Mizuhito Ogawa
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 650)


This paper gives a purely syntactical proof, based on proof normalization techniques, of an extension of Chew's theorem. The main theorem is that a weakly compatible TRS is uniquely normalizing. Roughly speaking, the weakly compatible condition allows possibly nonlinear TRSs to have nonroot overlapping rules that return the same results. This result implies the consistency of CL-pc which is an extension of the combinatory logic CL with parallel-if rules.


Normal Form Reduction Rule Combinatory Logic Uniquely Normalize Lambda Calculus 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.van Leeuwen (eds.), “Handbook of Theoretical Computer Science, Vol.B Formal models and Semantics”, The MIT Press/Elservier (1990)Google Scholar
  2. 2.
    L.Bachmair, “Canonical Equational Proofs,” BirkhÄuser (1991)Google Scholar
  3. 3.
    J.W. Klop, “Combinatory Reduction Systems”, Mathematical Centre Tracts 127, CWI Amsterdam (1980)Google Scholar
  4. 4.
    D.S.Johnson (eds.), “STOC/FOCS Bibliography (Preliminary version)”, ACM SIGACT (1991)Google Scholar
  5. 5.
    Barendregt,H.P., M.C.J.D.Eekelen, J.R.W.Glauert, J.R.Kcnnaway, M.J.Pasmeijer, and M.R.Sleep, ”Term Graph Rewriting”, Proc. Parallel Architectures and Languages Europe Vol.2, pp.141–158, Springer LNCS 259 (1987)Google Scholar
  6. 6.
    J.A.Bergstra,and J.W.Klop, “Conditional Rewrite Rules: Confluence and Termination,” Journal of Computer and System Science, Vol. 32, pp. 323–362 (1986)CrossRefGoogle Scholar
  7. 7.
    P.Chew, “Unique Normal Forms in Term Rewriting Systems with Repeated Variables”,Proc. the 13th ACM Sympo. on Theory of Computing, pp.7–18 (1981)Google Scholar
  8. 8.
    P.L.Curien,and G.Ghelli, “On Confluence for Weakly Normalizing Systems,” Proc. the 4th Int. Conf. on Reduction Techniques and Applications, pp.215–225, Springer LNCS 488 (1991)Google Scholar
  9. 9.
    N.Dershowitz,and M.Okada, “Proof-theoretic techniques for term rewriting theory,” Proc. the 3rd IEEE Sympo. on Logic in Computer Science, pp.104–111 (1988)Google Scholar
  10. 10.
    N.Dershowitz, and Z.Manna, “Proving Termination with Multiset Orderings,” Comm. of the ACM, Vol. 22, No.8, pp. 465–476 (1979)CrossRefGoogle Scholar
  11. 11.
    G.Huet, “Confluent reductions: Abstract properties and applications to term rewriting systems”, Journal of the ACM, Vol. 27, No.4, pp. 797–821 (1980)CrossRefGoogle Scholar
  12. 12.
    J.W.Klop, and Vrijer, “Unique normal forms for lambda calculus with surjective pairing,” Information and Computation, Vol. 80, pp. 97–113 (1989)Google Scholar
  13. 13.
    B.K.Rosen, “Tree-manipulating systems and Church-Rosser theorems”, Journal of the ACM, Vol. 20, No.1, pp. 160–187 (1973)CrossRefGoogle Scholar
  14. 14. Vrijer, “Extending the Lambda Calculus with Surjective Pairing is Conservative,” Proc. the 4th IEEE Sympo. on Logic in Computer Science, pp.204–215 (1989)Google Scholar
  15. 15. Vrijer, “Unique Normal Forms for Combinatory Logic with Parallel Conditional, a case study in conditional rewriting,” Technical Report, Free University, Amsterdam (1990)Google Scholar
  16. 16.
    M.Ogawa,and S.Ono,“On the uniquely converging property of nonlinear term rewriting systems,” IEICE Technical Report COMP89-7, pp.61–70 (1989)Google Scholar
  17. 17.
    M.Oyamaguchi, Private Communications (April 1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Mizuhito Ogawa
    • 1
  1. 1.NTT Basic Research LaboratoriesTokyoJapan

Personalised recommendations