Nivat's theorem for pushdown transducers

AbstractThe notions of an extended pushdown automaton (PDA) and a pushdown transducer (PDT) are formalized in matrix notation by generalizing the concept of a pushdown transition matrix. The resulting matrices form a semiring. The equivalence to “nonextended” PDAs and PDTs is shown. The semiring structure gives a new proof that the types reset-pushdown and one-counter are real-time types. Moreover, it allows the construction of the functional composition of a pushdown transduction and a finite transducer mapping. As an important application, Nivat's theorem is generalized to rational and polynomial PDTs over arbitrary semirings. Examples include the mirror image of the input and the Dyck reduction