Functional Schemas with Nested Predicates

Abstract

A class of (monadic) functional schemas with nested predicates is defined. It is shown that termination, divergence and freedom problems for these schemas are decidable. It is proved that when the schemas are more general the freedom problem is undecidable. A procedure is given for deleting the identity function from the schema's definition at the cost of increasing $k$ by 1 when $k$ is the maximum depth of nesting. Part of our results extend results of [1] about schemas without nesting. Our algorithm for checking freedom is not a natural extension of theirs. Furthermore, using our algorithm for schemas without nesting yields a much more efficient way of deciding freedom than the algorithm suggested in [1]. Keywords and Phrases: monadic functional schemas, nested predicates, decision problems, equivalence, freedom, polynomial time, DPDA.