Small Families
Jean-Jacques Lévy
Colloquium in Honor of Gérard Huet, Paris 22-23 June 2007
In the (first-order) typed lambda calculus, finiteness
of redex families is equivalent to finiteness of reductions
(generalized finite development theorem). We will explore how
this notion resists to any term rewriting system or to
other finite calculi.