<p>The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for.</p>

<p>If you use the <em>strict</em> lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser's paper):</p>

<blockquote>
  <p>If $B$ is a normal form of $A$, then there is a number $m$ such that any sequence of reductions starting from $A$ will lead to $B$ [modulo alpha equivalence] after at most $m$ reductions.</p>
</blockquote>

<p>Thus, even though you can write non-terminating terms in the (untyped) strict lambda calculus,  every term with a normal form normalizes strongly; that is, every sequence of reductions will reach that unique normal form.</p>

CC BY-SA 3.0
2014-01-04T08:18:49.677Z
Something is at odds, as $m$ does not appear in the conclusion.
Andrej Bauer
CC BY-SA 3.0
2014-01-09T16:25:52.827Z
Finished the theorem statement this time around, thanks. The part I wrote as [modulo alpha equivalence] was originally "(to within applications of Rule I)" which means the same thing unless I don't recall Rule I correctly.
Rob Simmons
CC BY-SA 3.0
2013-12-30T01:20:05.163Z
2014-01-09T16:24:36.273Z
2014-01-09T16:24:36.273Z
Rob Simmons
<p>Here's a fun one, by Neil Jones and Nina Bohr:</p>

<p><a href="http://www.lmcs-online.org/ojs/viewarticle.php?id=333&amp;layout=abstract">Call-by-value Termination in the Untyped $\lambda$-calculus</a></p>

<p>It shows how to apply the <em>size-change analysis</em> (a type of control flow analysis that detects infinite loops) on untyped $\lambda$-terms. This is quite nice in practice, but of course is restricted to $\lambda$-terms without defined constants (though the method may be extended to more general use).</p>

<p>The advantage of typing, of course is both the low complexity cost and the modularity of the approach: in general termination analyses are very non-modular, but typing can be done "piece-by-piece".</p>

CC BY-SA 3.0
2014-01-03T22:56:55.337Z
That's really interesting!
MaiaVictor
CC BY-SA 3.0
2014-01-03T20:07:02.277Z
2014-01-03T20:07:02.277Z
cody
<p>I can think of a few possible answers coming from linear logic.</p>

<p>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.</p>

<p>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).</p>

<p>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).</p>

CC BY-SA 3.0
2013-12-30T09:03:16.817Z
I would say Terui's Light Affine Lambda Calculus is typed, given the restrictions on affine variable usage, let-operators being stratified and the monoidalness of the !-operator. It's just that these restrictions are introduced informally. Girard's LLL is also typed.
Martin Berger
CC BY-SA 3.0
2013-12-30T14:55:02.243Z
@Martin: I disagree.  The structural constraints imposed on light affine terms are of a different nature than those of a typing system.  The biggest difference is that typing is necessarily inductive whereas well-formation (i.e., stratification, affine usage, etc.) may be defined as a combinatorial property of a term.  So, for example, when you type a term you usually have to type its subterms, whereas a subterm of a stratified term need not be stratified.
Damiano Mazza
CC BY-SA 3.0
2013-12-30T15:15:30.297Z
Sorry, one more thing about Girard's LLL: the system is obviously typed because it involves formulas.  However, as I mentioned in my answer, formulas play no role at all in LLL cut-elimination.  In fact, arbitrary fixpoints of formulas may be added (including Russel's paradoxical formula, which is equivalent to its own negation!) without LLL becoming inconsistent.  This is because cut-elimination holds for "purely structural" reasons, independently of the fact that you can attach types to your proofs (technically, the cut-elimination theorem for LLL may be proved in untyped proof nets).
Damiano Mazza
CC BY-SA 3.0
2013-12-30T17:15:48.643Z
OK, if you make inductiveness a condition of something being
a typing system. That's an interesting viewpoint that I had not come
across before.
Martin Berger
CC BY-SA 3.0
2013-12-31T02:52:25.783Z
...and it's a viewpoint I would say is misguided. For example, in systems involving subtyping (more generally, when considering an *extrinsic* interpretation of types in the sense of Reynolds) it is very natural to take a coinductive view of typing. There are quite a few examples in the literature (though I think this is underappreciated).
Noam Zeilberger
CC BY-SA 3.0
2013-12-30T02:03:47.807Z
2013-12-30T02:03:47.807Z
Damiano Mazza
<p>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?</p>

CC BY-SA 3.0
2013-12-29T18:59:36.510Z
The question is a bit unfocused: what do you mean by "similar to"? Are finite state automata similar? The $\lambda$-calculus is an universal model of computation, so anything that is 'similar' to it will probably feature non-terminating forms of computation.
Martin Berger
<pl.programming-languages><computability><lambda-calculus><functional-programming>
How to make the Lambda Calculus strong normalizing without a type system?
MaiaVictor
# How to make the Lambda Calculus strong normalizing without a type system?

(Asked by: username_0 on 2013-12-29)

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?

**Tags:** pl.programming-languages, computability, lambda-calculus, functional-programming

> **Comments:**
> **username_1**: The question is a bit unfocused: what do you mean by "similar to"? Are finite state automata similar? The $\lambda$-calculus is an universal model of computation, so anything that is 'similar' to it will probably feature non-terminating forms of computation.  

---

## 3 answers

### Answer by username_5 on 2013-12-30. Score: 24 | Accepted answer

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).

> **Comments:**
> **username_1**: I would say Terui's Light Affine Lambda Calculus is typed, given the restrictions on affine variable usage, let-operators being stratified and the monoidalness of the !-operator. It's just that these restrictions are introduced informally. Girard's LLL is also typed.  
> **username_5**: @Martin: I disagree.  The structural constraints imposed on light affine terms are of a different nature than those of a typing system.  The biggest difference is that typing is necessarily inductive whereas well-formation (i.e., stratification, affine usage, etc.) may be defined as a combinatorial property of a term.  So, for example, when you type a term you usually have to type its subterms, whereas a subterm of a stratified term need not be stratified.  
> **username_5**: Sorry, one more thing about Girard's LLL: the system is obviously typed because it involves formulas.  However, as I mentioned in my answer, formulas play no role at all in LLL cut-elimination.  In fact, arbitrary fixpoints of formulas may be added (including Russel's paradoxical formula, which is equivalent to its own negation!) without LLL becoming inconsistent.  This is because cut-elimination holds for "purely structural" reasons, independently of the fact that you can attach types to your proofs (technically, the cut-elimination theorem for LLL may be proved in untyped proof nets).  
> **username_1**: OK, if you make inductiveness a condition of something being a typing system. That's an interesting viewpoint that I had not come across before.  
> **username_6**: ...and it's a viewpoint I would say is misguided. For example, in systems involving subtyping (more generally, when considering an *extrinsic* interpretation of types in the sense of Reynolds) it is very natural to take a coinductive view of typing. There are quite a few examples in the literature (though I think this is underappreciated).  

---

### Answer by username_2 on 2013-12-30. Score: 13

The original paper by Church and Rosser, "Some Properties of Conversion," describes something that may be an example of what you're looking for.

If you use the *strict* lambda calculus, where in every occurrence of $\lambda x.M$ you have that $x$ appears free in $M$, then without a type system the following property holds (it's Theorem 2 in Church and Rosser's paper):

> If $B$ is a normal form of $A$, then there is a number $m$ such that any sequence of reductions starting from $A$ will lead to $B$ [modulo alpha equivalence] after at most $m$ reductions.

Thus, even though you can write non-terminating terms in the (untyped) strict lambda calculus, every term with a normal form normalizes strongly; that is, every sequence of reductions will reach that unique normal form.

> **Comments:**
> **username_3**: Something is at odds, as $m$ does not appear in the conclusion.  
> **username_2**: Finished the theorem statement this time around, thanks. The part I wrote as [modulo alpha equivalence] was originally "(to within applications of Rule I)" which means the same thing unless I don't recall Rule I correctly.  

---

### Answer by username_4 on 2014-01-03. Score: 11

Here's a fun one, by Neil Jones and Nina Bohr:

[Call-by-value Termination in the Untyped $\lambda$-calculus](http://www.lmcs-online.org/ojs/viewarticle.php?id=333&layout=abstract)

It shows how to apply the *size-change analysis* (a type of control flow analysis that detects infinite loops) on untyped $\lambda$-terms. This is quite nice in practice, but of course is restricted to $\lambda$-terms without defined constants (though the method may be extended to more general use).

The advantage of typing, of course is both the low complexity cost and the modularity of the approach: in general termination analyses are very non-modular, but typing can be done "piece-by-piece".

> **Comments:**
> **username_0**: That's really interesting!  

---

