Infinitary Term Rewriting allows to express infinitary terms and infinitary reductions that converge to them. As their notion of transfinite reduction in general, and as binary relations in particular two concepts have been studied in the past: strongly and weakly convergent reductions, and in the last decade research has mostly focused around the former. Finitary rewriting has a strong connection to the equational theory of its rule set: if the rewrite system is confluent this (implies consistency of the theory and) gives rise to a semi-decision procedure for the theory, and if the rewrite system is in addition terminating this becomes a decision procedure. This connection is the original reason for the study of these properties in rewriting. For infinitary rewriting there is barely an established notion of an equational theory. The reason this issue is not trivial is that such a theory would need to include some form of ``getting to limits'', and there are different options one can pursue. These options are being looked at here, as well as several alternatives for the notion of reduction relation and their relationships to these equational theories.

When Genetic Programming is used to evolve arithmetic functions it often operates by composing them from a fixed collection of elementary operators and applying them to parameters or certain primitive constants. This limits the expressiveness of the programs that can be evolved. It is possible to extend the expressiveness of such an approach significantly without leaving the comfort of terminating programs by including primitive recursion as a control operation.The technique used here was gene expression programming [2], a variation of grammatical evolution [8]. Grammatical evolution avoids the problem of program bloat; its separation of genotype (string of symbols) and phenotype (expression tree) permits to optimise the generated programs without interfering with the evolutionary process.

Chris Okasaki showed how to implement red-black trees in a functional programming language. Ralf Hinze incorporated even the invariants of such data structures into their types, using higher-order nested datatypes. We show how one can achieve something very similar without the usual performance penalty of such types, by combining the features of nested datatypes, phantom types and existential type variables.