Abstract: 
We introduce streaming data string transducers that map input data strings to output data strings in a single lefttoright pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data do main that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next in put symbol, updating its state, remembering the input data value in its data variables, and updating datastring variables by concatenat ing datastring variables and new symbols formed from data vari ables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over in put/output datastrings, are in PSPACE.
We identify a class of imperative and a class of functional pro grams, manipulating lists of data items, which can be effectively translated to streaming datastring transducers. The imperative pro grams dynamically modify a singlylinked heap by changing next pointers of heapnodes and by adding new nodes. The main re striction specifies how the nextpointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.
