Paper: Monadic theory of term rewritings (at LICS 1992)

Authors: Didier Caucal

Abstract

The monadic second-order theory of term rewritings is considered. It is shown that the monadic theory of the rewriting (or the suffix rewriting) of a ground rewrite system is undecidable. Furthermore, the first-order theory is undecidable for the prefix derivation according to a linear context-free grammar on linear terms. Nevertheless, a new notion on terms with variables is introduced: a term is entire if each of its subterms either is a variable, or is without variable or has the same variables as the term. It is shown that the monadic theory is decidable (respectively undecidable) for the prefix rewriting according to a rewrite system on entire terms, with an axiom (respectively without axiom)

BibTeX

  @InProceedings{Caucal-Monadictheoryofterm,
    author = 	 {Didier Caucal},
    title = 	 {Monadic theory of term rewritings},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS 1992)},
    year =	 {1992},
    month =	 {June}, 
    pages =      {266--273},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }