ABSTRACT. We summarize recent work based on affine lambda-calculi which brings together some aspects of infinitary and higher-order rewriting. In particular, we discuss three points: the relationship with the (infinitary) lambda-calculus; the categorical perspective, which gives a way of building models of linear logic; and the applications to implicit computational complexity, in particular the possiblity of representing non-uniform polytime computation in a functional, higher-order setting.

ABSTRACT. Several extensions of the lambda-calculus allow to rewrite a term into a linear combination of terms taking coefficients in the ring of non-negative real numbers. The goal of this work is to define a notion of algebraic rewrite system abstracting away these calculi. In particular, we look for a notion of normalization induced by a rewriting compatible with the semi-ring structure and the usual topology on non-negative reals. The goal is to achieve a kind of Newman's lemma: "strong normalization together with local confluence implies confluence". We state the formal definitions and show how a (naïve) expected implication fails short with several non-trivial examples.