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?
$\begingroup$
$\endgroup$
1
-
6$\begingroup$ 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. $\endgroup$– Martin BergerCommented Dec 29, 2013 at 18:59
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
5
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).
answered Dec 30, 2013 at 2:03
-
$\begingroup$ 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. $\endgroup$ Commented Dec 30, 2013 at 9:03
-
$\begingroup$ @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. $\endgroup$ Commented Dec 30, 2013 at 14:55
-
$\begingroup$ 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). $\endgroup$ Commented Dec 30, 2013 at 15:15
-
$\begingroup$ 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. $\endgroup$ Commented Dec 30, 2013 at 17:15
-
$\begingroup$ ...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). $\endgroup$ Commented Dec 31, 2013 at 2:52
$\begingroup$
$\endgroup$
2
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.
-
1$\begingroup$ Something is at odds, as $m$ does not appear in the conclusion. $\endgroup$ Commented Jan 4, 2014 at 8:18
-
$\begingroup$ 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. $\endgroup$ Commented Jan 9, 2014 at 16:25
$\begingroup$
$\endgroup$
1
Here's a fun one, by Neil Jones and Nina Bohr:
Call-by-value Termination in the Untyped $\lambda$-calculus
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".
