λ-definition of function(al)s by normal forms

Abstract

Lambda-calculus is extended in order to represent a rather large class of recursive equation systems, implicitly characterizing function(al)s or mappings of some algebraic domain into arbitrary sets. Algebraic equality will then be represented by λβδ-convertibility (or even reducibility). It is then proved, under very weak assumptions on the structure of the equations, that there always exist solutions in normal form (Interpretation theorem). Some features of the solutions, like the use of parametric representations of the algebraic constructors, higher-order solutions by currification, definability of functions on unions of algebras, etc., have been easily checked by a first implementation of the mentioned theorem, the CuCh machine.