(will be inserted by the editor)
Kazushige Terui
Light Aﬃne Lambda Calculus and Polynomial Time Strong Normalization
Received: date / Revised version: date – cSpringerVerlag 2004
Abstract. Light Linear Logic(LLL) andIntuitionistic Light Aﬃne Logic(ILAL) are logics that capture polynomial time computation. It is known that every poly nomial time function can be represented by a proof of these logics via the proofs asprograms correspondence. Furthermore, there is a reduction strategy which normalizes a given proof in polynomial time. Given the latter polynomial time
“weak” normalization theorem, it is natural to ask whether a “strong” form of polynomial time normalization theorem holds or not.
In this paper, we introduce an untyped term calculus, called Light Aﬃne Lambda Calculus(λla), which corresponds toILAL.λlais a bimodalλcalculus with certain constraints, endowed with very simple reduction rules. The main property ofλlais the polynomial time strong normalization:anyreduction strat egy normalizes a givenλlaterm in a polynomial number of reduction steps, and indeed in polynomial time. Since proofs ofILAL are structurally representable by terms ofλla, we conclude that the same holds forILAL.
1. Introduction
In [9], Girard introducedLight Linear Logic(LLL) as an intrinsically poly time logical system: every polynomial time function is representable by an LLL proof, and every LLL proof (of lazy conclusions) is normalizable in polynomial time. Later on, Asperti [1] introduced a simpliﬁed system, called Light Aﬃne Logic, by adding the full (unrestricted) weakening rule toLLL.
Its intuitionistic fragment (ILAL) has been particularly well investigated (see [2]), because it allows a compact term notation for proofs and has clear relevance to functional programming issues.
Light Logics provide animplicitcharacterization of polynomial time; in contrast with their precursor,Bounded Linear Logic[10], the syntax of Light Logics do not contain any polynomials. Moreover, the characterization is purely logical; in contrast with those implicit characterizations of polynomial time which are mostly based on safe recursion or data ramiﬁcation (see [6, Kazushige Terui: National Institute of Informatics, 212 Hitotsubashi, Chiyoda ku, 1018430 Tokyo, Japan. email:terui@nii.ac.jp
This is a full version of the paper [21] presented at LICS 2001.
Key words or phrases:Light logics – Lambda calculus – Polynomial time
14, 13, 11, 7]), Light Logics do not contain any builtin data types, and the characterization result is about the complexity of cutelimination, which is of purely logical nature. It naturally extends to a consistent naive set theory, in which one can reason about polynomial time concepts [9, 23].
Also notably, Light Logics are endowed with various semantics [12, 3, 16], which could lead to a semantic understanding of polynomial time.
An important problem remains to be settled, however. By inspecting the normalization theorem given by [9], one observes that what is actually shown is the polynomial timeweak normalization, namely, that there is a speciﬁc reduction strategy which normalizes a givenLLLproof in polynomial time.
The same is true of ILAL [1, 2]. It has been left unsettled whether the polynomial timestrongnormalization holds for these Light Logics, namely, whetheranyreduction strategy normalizes a given proof in polynomial time.
The primary purpose of this paper is to give a solution to this problem.
Having such a property will be theoretically important in that it gives further credence to Light Logics as intrinsically polytime systems. It will be practically important, too. Through the CurryHoward correspondence, the proofs of Light Logics may be considered asfeasible programs. In this context, the property will ensure that the programs can be executed in polynomial timeindependent ofevaluation strategies.
For our purpose, it is reasonable to begin with ILAL, because it is simpler than LLL as a logical system. However, the existing term calculi proposed for ILAL either have a complicated notion of reduction deﬁned by more than 20 rewriting rules [1, 20], or involve notational ambiguity [19, 2]^{1}. Therefore, it is desirable to have a simple and accurate term calculus for ILAL. Such a simple calculus will provide a clearer intuition on the computational aspect of Light Logics. That is our secondary purpose^{2}.
In this paper, we introduce a new term calculus, called Light Aﬃne Lambda Calculus(λla) (in Section 2). It amounts to a simple modiﬁcation ofλcalculus with modal and let operators. The main advantage of λla is operational simplicity; it has only ﬁve reduction rules and each rule has a clear meaning. Although λla is untyped, all the wellformed terms are normalizing. We then reintroduceILALas a Currystyle type assignment system for λla and prove the subject reduction theorem (in Section 3).
There are a number of reasons for adopting a Currystyle presentation:
1. First of all, to design a truly polytime (rather than just polystep) poly morphic calculus, one has to give up a Churchstyle term syntax with embedded types: a universal quantiﬁer may bind an arbitrary number
1 See the remark in Section 9.1 of [2]. To compensate this ambiguity, the latter paper presents a proofnet syntax forILAL.
2 Another approach is to identify a wellbehaved fragment ofILALfor which the ordinary lambda calculus works perfectly well. This line of research is pursued by [4].
of type variable occurrences, and thus iterated type instantiations (Λ reductions) may easily cause exponential growth in the size of types.^{3} 2. An untyped polytime calculus deserves investigation in its own right.
3. The notion of wellformedness, rather than typability, neatly captures the syntactic condition for polynomial time normalizability.
4. Last but not least, typability inILALis presumably intractable^{4}, while wellformedness can be checked very easily (in quadratic time).
In this setting, we prove our main theorems (in Sections 4 and 5):
– The Polystep Strong Normalization Theorem: every reduction sequence in λla has a length bounded by a polynomial in the size of the initial term (when the term depth is ﬁxed).
– The Polytime Strong Normalization Theorem: every reduction strategy (given as a function oracle) induces a normalization procedure which terminates in polynomial time.
Since proofs of ILAL are structurally representable by terms of ILAL (where formulas are erased), we can conclude that the same theorem holds forILAL.
We ﬁnally discuss some related issues, such as the relationship with the safe recursion approach, polynomial time strong normalization for LLL, a lowerbound for normalization and decision problems for type inference (in Section 6).
2. Light Aﬃne Lambda Calculus
In this section, we presentλla. We begin by introducing the pseudoterms and several basic notions in 2.1, then move on to the wellformed terms in 2.2. Finally, the reduction rules are given in 2.3.
2.1. PseudoTerms
Letx, y, z . . .range over term variables.
Deﬁnition 1.The setPT ofpseudotermsis deﬁned by the following gram mar:
t, u::=xλx.t tu!t let!x=uint  §t let§x=uint.
In addition toλabstraction and application, we have two modal opera tors (!,§) and twoletoperators (let!,let§). Pseudoterms !tand§tare called
!boxand§boxrespectively. It is suggestive to think of them as “boxes” in the literal sense:
3 Proofnets (ofLLL) contain formulas. Hence proofnets themselves are not nor malizable in polynomial time. A solution suggested by [9] is to work with untyped proofnets (with formulas erased) in the actual computation. When the conclusion is lazy, the formulas can be automatically recovered after normalization, and such formulas are not exponentially large. Our approach is essentially the same, but we start by a typefree setting, then consider typing afterwards.
4 The problem is undecidable for System F in the Curry style [24].
x.let !x be !y in yy
let !x be !y in yy
!x λ
yy
x y y
ε 0
00 01
011 010 000
Fig. 1.Term Tree and Addresses
! t § t.
With boxes thus drawn, each pseudoterm is stratiﬁed into layers. For in stance, (let!x=!y in§!(λz.zx))zis stratiﬁed into three layers as follows:
(let!x=! y in§ ! λz.zx )w.
In the sequel, symbol † stands for either ! or §. Pseudoterms (λx.t) and (let †x = uint) bind each occurrence of x in t. As usual, pseudoterms are considered up toαequivalence, and subject to thevariable convention;
namely, the bound variables are chosen to be diﬀerent from the free vari ables, so that variable clash is never caused by substitution. The notation t[u/x] denotes the pseudoterm obtained by substituting ufor the free oc currences of x in t. F V(t) denotes the set of free variables in t. F O(x, t) denotes the number of free occurrences of x in t, and F O(t) denotes the number of all free variable occurrences int.
Each pseudotermtcan be represented as aterm tree, and each subterm occurrence u in t can be pointed by its address, i.e., a word w ∈ {0,1}^{∗} which describes the path from the root to the node corresponding to uin the term tree. For example, the term tree for (λx.let!y=!xin yy) and the addresses in it are illustrated in Figure 1. We writewvwhenwis a preﬁx ofv.
Thesizet of a pseudotermtis the number of nodes in its term tree.
Since pseudoterms are untyped, t is not signiﬁcantly diﬀerent from the length of the string representation oft. Given a pseudotermtand an address w, the depthof w in t is the number of !boxes and§boxes enclosing the subexpression atw. The depthof tis the maximum depth of all addresses in it.
AcontextΦis a pseudoterm with a hole •. If Φis a context andt is a pseudoterm, thenΦ[t] denotes the pseudoterm obtained by substitutingt for•in Φ.
2.2. WellFormed Terms
The wellformed terms are obtained by imposing certain conditions on the pseudoterms. To begin with, let us give an informal description.
First, the base of our calculus isaﬃne: eachλmay bind at most one free variable. That is to say,λis in charge of abstraction and cancellation, but not of duplication. Moreover, theλbinding relation may not cross a box.
For instance, the binding below is not allowed:
λx. ! xt
The eﬀect is thatλ and !components do not interleave each other.
Second, let operators must respect stratiﬁcation: for each pair of a let operator and a variable it binds, the binding relation must crossexactly one box, as follows:
let!x=t in§ xxy ! xu
To see why this condition is needed, deﬁne ω_{1}≡λx.(let!y=xin y!y), ω_{2}≡λx.(let!y=xin !(y(!y)).
These pseudoterms clearly violate the above condition; in ω_{1} the binding relation indicated below does not cross a box, while inω_{2} the one indicated below crosses two boxes.
λx.(let!y =xiny! y ) λx.(let!y=xin! y! y )
These terms causes nontermination of reductions. In fact, anticipating the reduction rules in Figure 2, we see that the following pseudoterms are not normalizing:
ω_{1}!ω_{1}−→^{(β)} let!y=!ω_{1} iny!y
−→(!) ω_{1}!ω_{1}−→ · · · ω_{2}!ω_{2}−→^{(β)} let!y=!ω_{2} in!(y!y))
−→(!) !(ω_{2}!ω_{2})−→ · · ·
Note that the above condition reﬂects the lack of the dereliction and diggingprinciples in Light Logics:
– Dereliction: !A−◦A, – Digging: !A−◦!!A.
Third, a !box may contain at most one free variable. This is to rule out a pseudoterm like
2≡λx.(let!y=xin ! yy ),
which causes an exponential explosion:
2^{n}(!z) −→^{(β)} 2^{n−1}(let!y=!zin !yy)
−→(!) 2^{n−1}(!zz)
−→(β) 2^{n−2}(let!y=!zzin!yy)
−→(!) 2^{n−2}(!(zz)(zz))
−→^{∗}!(zz · · · ·z
2^{n} times
).
This condition intuitively means that a !box is to be duplicated, but not to duplicate another !box. It reﬂects the lack of themonoidalnessin Light Logics (which distinguishes Light Logics fromElementary Logics[9, 8]):
– Monoidalness: !A⊗!B−◦!(A⊗B).
Since the last condition is too severe, we need another modal operator
§ as a compensation. A §box may contain an arbitrary number of free variables. Instead,let§may not bind more than one free variable. In other words, a §box is to duplicate something, but not to be duplicated. Two modalities ! and §are related by the following conditions: a let! operator may bind a free variable in a §box (corresponding to the weak dereliction principle !A−◦ §Athat holds in Light Logics), whereas alet§operator may not bind a free variable in a !box.
Let us now give a formal deﬁnition. Here, it is convenient to classify variables into three groups:undischarged, !discharged, and§dischargedvari ables. These are to be bound byλabstraction,let! operator and let§op erator, respectively. In the sequel,stands for disjoint union.
Deﬁnition 2.Let X, Y, Zrange over the ﬁnite sets of variables. The 4ary relation t ∈ TX,Y,Z (saying that t is a wellformed term with undischarged variables from X, !discharged variables from Y and§discharged variables from Z) is deﬁned as follows (in writing t∈ TX,Y,Z, we implicitly assume that X,Y andZ are mutually disjoint):
1.x∈ T_{X,Y,Z} ⇐⇒ x∈X.
2.λx.t∈ TX,Y,Z ⇐⇒t∈ T_{X{x},Y,Z}, F O(x, t)≤1.
3.tu∈ TX,Y,Z ⇐⇒ t∈ TX,Y,Z, u∈ TX,Y,Z. 4.!t∈ TX,Y,Z ⇐⇒ t∈ T_{Y,∅,∅}, F O(t)≤1.
5.§t∈ TX,Y,Z ⇐⇒ t∈ T_{Y}_{Z,∅,∅}.
6.let!x=tin u∈ TX,Y,Z ⇐⇒ t∈ TX,Y,Z, u∈ T_{X,Y}_{{x},Z}.
7.let§x=t inu∈ TX,Y,Z ⇐⇒t∈ TX,Y,Z, u∈ T_{X,Y,Z{x}}, F O(x, u)≤1.
We say thattis a wellformed term, or simply aterm, ift∈ TX,Y,Z for someX, Y andZ.
Note that clause 2 above embodies the aﬃnity ofλabstraction, clause 4 embodies the nomorethanonevariable condition on !boxes. In the mean time, the statement 3 of the next lemma ensures that the stratiﬁcation condition on ! and§ boxes is satisﬁed.
Lemma 1.Let t∈ TX,Y,Z.
1. IfX ⊆X^{},Y ⊆Y^{} andZ⊆Z^{}, then t∈ TX^{},Y^{},Z^{}. 2. Ifx∈F V(t), then t∈ T_{X\{x},Y}_{\{x},Z\{x}}.
3. Letx∈F V(t). Thenxoccurs at depth 0 iﬀ x∈X.xoccurs at depth 1 iﬀx∈Y ∪Z.xnever occurs at depth>1.
Proof. By induction ont.
Lemma 2. (Substitution)
1.t∈ T_{X{x},Y,Z} andu∈ TX,Y,Z =⇒t[u/x]∈ TX,Y,Z.
2.t∈ T_{X,Y}_{{x},Z},u∈ T_{Y,∅,∅} andF O(u)≤1 =⇒t[u/x]∈ TX,Y,Z. 3.t∈ T_{X,Y,Z{x}} andu∈ T_{Y}_{∪Z,∅,∅} =⇒t[u/x]∈ TX,Y,Z.
Proof. By induction ont.
Example 1.We writeλ^{!}x.tto denoteλx.let!y=xint[y/x] withy fresh.
1. While ω_{1} and ω_{2} in the previous subsection are not wellformed,ω_{3} ≡ λx.(let!y=xin§yy) is wellformed.
2. For each natural number n, we haveChurch numeral n∈ T deﬁned by n≡λ^{!}x.§λz.(x· · ·(x
n times
z)· · ·).
3. For each wordw≡i_{0}· · ·i_{n} ∈ {0,1}^{∗}, we havew∈ T deﬁned by w≡λ^{!}x_{0}.λ^{!}x_{1}.§λz.(xi0· · ·(x_{i}_{n}z)· · ·).
Observe thatn’s andw’s are of depth 1.
4.Suc≡λn.λ^{!}f.let§h=n!f in§λy.f(hy)∈ T.
Remark 1.As discussed in Section 3 of [1], a naive use of box notation causes ambiguity, and in conjunction with naive substitution, it causes a disastrous eﬀect on complexity.
While Asperti solved this problem by using a more sophisticated box notation§(t)[u1/x_{1}, . . . , u_{n}/x_{n}], our solution is more implicit and based on a conceptual distinction between discharged and undischarged variables.
Asperti’s box§(tx1x_{2})[y/x_{1}, y/x_{2}] (withy of !type) corresponds to (let!x=y in§(txx)) in our syntax. Observe that variabley, which is exter nal to the§box, is shared in the former, while variablex, which is internal to the §box, is shared in the latter. This is parallel to the diﬀerence be tween the contraction inference rule of Asperti’sILALand that of Girard’s LLL; the former contracts !formulas, while the latter contracts discharged formulas.
Remark 2.There is a quadratic time algorithm for wellformedness checking.
Let t be a pseudoterm, and X and Y be the sets of its free variables at depth 0 and at depth 1, respectively. Thentis wellformed iﬀt∈ T_{X,Y,∅}(by Lemma 1 and the fact thatt∈ TX,Y,Z impliest∈ T_{X,Y}_{∪Z,∅}). The latter can be recursively checked with at mosttrecursive calls, and each call involves a variable occurrence check at most once (corresponding to Clauses 2, 4 and 7 of Deﬁnition 2). Therefore the algorithm runs in timeO(n^{2}), given a term of sizen.
Name Redex Contractum
(β) (λx.t)u t[u/x]
(§) let§x=§uint t[u/x]
(!) let !x=!uint t[u/x]
(com) (let †x=uint)v let †x=uin(tv) let †y= (let †x=uint)invlet †x=uin(let †y=tinv)
Fig. 2.Reduction Rules
2.3. Reduction Rules
Deﬁnition 3.The reduction rules of λla are given in Figure 2. We say that t reduces to u at address w by rule (r), and write as t −−−→^{w,(r)} u, if t≡Φ[v_{1}],u≡Φ[v_{2}], the hole• is located at winΦ, and v_{1} is an(r)redex whose contractum isv_{2}.
Note that the address w uniquely determines the rule (r) to be used.
When the address w or the rule (r), or both, are irrelevant, we write as t −−→^{(r)} u,t −→^{w} uand t −→u, respectively. Thedepth of a reduction is the depth of its redex.
A ﬁnite sequence σ of addresses w_{0}, . . . , w_{n−1} is said to be a reduc tion sequencefromt_{0} tot_{n}, written as t_{0}−→^{σ} ^{∗}t_{n}, if there are pseudoterms t_{1}, . . . , t_{n−1}such that
t_{0}−−→^{w}^{0} t_{1}−−→ · · ·^{w}^{1} −−−→^{w}^{n−1} t_{n}.
If every reduction in σ is an application of rule (r), then σ is called an (r)reduction sequenceand written ast_{0}−−−→^{σ,(r)}^{∗} t_{n} (or simply ast_{0}−−→^{(r)}^{∗}t_{n}).
The length ofσis denoted by σ.
The wellformed terms are closed under reduction:
Proposition 1.If t∈ TX,Y,Z andt−→u, thenu∈ TX,Y,Z.
Proof. We prove the following by induction on Φ: if Φ[t] ∈ TX,Y,Z and Φ[t]→Φ[u], then
(1) Φ[u]∈ TX,Y,Z and
(2) F O(x, Φ[u])≤F O(x, Φ[t]) for everyx∈X∪Z.
WhenΦ≡ •and the reduction is of the form t≡let!x=!v_{1}in v_{2}−→^{(!)} v_{2}[v_{1}/x]≡u,
thenv_{2}∈ T_{X,Y}_{{x},Z},v_{1}∈ T_{Y,∅,∅}andF O(v_{1})≤1. Hencev_{2}[v_{1}/x]∈ TX,Y,Z
by Lemma 2. (2) is obvious since no variable inv_{1} belongs toX∪Z.
If Φ ≡ λy.Φ^{}, then Φ^{}[t] ∈ T_{X{y},Y,Z} and F O(y, Φ^{}[t]) ≤ 1. By the induction hypothesis, Φ^{}[u] ∈ T_{X{y},Y,Z} and F O(y, Φ^{}[u]) ≤1. Therefore λy.Φ^{}[u]∈ TX,Y,Z. (2) is obvious.
Other cases are similar.
(1)
ω3!ω3 (β)
−→(let!y=!ω3 in§yy)
−→ §ω(!) 3ω3
−→ §(β) (let!y=ω3 in§yy). (2)
(λ^{!}x.t)!u ≡ (λx.let!y=xint[y/x])!u
−→(β) let!y=!uint[y/x]
−→(!) t[u/x] (3)
Suc2 −→^{(β)} λ^{!}f.let§h= (λ^{!}x.§λz.x(xz))!f in§λy.f(hy)
−→^{∗}λ^{!}f.let§h=§λz.f(fz)in§λy.f(hy)
−→(§) λ^{!}f.§λy.f((λz.f(fz))y)
−→(β) λ^{!}f.§λy.f(f(fy))≡3
Fig. 3.Examples of normalization
Example 2.
1. We have seen in Example 1 that the termω_{3}≡λx.(let!y=xin §yy) is wellformed. In contrast to ω_{1}!ω_{1} and ω_{2}!ω_{2} described before, ω_{3}!ω_{3} is normalizing (or better, deadlocking). See Figure 3 (1).
2. (λ^{!}x.t)!ureduces tot[u/x] as in Figure 3 (2).
3. The termSuc in Example 1 surely represents the successor for Church numerals. In fact, the term Suc 2 reduces to 3, as illustrated in Fig ure 3 (3).
Remark 3.The stratiﬁed structure of a term is strictly preserved by reduc tion. In particular, the depth of a term never increases, since in reduction rules (β), (§) and (!) a subterm uis substituted for a variablexoccurring at the same depth, and (com) does not aﬀect the stratiﬁed structure.
Reduction rules (β) and (§) are strictly sizedecreasing, since they never involve duplication. (com) preserves the size. The only reduction rule that is potentially sizeincreasing is (!). Nevertheless, it is also strictly size decreasing at the depth where the redex is located. The size increases only at deeper layers.
3. Type Assignment
The purpose of this section is to present Intuitionistic Light Aﬃne Logic (ILAL) as a type assignment system for λla and to prove the subject reduction theorem.
In 3.1, we introduce ILAL in a sequent calculus style. It is, however, diﬃcult to prove the subject reduction theorem directly for it. The main diﬃculty is that it does not satisfy the subterm typability. To overcome this, we introduce a natural deduction systemILAL_{N} in 3.2. It is equivalent to ILALas far asclosedterms are concerned, and it does satisfy the subterm typability. Once having deﬁned the suitable formalism ILAL_{N}, it is easy to prove the subject reduction theorem. This is accomplished in 3.3.
3.1. ILAL as a Type Assignment System Letα, βrange over the type variables.
Deﬁnition 4.The types (formulas) of ILAL are given by the following grammar:
A, B::=α A−◦B  ∀α.A!A  §A.
A !discharged type is an expression of the form [A]_{!}. A§discharged type is an expression of the form[A]_{§}.
In the sequel,†^{n}A abbreviates † · · · †
n times
A.
A declaration is an expression of the form x:A or x: [A]_{†}. A ﬁnite set of declarations is denoted byΓ, ∆, etc. LetΓ be a set of declarations x_{1}:A_{1}, . . . , x_{n}:A_{n} in which all types are undischarged. Then [Γ]_{†} denotes x_{1}: [A_{1}]_{†}, . . . , x_{n}: [A_{n}]_{†}. IfΓ contains a declaration with a discharged type, then [Γ]_{†} is undeﬁned.
Deﬁnition 5.The type inference rules of ILAL are given in Figure 4. A pseudotermt is typablein ILAL if Γ t:A is derivable for some Γ and A by those inference rules. Likewise, a pseudotermt isof typeA ift:A is derivable.
As expected, we have:
Proposition 2.Every typable pseudoterm is a term. More exactly, if−→x:
−
→A ,−→y :−→
[B]_{!},−→z :−→
[C]_{§}t:D,is derivable, then t∈ T_{{−}^{→}_{x}_{},{−}^{→}_{y}_{},{−}^{→}_{z}_{}}.
Proof. By induction on the length of the typing derivation. In the case of (Cut) and (−◦l), apply Lemma 2(1).
Example 3.Let int ≡ ∀α.!(α−◦α)−◦ §(α−◦α) and bint ≡ ∀α.!(α−◦
α)−◦!(α−◦α)−◦ §(α−◦α). Then we have n:int for each n ∈ N and w:bintfor eachw∈ {0,1}^{∗}.
x:Ax:A Id Γ1u:A x:A, Γ2t:C Γ1, Γ2 t[u/x] :C Cut
Γ t:C
∆, Γt:C W eak x: [A]_{!}, y: [A]_{!}, Γt:C z: [A]_{!}, Γt[z/x, z/y] :C Cntr Γ1u:A1 x:A2, Γ2t:C
Γ1, y:A1−◦A2, Γ2t[yu/x] :C −◦l x:A1, Γ t:A2
Γ λx.t:A1−◦A2 −◦r x:A[B/α], Γ t:C
x:∀α.A, Γ t:C ∀l Γ t:A
Γ t:∀α.A ∀r, (αis not free inΓ) x: [A]_{!}, Γt:C
y:!A, Γlet!x=yint:C !l x:Bt:A x: [B]_{!}!t:!A !r x: [A]_{§}, Γt:C
y:§A, Γ let§x=yint:C §l Γ, ∆t:A [Γ]_{!},[∆]_{§} §t:§A §r In rule (!r),x:B can be absent. In rule (§r),Γ and∆can be empty.
Fig. 4.Type Assignment SystemILAL
An example of an untypable wellformed term isω_{3}!ω_{3}. To see the reason, deﬁne the erasureof a λla term to be a λterm obtained by applying the following operations as much as possible:
†u→u, let †x=uint→t[u/x].
As easily seen, if a term is typable in ILAL, then its erasure is typable in System F (in the Curry style). Now, ω_{3}!ω_{3} cannot be typed in ILAL, because its erasure is (λx.xx)(λx.xx), a term which cannot be typed in System F.
Remark 4.Unlike the ordinaly lambda calculus,λladoes not need types to ensure normalization. Nevertheless, types are useful in several ways:
–Types are used to avoiddeadlocks, such as (†t)uandlet †x= (λx.t)inu.
–Some types, typically data types such as int and bint, constrain the shape of normal terms. For instance, all normal terms of typeintare of the formnfor somen≥0 (or λx.(let!z=xin §z), which may be seen as anηvariant of 1). More generally, all normal terms of type§^{k}intare of the form§^{k}n (or anηvariant of§^{k}1).
–Lazytypes, i.e., those which do not contain a negative occurrence of∀, constrain the depth of normal terms. If a termt is normal and of lazy typeA, then it means thatt:A can be derived without using the (∀l)
inference rule, which has an eﬀect of hiding some information on the derivation. Thus all uses of the ! and§inference rules in the derivation are recorded withinA. Hence the depth oft is necessarily bounded by the depth of A. Note that the standard data types such as int, bint, booleans and lists of booleans are all lazy.
–The above suggests that in order to normalize a term of lazy type of depthd, one does not have to take care of redices at depth> d, which will be removed anyway by reductions at lower depths before arriving at the normal form. In this way, lazy types help us detect redundant redices.
The expressive power ofILAL, hence ofλla, is witnessed by:
Theorem 1 (Girard[9], Roversi[19]). Every function f : {0,1}^{∗} −→
{0,1}^{∗} that is computable in polynomial time is represented by a term of typebint−◦ §^{d}bint for somed.
See [2] for a detailed exposition. Neergaard and Mairson [18] improve the above theorem by showing that a function inDT IM E[n^{k}] can be rep resented by a proofnet of depthO(logk). The converse will be taken up in Section 5.
3.2. Natural Deduction SystemILAL_{N}
ILAL does not satisfy the subterm typability; for example, §(xx) can be typed asx: [A]_{!} §(xx) :§AwithA≡ ∀α.α, but it is clear that its subterm xx cannot be typed. This makes diﬃcult to prove the subject reduction theorem directly for ILAL. For this reason, we introduce a type system ILAL_{N} in natural deduction style, which does satisfy the subterm typabil ity. Then we show that ILALand ILAL_{N} are equivalent as far as closed terms are concerned.
The inference rules ofILAL_{N} are given in Figure 5.
Lemma 3.If x:µ, Γ t:A is derivable in ILAL_{N} andx∈F V(t), where µis either a nondischarged or a discharged type, thenΓ t:Ais derivable inILAL_{N}. The same property holds forILAL, too.
Proof. By induction on the derivation.
Lemma 4.The following rules are derivable inILAL_{N}: Γ t:C
∆, Γ t:C (W eak) x: [A]_{!}, y: [A]_{!}, Γ t:C
z: [A]_{!}, Γ t[z/x, z/y] :C (Cntr) Γ u:A x:A, Γ t:C
Γ t[u/x] :C (Cut)
∆u:A x: [A]_{!},[∆]_{!}, Γ t:C F O(u)≤1 [∆]_{!}, Γ t[u/x] :C (Cut_{!})
x:A, Γx:A (Ax) Γ t:A−◦B Γ u:A
Γ tu:B (−◦E) x:A, Γt:B F O(x, t)≤1 Γ λx.t:A−◦B (−◦I) Γ t:∀α.A
Γ t:A[B/α] (∀E) Γ t:A α∈F V(Γ) Γ t:∀α.A (∀I) Γ u:!A x: [A]_{!}, Γt:B
Γ let!x=uint:B (!E) Γ t:A F O(t)≤1 [Γ]_{!}, ∆!t:!A (!I) Γ u:§A x: [A]_{§}, Γ t:B F O(x, t)≤1
Γ let§x=uint:B (§E) Γ, Σt:A
[Γ]_{!},[Σ]_{§}, ∆ §t:§A (§I) Fig. 5. Natural Deduction SystemILAL_{N}
∆, Π u:A x: [A]_{§},[∆]_{!},[Π]_{§}, Γ t:C
[∆]_{!},[Π]_{§}, Γ t[u/x] :C (Cut_{§}) Proof. (W eak) By induction on the derivation.
(Cntr) By induction on the derivation. Actually we show that contraction is derivable not only for !discharged formulas but also for nondischarged and§discharged formulas.
(Cut) By induction on the derivation ofx:A, Γ t:C.
(Cut_{!}) By induction on the derivation of x: [A]_{!},[∆]_{!}, Γ t :C. Let us show the critical case. Suppose thatt≡!t^{} and the last inference rule in the derivation is of the form:
x:A, ∆t^{} :C^{} F O(t^{})≤1 x: [A]_{!},[∆]_{!}, Γ !t^{} :!C^{} (!I)
.
By (Cut),∆t^{}[u/x] :Cis derivable inILAL_{N}. By assumption,F O(u)≤1 and F O(t^{}) ≤ 1, hence F O(t^{}[u/x]) ≤ 1. Therefore we can apply (!I) to obtain [∆]_{!}, Γ !t^{}[u/x] :!C^{}.
(Cut_{§}) By induction on the derivation ofx: [A]_{§},[∆]_{!},[Π]_{§}, Γ t:C.
Lemma 5.If Γ t:A is derivable in ILAL, then it is also derivable in ILAL_{N}.
Proof. By induction on the derivation, using derived rules (W eak), (Cntr) and (Cut) in Lemma 4.
Avariable substitutionis a functionθ from the set of term variables to itself. tθ denotes the term obtained by replacing each free variable x in t withθ(x).Γ θ denotes the set of declarations obtained fromΓ by replacing each variablexwithθ(x). It may decrease the number of declarations due
to uniﬁcation. For example, If Γ ≡x:A, y:A and θ(x) = θ(y) = z, then Γ θ≡z:A.
Lemma 6.Suppose thatΓ t:A is derivable in ILAL_{N}. Then there are Γ^{},t^{} and a variable substitution θ such that
–Γ^{}t^{}:A is derivable inILAL, –Γ^{}θ≡Γ andt^{}θ≡t.
Proof. By induction on the derivation. We only deal with several critical cases.
(Case 1) The last inference is (−◦E) of the form:
Γ t:A−◦B Γ u:A Γ tu:B (−◦E)
By the induction hypothesis, there areΓ_{1}^{},Γ_{2}^{}, t^{}, u^{} and variable substitu tionsθ_{1}andθ_{2} such that
– Γ_{1}^{}t^{}:A−◦B andΓ_{2}^{} u^{}:Aare derivable inILAL, – Γ_{1}^{}θ_{1}≡Γ_{2}^{}θ_{2}≡Γ,t^{}θ_{1}≡tand u^{}θ_{2}≡u.
Without loss of generality, we may assume that F V(Γ_{1}^{}) andF V(Γ_{2}^{}) are disjoint. From these, Γ_{1}^{}, Γ_{2}^{} t^{}u^{} :B is derivable in ILAL. A suitable variable substitutionθ is deﬁned by
θ(x) =θ_{1}(x), ifx∈F V(Γ_{1}^{});
=θ_{2}(x), otherwise.
(Case 2) The last inference is (−◦I) of the form:
x:A, Γ t:B F O(x, t)≤1 Γ λx.t:A−◦B (−◦I)
By the induction hypothesis, there arex_{1}:A, . . . , x_{n}:A,Γ^{},t^{}and a variable substitutionθ such that
– x_{1}:A, . . . , x_{n}:A, Γ^{}t^{}:B is derivable inILAL, – θ(x_{1}) =· · ·=θ(x_{n}) =x,Γ^{}θ≡Γ andt^{}θ≡t.
Since F O(x, t) ≤ 1, there is at most one x_{i} such that x_{i} ∈ F V(t^{}). By Lemma 3,x_{i}:A, Γ^{}t^{}:B is derivable inILAL. Renamex_{i} asx. Then we can apply (−◦r) to deriveΓ^{}λx.(t^{}[x/x_{i}]) :A−◦Bin ILAL.
(Case 3) The last inference is (!E) of the form:
Γ u:!A x: [A]_{!}, Γ t:B Γ let!x=uint:B (!E)
By the induction hypothesis, there are Γ_{1}^{},x_{1}: [A]_{!}, . . . , x_{n}: [A]_{!}, Γ_{2}^{}, t^{}, u^{} and variable substitutionsθ_{1} andθ_{2} such that
– Γ_{1}^{}u^{} :!Aandx_{1}: [A]_{!}, . . . , x_{n}: [A]_{!}, Γ_{2}^{}t^{}:B are derivable inILAL, – θ(x_{1}) =· · ·=θ(x_{n}) =x,Γ_{1}^{}θ_{1}≡Γ_{2}^{}θ_{2}≡Γ,u^{}θ_{1}≡uandt^{}θ_{2}≡t.
We may assume that F V(Γ_{1}^{}), F V(Γ_{2}^{}) and {x_{1}, . . . , x_{n}} are disjoint. By (Cntr), (!l) and (Cut), Γ_{1}^{}, Γ_{2}^{} let!x=u^{} in(t^{}[x/x_{1}, . . . , x/x_{n}]) is deriv able inILAL. A suitable variable substitutionθcan be deﬁned as in (Case 1).
As a consequence, we obtain:
Theorem 2 (Equivalence between ILAL and ILAL_{N}).t:Ais deriv able inILAL if and only if it is derivable inILAL_{N}.
Proof. By Lemma 5 and Lemma 6.
3.3. Subject Reduction Theorem
We prove the subject reduction theorem forILAL_{N} by employing the tech nique described in [5]. The following deﬁnition is a reﬁnement of Deﬁnition 4.2.1 in [5].
For any setΓ of declarations, deﬁne a binary relation>_{Γ} on types by
∀α.A >_{Γ} A[B/α],
A >_{Γ} ∀α.A, ifα∈F V(Γ).
Denote the reﬂexive transitive closure of >_{Γ} by≥Γ. It is easy to see that wheneverΓ t:AandA≥Γ B,Γ t:B is derivable.
Lemma 7 (Generation lemma).The following hold for ILAL_{N}: 1.Γ x:A =⇒x:B∈Γ for someB≥Γ A.
2.Γ λx.t:A=⇒x:B, Γ t:Cfor someBandCsuch thatB−◦C≥Γ A, andF O(x, t)≤1.
3.Γ tu:A=⇒Γ t:B−◦C andΓ u:B for someB andC≥Γ A.
4.Γ let!x=uin t:A =⇒ Γ u:!B and x: [B]_{!}, Γ t:C for some B andC≥Γ A.
5.Γ !t:A =⇒ ∆ t:C for some C and ∆ such that !C ≥Γ A and [∆]_{!}⊆Γ, and F O(t)≤1.
6.Γ let§x=uin t:A =⇒ Γ u:§B and x: [B]_{§}, Γ t:C for some B andC≥Γ A, andF O(x, t)≤1.
7.Γ §t:A =⇒ ∆, Σ t:C for some C, ∆ andΣ such that §C ≥Γ A and[∆]_{!},[Σ]_{§}⊆Γ.
Proof. By induction on derivations. Note that (∀I) and (∀E) are the only inference rules that do not change the subjectt. These rules are handled by means of≥Γ.
Theorem 3 (Subject Reduction for ILAL_{N}). If Γ t:A is derivable inILAL_{N} andt−→u, thenΓ u:Ais derivable inILAL_{N}.
Proof. The proof is parallel to that of Proposition 1. We prove the following by induction on Φ: if Γ Φ[t] :Ais derivable in ILAL_{N} and Φ[t] →Φ[u], then
(1) Γ Φ[u] :A and
(2) F O(x, Φ[u]) ≤ F O(x, Φ[t]) for each x such that either x:A ∈ Γ or x: [A]_{§}∈Γ for someA.
Suppose thatΦ≡ • and the reduction is of the form t≡let!x=!v_{1}in v_{2}−→^{(!)} v_{2}[v_{1}/x]≡u.
By Generation Lemma (4) and (5), we have:
x: [B]_{!}, Γ v_{2}:Cfor some B andC≥Γ A,
∆v_{1}:Dfor some ∆andD such that [∆]_{!}⊆Γ andD≥Γ B.
From the latter, it follows that∆v_{1}:B. By (Cut_{!}) of Lemma 4, we derive Γ v_{2}[v_{1}/x] :C, and thusΓ v_{2}[v_{1}/x] :A. (2) is obvious, because any free variable inv_{1} is !discharged inΓ.
Whent is a (β) redex, argue as in the proof of Theorem 4.2.5 in [5].
Other cases are similar.
Corollary 1 (Subject Reduction for ILAL).If Γ t:Ais derivable in ILAL andt−→u, thenΓ u:Ais derivable in ILAL.
Proof. The general case is reducible to the case of closed terms, by using the following facts:
x:A, Γ t:B⇐⇒Γ λx.t:A−◦B
x: [A]_{†}, Γ t:B⇐⇒y:†A, Γ let †x=yin t:B.
Hence the corollary follows from Theorem 2 and Theorem 3.
4. Proving the Polystep Strong Normalization Theorem
In this section, we prove the polystep strong normalization theorem. The ba sic idea is very simple: to reduce polystep strong normalization to polystep weak normalization, by showing that any reduction sequence can be trans formed (standardized) into alongerone which is subject to the outerlayer ﬁrst strategy. Since the latter sequence is polynomially bounded by Girard Asperti’s result [9, 1], we can conclude that any sequence is polynomially bounded as well. Unfortunately, this argument does not work forλlaitself, since standardization inλlamay shorten the reduction sequence. To avoid this, we ﬁrst introduce an auxiliary term calculus, and show any reduction sequence in λla can be translated into another in the auxiliary calculus in 4.1. Then we show the standardization theorem in 4.2. Finally, we ac commodate GirardAsperti’s polynomial time weak normalization theorem to our setting in 4.3.
4.1. An Extended Calculus with Explicit Weakening
Suppose that t −−→^{(r)} u and consider the following reduction sequence of length two:
(λx.y)!t−−→^{(r)} (λx.y)!u−→^{(β)} y.
It is not outerlayerﬁrst. If one standardizes it, i.e., transforms it into an outerlayerﬁrst one, then the result is
(λx.y)!t−→^{(β)} y,
a shorter reduction sequence of length one, and the standardization argu ment breaks down. The failure may be ascribed to implicit weakening in volved byλabstraction. We avoid this by introducing an extended calculus where weakening isexplicit.
The setPT^{w}ofextended pseudotermsis deﬁned to be the setPT aug mented with subexpressions of the formlet =tinu(explicit weakening).
To deﬁne a new wellformedness relationt∈ T_{X,Y,Z}^{w} , we modify Deﬁnition 2 as follows.
(1) Replace clauses 2, 6, and 7 with:
2’ λx.t∈ T_{X,Y,Z}^{w} ⇐⇒ t∈ T_{X{x},Y,Z}^{w} , F O(x, t) = 1.
6’ let!x=tinu∈ T_{X,Y,Z}^{w} ⇐⇒ t∈ T_{X,Y,Z}^{w} , u∈ T_{X,Y}^{w} _{{x},Z}, F O(x, u)≥1.
7’ let§x=t inu∈ T_{X,Y,Z}^{w} ⇐⇒ t∈ T_{X,Y,Z}^{w} , u∈ T_{X,Y,Z{x}}^{w} , F O(x, u) = 1.
Namely, we require thatλandlet§bind exactly one variable andlet! binds at least one variable.
(2) Add the following clause:
8’ let =t inu∈ T_{X,Y,Z}^{w} ⇐⇒ t∈ T_{X,Y,Z}^{w} , u∈ T_{X,Y,Z}^{w} .
We say thattis a(wellformed) extended termift∈ T_{X,Y,Z}^{w} for someX,Y, Z.
The reduction rules in Figure 2 are extended toPT^{w}with the following modiﬁcations:
– Extend (com) to the newletoperator.
– Add a new reduction rule ( ):let =uin t−→t.
Reduction rules other than ( ) are called proper. A reduction sequence is properif it consists of proper reductions.
Lemmas 1 and 2 hold forT^{w}, too. In addition, we have
Proposition 3.If t∈ T_{X,Y,Z}^{w} ,t−−→^{(r)} uand(r)is proper, thenu∈ T_{X,Y,Z}^{w} . Now we consider a translation ofλlaterms into extended terms.
Lemma 8.For every termt, there is an extended termt^{w}such thatt^{w}−−→^{( )}^{∗} t andt^{w} ≤4t.
Proof. By induction ont. Whent≡λx.uandF O(x, u) = 0, deﬁnet^{w}to be λx.(let =xinu^{w}). When t≡(let †x=v inu) and F O(x, u) = 0, deﬁne t^{w} to belet †x=v^{w} in(let =§xinu^{w}). Other cases are straightforward.
Theorem 4 (Translation into the extended calculus).Lett_{0}be a term and let t_{0} −→^{σ} ^{∗}t_{1} be a reduction sequence in λla. Then there are extended terms t^{}_{0}, t^{}_{1} and a proper reduction sequence τ such that σ ≤ τ, t^{}_{0} = O(t0)and
t_{0} −→^{σ}^{∗} t_{1}
∗ ( )
∗ ( )
t^{}_{0} −→^{τ} ^{∗} t^{}_{1}.
The proof is based on permutation of reduction sequences. Each step of permutation is supported by the following two lemmas.
Lemma 9.Let t_{0} be an extended term. Ift_{0}−−→^{( )} t_{1}−−−−→^{(com)} t_{2}, then t_{0}−−−−→^{(com)}^{∗} t^{}_{1}−−−−→^{(com)} t^{}_{1} −−→^{( )} t_{2}
for somet^{}_{1} andt^{}_{1}.
Proof. Letube the contractum of the ﬁrst reduction (at address w_{0}) and v be the redex of the second reduction (at address w_{1}) in t_{1}. One can distinguish four cases: (i)uandvare separated (w_{0}w_{1}andw_{0}w_{1}), (ii) ucontainsv(w_{0}w_{1}), (iii)vproperly containsu(w_{0}w_{1}00 orw_{0}w_{1}1), (iv) u and v overlap (w_{0} =w_{1}0). In the ﬁrst three cases, permutation is straightforward and does not change the length of a reduction sequence. In the case (iv), we apply thepermutation rulein Figure 6(a), which says that the reduction sequence in solid line may be replaced with the other one in broken line.
Lemma 10.Let t_{0} be an extended term. If t_{0} −−→^{( )} t_{1} −−→^{(r)} t_{2}, where (r) is neither(com)nor( ), then
t_{0}−−−−→^{(com)}^{∗} t^{}_{1}−−→^{(r)} t^{}_{1}−−→^{( )}^{∗} t_{2} for somet^{}_{1} andt^{}_{1}.
Proof. As before, one can distinguish four cases, and the critical case is (iv):
two reductions overlap. In this case, use the permutation rules in Figure 6 (b) and (c).
Proof of Theorem 4.We argue step by step as follows:
(1) Ift_{0}−→^{( )} t_{1}−−−−−→^{ν,(com)}^{∗} t_{2}, thent_{0} ^{ν}
,(com)
−−−−−→^{∗} t^{}_{1}−→^{( )} t_{2},
(a)
Ψ[let =u1in (let∗=u2 int)] Ψ[let∗=u2 int]
let∗=u2 inΨ[t]
let =u1 in(Ψ[let∗=u2 int]) let =u1 in(let∗=u2in Ψ[t])
( )  pppppp
pppppp pppppp pppppp pppppp pppppp pppp
?
(com)
?
(com)
p p p p p p p^{(com)} ppppppppppppppppp6
( )
where∗is either †xor andΨ is either (•)vor (let∗=•inv).
(b)
(let =tin(λy.u))v (λy.u)v u[v/y]
let =tin ((λy.u)v) let =tin(u[v/y])
( ) pppppp
pp?
(com)
(β) 
p p p p p p p p p p p p p p p p p p p p p p p p p p^{(β)}  pppppppp6_{( )}
(c)
let †y= (let =tin †u) inv let †y=†uin v
v[u/x]
let =tin (let †y=†uinv) let =tin(v[u/x])
( ) pppppp
pppppp pppppp pppppp pppppp
pp?
(com)
?
(†)
p p p p p p p^{(†)} ppppppppppppp6
( )
(d)
(let!x=!tin(λy.u))v (λy.u[t/x])v u[t/x][v/y]
let!x=!tin(λy.u)v let!x=!tinu[v/y] u[v/y][t/x] 
(!)
pppppp pppp
?
(com)

(β)
p p p p p p p^{(β)} p p p p p p p p p p p p^{(!)} 
≡
Fig. 6.Permutation Rules