Abstract: "We show that a form of divide and conquer recursion on sets together with the relational algebra expresses exactly the queries over ordered relational databases which are NC-computable. At a finer level, we relate k nested uses of recursion exactly to AC[superscript k], k [> or =] 1. We also give corresponding results for complex objects."

The same programming paradigm scales up, yielding query languages for the complex-object model [AB89]. Beyond that, there are, for example, efficient programs for transitive closure and we are also able to write programs that move out of sets, and then perhaps back to sets, as long as we stay within a (quite flexible) type system. The uniform paradigm of the language suggests positive expectations for the optimization problem. In fact, structural recursion yields finer grain programming therefore we expect that lower-level, and therefore better optimizations will be feasible."

Abstract: "We study issues that arise in programming with primitive recursion over non-free datatypes such as lists, bags, and sets. Programs written in this style can lack a meaning in the sense that their outputs may be sensitive to the choice of input expression. We are, thus, naturally lead to a set-theoretic denotational semantics with partial functions. We set up a logic for reasoning about the definedness of terms and a deterministic and terminating evaluator. The logic is shown to be sound in the model, and its recursion free fragment is shown to be complete for proving definedness of recursion free programs.

We also show that if a many-sorted algebraic rewrite system R has the Church-Rosser property (is confluent), the R + [beta] + type-[beta] + type-[eta] rewriting of mixed terms has the Church-Rosser property too. Combining the two results, we conclude that if R is canonical (complete) on algebraic terms, then R +[beta] + type-[beta] + type-[eta] is canonical on mixed terms. [Eta] reduction does not commute with algebraic reduction, in general. However, using long [eta]-normal forms, we show that if R is canonical then R + [beta] + [eta] + type-[beta] + type-[eta] convertibility is still decidable."

Abstract: "We study combinations of many-sorted algebraic term rewriting systems and polymorphic lambda term rewriting. Algebraic and lambda terms are mixed by adding the symbols of the algebraic signature to the polymorphic lambda calculus, as higher-order constants. We show that if a many-sorted algebraic rewrite system R has the Church-Rosser property (is confluent), then R + [beta] + [eta] + type-[beta] + type-[eta] rewriting of mixed terms has the Church-Rosser property too. [Eta] reduction does not commute with algebraic reduction, in general. However, using long normal forms, we show that if R is canonical (confluent and strongly normalizing) then equational provability from R + [beta] + [eta] + type-[beta] + type-[eta] is still decidable."