Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
How to make the Lambda Calculus strong normalizing without a type system?
pl.programming languages;computability;lambda calculus;functional programming
I can think of a few possible answers coming from linear logic.The simplest one is the affine lambda-calculus: consider only lambda-terms in which every variable appears at most once.  This condition is preserved by reduction and it is immediate to see that the size of affine terms strictly decreases with each reduction step.  Therefore, the untyped affine lambda-calculus is strongly normalizing.More interesting examples (in terms of expressiveness) are given by the so-called light lambda-calculi, arising from the subsystems of linear logic introduced by Girard in Light Linear Logic (Information and Computation 143, 1998), as well as Lafont's Soft Linear Logic (Theoretical Computer Science 318, 2004).  There are several such calculi in the literature, perhaps a good reference is Terui's Light affine lambda calculus and polynomial time strong normalization (Archive for Mathematical Logic 46, 2007).  In that paper, Terui defines a lambda-calculus derived from light affine logic and proves a strong normalization result for it.  Even though types are mentioned in the paper, they are not used in the normalization proof.  They are useful for a neat formulation of the main property of the light affine lambda-calculus, namely that the terms of a certain type represent exactly the Polytime functions.  Similar results are known for elementary computation, using other light lambda-calculi (Terui's paper contains further references).As a side note, it is interesting to observe that, in proof-theoretic terms, the affine lambda-calculus corresponds to intuitionistic logic without the contraction rule.  Grishin observed (before linear logic was introduced) that, in the absence of contraction, naive set theory (i.e., with unrestricted comprehension) is consistent (i.e., Russel's paradox does not give a contradiction).  The reason is that cut-elimination for naive set-theory without contraction may be proved by a straightforward size-decreasing argument (as the one I gave above) which does not rely on the complexity of formulas.  Via the Curry-Howard correspondence, this is exactly the normalization of the untyped affine lambda-calculus.  It is by translating Russel's paradox in linear logic and by tweaking the exponential modalities so that no contradiction could be derived that Girard came up with light linear logic.  As I mentioned above, in computational terms light linear logic gives a characterization of the polynomial-time computable functions.  In proof-theoretic terms, a consistent naive set theory may be defined in light linear logic such that the provably total functions are exactly the polynomial-time computable functions (there is another paper by Terui on this, Light affine set theory: A naive set theory of polynomial time,Studia Logica 77, 2004).