[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #97

Originator: Henk Barendregt [Bar75]
Date: 1975

Summary: Is the word problem for the S-combinator decidable?

The word problem for the S-combinator is: Given two ground terms build only of the constant S in combinatory logic (that is with an application operator written as juxtaposition, and parantheses), are they convertible in the system consisting only of the definition of the S-combinator

Is the word-problem for the S-combinator decidable? See also [Wal98b] and [Wal98a] for more background.

A related problem is the word problem for proper combinators of order smaller than 3 (S is of order 3), see Problem #96.

References

[Bar75]

Henk Barendregt. Open problems. In Corrado Böhm, editor, Lambda Calculus and Computer Science Theory, volume 37 of Lecture Notes in Computer Science, pages 367–370. Springer-Verlag, 1975.

[Wal98a]

Johannes Waldmann. The Combinator S. PhD thesis, Fakultät für Mathematik und Informatik of the Friedrich-Schiller-Universität Jena, Jena, Germany, 1998.

[Wal98b]

Johannes Waldmann. Normalisation of s-terms is decidable. In Tobias Nipkow, editor, 9th International Conference on Rewriting Techniques and Applications, volume 1379 of Lecture Notes in Computer Science, pages 138–150, Tsukuba, Japan, April 1998. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]