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

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

Problem #102

Originator: Bruno Courcelle
Date: January 2005

Summary: Investigate normalization by a canonical term rewrite system in the setting of second-order monadic logic

Consider a confluent and terminating term rewriting system and the mapping from a term to its normal form. When is this mapping a monadic second-order transduction? When does it preserve decidability of the monadic second-order theory of a set of terms?

See [Cou94, CK02]

References

[CK02]

Bruno Courcelle and Teodor Knapik. The evaluation of first-order substitution is monadic second-order compatible. Theoretical Computer Science, 281(1–2):177–206, June 2002.

[Cou94]

Bruno Courcelle. Monadic-second order graph transductions: A survey. Theoretical Computer Science, 126:53–75, 1994.

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

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