Name
Abstract | ||
|---|---|---|
We denote first-order substitutions of finite and infinite terms by function symbols indexed by the sequences of first-order variables to which substitutions are made. We consider the evaluation mapping from infinite terms to infinite terms that evaluates these substitution operations. This mapping may perform infinitely many nested substitutions, so that a term which has the structure of an infinite string can be transformed into one isomorphic to an infinite binary tree. We prove that this mapping is monadic second-order compatible which means that a monadic second-order formula expressing a property of the output term produced by the evaluation mapping can be translated into a monadic second-order formula expressing this property over the input term. This implies that, deciding the monadic second-order theory of the output term reduces to deciding that of the input term. As an application, we obtain another proof that the monadic second-order properties of the algebraic trees, which represent the behaviours of recursive applicative program schemes, are decidable. This proof extends to hyperalgebraic trees. These infinite trees correspond to certain recursive program schemes with functional parameters of arbitrary high type. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S0304-3975(02)00012-9 | Theor. Comput. Sci. |
Keywords | DocType | Volume |
evaluation mapping,monadic second-order logic,decidability of logical theories,monadic second-order formula,infinite binary tree,infinite string,first-order substitution,monadic second-order theory,infinite tree,output term,infinite term,monadic second-order property,hyperalgebraic tree,algebraic tree,input term | Journal | 281 |
Issue | ISSN | Citations |
1 | Theoretical Computer Science | 4 |
PageRank | References | Authors |
0.86 | 14 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bruno Courcelle | 1 | 3418 | 388.00 |
| Teodor Knapix | 2 | 4 | 0.86 |