Solutions of the equations X = ZX and X = XZ are found and discussed for Z, X normal terms of the lambda-calculus. Obviously fixed point combinators are of no help. Solutions will be independent from any kind of gödelization or coding of data structures, they will be provided by typeless self-application. Different approaches will be shown: algebraic properties, one side invertibility and idempotency. Certain subsets of proper combinators and Church algebras between them will be proved to be domains consisting only of fixed points of combinators.

Given a finite set T identical to (T/sub 1/, . . . ,T/sub t/) of terms of the lambda - beta -K-calculus and a set X/sub T/ identical to (x/sub 1/, . . ., x/sub n/) of free variables (occurring in the elements of T), X/sub T/-separability is the problem of deciding whether there exists a simultaneous substitution for the elements of X/sub T/ transforming T into the set Z identical to (Z/sub 1/, . . . Z/sub t/) of arbitrary terms. The X/sub T/-separability problem is proved to be solvable for any approximation T/sup Hash / of the set T by terms in lambda - beta - Omega -normal form. Since the characterization is constructive, if the terms T/sup , Hash //sub i/ identical to lambda x/sub 1/ . . . x/sub n/. T/sup Hash //sub i/ (i=1, . . ., t) are closed then the sequence T/sup Hash //sub 1/, . . ., T/sup Hash //sub t/ induces a family of mappings (from n to t dimensions) whose surjectivity and right-invertibility becomes decidable. The left-invertibility of this family is proved to be decidable too.>

Abstract The notion of a minimal form is defined as an extension of the notion of a normal form inλ-β-calculus and its meaning is discussed in a computational environment. The features of the Knuth-Gross reduction strategy are used to prove that to possess a minimal form, for a generic term, is a semidecidable predicate.