Normalization of S-terms is decidable

1. H. P. Barendregt. The Lambda Calculus, Its Syntax and Sematics. Elsevier Science Publishers, 1984.

   Google Scholar 

2. Jan Bergstra and Jan Willem Klop. Church-Rosser strategies in the Lambda calculus. Theoretical Computer Science, 9:27–38, 1979.

   Article  MathSciNet  MATH  Google Scholar 

3. F. Gécseg and M. Steinby. Tree Automata. Akadémiai Kiadó, Budapest, 1984.

   MATH  Google Scholar 

4. Jan Willem Klop. Reduction Cycles in Combinatory Logic, pages 193–214. In Seldin and Hindley [SH80], 1980.

   Google Scholar 

5. Richard Kennaway and Ronan Sleep. Director strings as combinators. ACM Transactions on Programming Languages and Systems, 10(4):602–626, October 1988.

   Article  MATH  Google Scholar 

6. J. P. Seldin and J. R. Hindley, editors. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.

   Google Scholar 

7. Raymond Smullyan. To Mock a Mockingbird: and other logic puzzles including an amazing adventure in combinatory logic. Knopf, New York, 1985.

   Google Scholar 

8. Richard Statmann. The word problem for Smullyan's lark combinator is decidable. J. Symbolic Comput., 7:103–112, 1989.

   Article  MathSciNet  Google Scholar 

9. J. Waldmann. Nimm Zwei. Internal Report IR-432, Vrije Universiteit Amsterdam, Research Group Theoretical Computer Science, September 1997.

   Google Scholar 

10. Efstathios Zachos. Kombinatorische Logik und S-Terme. Berichte des Instituts für Informatik 26, Eidgenössische Technische Hochschule Zürich, 1978.

    Google Scholar 

11. H. Zantema and A. Geser. Non-looping rewriting. Technical Report UU-CS-1996-03, Utrecht University, January 1996.

    Google Scholar 

Download references