9512.net

甜梦文库

甜梦文库

当前位置：首页 >> >> # A proof of weak termination of the simply-typed oe-calculus

INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET AUTOMATIQUE

A Proof of Weak Termination of the Simply-Typed -Calculus

Jean Goubault-Larrecq

3090

N 3090

Janvier 1997

THEME 2

apport de recherche

ISSN 0249-6399

A Proof of Weak Termination of the Simply-Typed -Calculus

Jean Goubault-Larrecq

Theme 2 | Genie logiciel et calcul symbolique Projet Coq Rapport de recherche n 3090 | Janvier 1997 | 10 pages

Abstract: We show that reducing any simply-typed -term by applying the rules in

* * *

eagerly always terminates, by a translation to the simply-typed -calculus, and similarly for -terms with -eager rewrites. This holds even with term and substitution metavariables. In fact, every reduction terminates provided that ( )-redexes are only contracted under so-called safe contexts. The previous results follow because in , resp. -normal forms, all contexts around terms of sort T are safe. Key-words: -calculus, explicit substitutions, termination, -calculus, simple types

(Resume : tsvp)

Jean.Goubault@inria.fr

Unite de recherche INRIA Rocquencourt Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex (France) Telephone : (33 1) 39 63 55 11 { Telecopie : (33 1) 39 63 53 30

Resume : Nous montrons que reduire n'importe quel -terme simplement type en appliquant toujours les regles de le plus t^t possible est un processus qui termine. Ceci est o prouve a l'aide d'une traduction vers le -calcul simplement type, et de m^me pour le e calcul avec reduction prioritaire par . Ceci est valide m^me en presence de meta-variables e de termes et de substitutions. En fait, toute reduction termine des qu'on ne contracte que les ( )-redex qui apparaissent sous des contextes dits s^rs. Les resultats enonces plus haut u s'en deduisent car dans toute forme -normale, resp. -normale, tous les contextes autour de termes de sorte T sont s^rs. u Mots-cle : -calcul, substitutions explicites, terminaison, -calcul, types simples

* * *

Une preuve de terminaison faible du -calcul simplement type

Introduction

Although the simply-typed -calculus does not terminate strongly Mel94, Mel95], it terminates in the weak sense: every typed term has some (unique) normal form. We present a re ned proof of this fact. In fact, we prove the widely believed claim that every reduction where steps are applied eagerly is nite. For the sake of generality, we prove this result even in the presence of term and substitution metavariables, and for a general -calculus that encompasses both the original -calculus ACCL90] and the E -calculus of HL89]. The techniques that we use are basically the same as in GL97], where they are used for a more complicated calculus. The plan of the paper is as follows. We recapitulate some basic de nitions in Section 1 and prove a few preliminaries in Section 2. In Section 3, we prove the main theorem of this paper: every reduction where ( )contraction occurs only under so-called safe contexts always terminates. This result is applied in Section 4 to show that all normalization strategies that apply (resp. ) eagerly in the -calculus (resp. in , a.k.a. E ) terminate.

* *

1 De nitions

T ::= VT j T j TT j T S] j 1 S ::= VS j S S j id j T S j"j* S where VT and VS are disjoint in nite sets of term variables x, y, z, : : :, and stack variables X, Y , Z, etc. The set of -terms is the subset of -terms where * does not occur. We call (untyped) -calculus the rewrite system of Figure 1. It is a slight generalization, in the sense that it can simulate every reduction, of both the -calculus of ACCL90] and of the -calculus of HL89] (where it is named E ). Notice that, because of rule ( *), all the other rules with * in their names are super uous. The -calculus is the rewrite system de ned by all rules of without the three rules with an in their names. (The latter is basically group (B) of GL96], while the former is group (B) plus part of group (H)).

* * *

Consider the language stacks S are given by:

*

de ned as T S, where the sublanguage T and that of explicit substitutions or

( ) ( id]) ( id) (id ) ( ]) () (1) (") () () (app)

( u)v ! u v id] ( *) u id] ! u ( ) u id ! u ( ) id u ! u (1 *) (u v]) w] ! u v w] (1 * ) (u v) w ! u (v w) ("*) 1 u v] ! u ("* ) " (u v) ! v (**) (u v) w ! (u w]) (v w) (** ) ( u) w] ! (u * w]) (* ) (uv) w] ! (u w])(v w]) (* id) Figure 1: The

*

* w ! 1 (w ") 1 "! id (1 u]) (" u) ! u 1 * u] ! 1 1 * u v] ! 1 v] " *u!u " " (* u v) ! u (" v) * u * v !* (u v) * u (* v w) !* (u v) w * u (v w) ! v (u w) * id ! id

-calculus terminates, when rewrites are

0

-calculus

The purpose of this paper is to show that the simply-typed restricted to be -eager rewrites , i.e. rewrites of the form:

0 0

( ) ( ) ( ) u?! u1?!u1 ?! u2 ?!u2?! : : : ?! uk ?!uk ?! : : :

where u1 , u2 , : : :, uk , : : : are -normal. And similarly, that the simply-typed rewrites are restricted to be -eager rewrites, de ned similarly.

*

*

-calculus terminates, when

1

the list; formulas are either atoms A, B, : : :, or implications (arrow types) 1 ! 2 . Stack types are similar sequents ? ` , but is a nite list of formulas as well. For simplicity, we shall assume that the calculus is given in Church style: variables x? are annotated with their type ? ` ; we write them x when no confusion arises. (Writing terms in Church style will allow us to translate -terms to -terms in Section 3; otherwise, we would need to translate typing derivations of -terms to typing derivations of -terms, which is not that di erent, but would be much less readable.)

`

The typing rules are given in Figure 2. Types are either term types or stack types. Term types are sequents ? ` , where is a formula and ? is a nite list of formulas 1 ; : : :; n; , where marks the end of

X?

`

:?`

(V arS )

x? : ? `

`

(V arT ) (I)

u:?` v:?` (; I) u v:?` ; u:?` (*) * u : ;? ` ; u : 1; ? ` 2 (! I) u:?` 1! 2 u: ` v:?` (CutS ) u v:?`

id : ? ` ? 1 : ;? `

(; E1) (; E2)

1

": ; ? ` ?

u:?`

1

(! E) uv : ? ` 2 u: ` v:?` (CutT ) u v] : ? `

!

2

v:?`

Figure 2: Typing rules To get a calculus in Church style, we also need to annotate the terms 1, ", id and * u with types agreeing with the rules of Figure 2. We shall usually write these terms without their type annotations when context permits, however. Then, every typed term has a unique type. There is a unique way of lifting the rules of Figure 1 to the typed case so that the resulting typed calculus has the subject reduction property: see Figure 3. ( ) ( id]) ( id) (id ) ( ]) () (1) (") () () (app) ( u)v ! u v id? ?] where v : ? ` u id? ?] ! u u id? ? ! u id? ? u ! u (u v]) w] ! u v w] (u v) w ! u (v w) 1? u v] ! u "? (u v) ! v (u v) w ! (u w]) (v ( u) w] ! (u (* w) ;? where w : ? ` ; u : ; (uv) w] ! (u w])(v w])

` ` ` ` ` `

( *)

`

( ) ( ) (1 *) (1 * ) ("*) ("* ) (**) w) (** ) ; ]) (* ) ` (* id) (* id? ?) ;? ;? ! id ;? ;?

` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` 0 ` ` ` `

(* w) ;? ; ! 1 ;? (w " ;? ?) 1 ;? " ;? ?! id ;? ;? (1 ;? u]) (" ;? ? u) ! u 1 ; (* u) ;? ; ] ! 1 ;? 1 ; (* u) ;? ; v] ! 1 ;? v] "; (* u) ;? ; ! u " ;? ? "; ((* u) ;? ; v) ! u (" ;? ? v) (* u) ; ; (* v) ;? ; ! (* (u v)) ;? ; (* u) ; ; ((* v) ;? ; w) ! (* (u v)) ;? ; (* u) ;? ; (v w) ! v (u w)

` ` ` ` ` ` ` ` `

w

Figure 3: The typed reduction rules 2

2 Other Preliminaries

Lemma 1 is a terminating rewrite system. Proof: We use Zantema's distribution elimination technique Zan94]. (Refer to this paper for notations

and concepts; our is slightly more complicated than the that Zantema considers, but the argument is similar.) We actually show that is totally terminating, i.e. that the reduction relation for can actually be extended to a total well-founded quasi-ordering on terms. Total termination implies simple termination, which is the fact that plus all rules of the form f(: : :; u; : : :) ! u, for every function symbol f, terminates. Now consider the following rewrite system , which is obtained from by replacing u v] by u v, uv by u v, id by 1 ", merging duplicate rules, eliminating rule ( ) and adding rule (d *):

0

(d *) * u (v w) ! (* u v) (* u w) ( *) ( id) u (1 ") ! u ( ) (id ) (1 ") u ! u (1 *) (1 * ) ( ) (u v) w ! u (v w) ("*) (1) 1 (u v) ! u ("* ) (") " (u v) ! v (**) ( ) (u v) w ! (u w) (v w) (** ) ( ) ( u) w ! (u * w) (* ) (* id)

0

* w ! 1 (w ") (1 u) (" u) ! u 1 *u!1 1 (* u v) ! 1 v " *u!u " " (* u v) ! u (" v) * u * v !* (u v) * u (* v w) !* (u v) w * u (v w) ! v (u w) * (1 ") ! (1 ")

0

If is totally terminating, then it is clear that is totally terminating as well. Let indeed > be any total well-founded quasi-ordering extending the rewrite relation of . This induces a total well-founded quasi-ordering on -terms that extends all the rules in except ( ) (for which both sides are equivalent). Let > be the quasi-ordering such that u > v if and only if u has more occurrences of than v: then the lexicographic product of > and > is a well-founded total quasi-ordering extending the rewrite relation of . Now call a rule embedding if and only if its right-hand side is homeomorphically embedded in its left-hand side (i.e., it can be simulated by a sequence of rewrite steps of the form f(: : :; u; : : :) ! u). The rules ( id), (id ), (1), ("), ( ), (1 *), (1 * ), (* id) are embedding. Since total termination implies simple termination, is totally terminating if and only if minus these rules is. Moreover, (* ) can be simulated by (d *) plus embedding, so we can ignore the former for purposes of total termination. To sum up, is totally terminating if and only if the following system is totally terminating: (d *) * u (v w) ! (* u v) (* u w) ( *) * w ! 1 (w ") ( ) (u v) w ! u (v w) ("*) " * u ! u " ("* ) " (* u v) ! u (" v) (**) * u * v !* (u v) ( ) (u v) w ! (u w) (v w) (** ) * u (* v w) !* (u v) w ( ) ( u) w ! (u * w)

0 0 0 0 0 0 00

Now, in the rules (d *) and ( ) are distribution rules for , and no other rule features on the left-hand side. Zantema's theorem Zan94] then states that the rewrite system obtained from by dropping these distribution rules and replacing each rule with some subterm u v on the right-hand side by two rules, one with u v replaced by u, the other with u v replaced by v, is totally terminating if and only if is. Here is : *w!1 *w!w " (u v) w ! u (v w) " *u!u " " (* u v) ! u (" v) * u * v !* (u v) * u (* v w) !* (u v) w ( u) w ! (u * w) is then proved totally terminating by using two polynomial interpretations P1 and P2 , ordered lexico00 000 00 00 000 000

3

graphically, as in HL89]; we let:

P1 P2 u v uv u(v + 1) *u u 3u 1 2 1 " 2 1 u u+1 u Using the fact that P1 (u) 2 for every term u, and P2(u) 1, a quick calculation shows that for every rule l ! r but the last one (i.e., ( )), P1(l) P1(r) and P2(l) > P2 (r), while in the case of ( ) P1(l) > P1(r). It follows that is totally terminating. 2 In fact, is locally con uent, as a Knuth-Bendix test shows, whether as the subsystem of Figure 1 or Figure 3, so it is convergent; but we shall not be interested in this property here.

3 Reduction Under Safe Contexts Terminates

We translate each -term with Church-style typing into a family of -terms, typed a la Church as well. Let > be a given arbitrary type. We assume that we have in nitely many variables of each type. With each term variable x 1 ;:::; n ; of , we associate a variable x 1 ::: n ^ of the -calculus of ^1 1 ::: n the indicated type. Similarly, we map each stack variable X 1 ;:::; n ; 1 ;:::; n ; to a list X :: 1 ^ ^ : : : :: Xn 1 ::: n :: Xn +1 1 ::: n of -variables of the indicated types. (The cons operator n :: is just a meta-linguistic way of forming lists; it is assumed to be right-associative.) We do not assume the mapping to be injective in any sense. Our translation maps every -term u of type 1 ; : : :; n; ` to a function u]] taking a list of n + 1 terms t1 :: : : : :: tn :: tn+1 of respective types 1, : : :, n and >, and returns a -term u]](t1 :: : : : :: tn :: tn+1 ) of type . Similarly, our translation maps every -term u of type 1 ; : : :; n; ` 1 ; : : :; n ; to a function u]] taking a list of n + 1 -terms t1 :: : : : :: tn :: tn+1 of respective types 1 , : : :, n and >, and returns a list of n + 1 -terms of respective types 1 , : : :, n and >. The translation is given in Figure 4.

` !

0

!

!>!

` 0

0

!

!

!>! 0

0

!

!

!>! 0 0

0

!

!

!>!>

0

0

0

0

0

0

0

x 1;:::; n ; ] (t1 :: : : : :: tn :: tn+1 ) = x 1 ::: n ^ t1 : : :tn tn+1 ^ X 1 ;:::; n ; 1;:::; n ; ] (t1 :: : : : :: tn :: tn+1) = (X1 1 ::: n t : : :tn tn+1) 1 1 :: : : : ^ :: (Xn 1 ::: n t1 : : :tn tn+1) ^n +1 1 ::: n n t1 : : :tn tn+1) :: (X u]](s) = z u]](z :: s) where u : ; ? ` uv]](s) = ( u]](s))( v]](s)) u v]]](s) = u]]( v]](s)) 1 ;? ] (t :: s) =t u v]](s) = u]]( v]](s)) id? ?] (s) =s u v]](s) = u]](s) :: v]](s) " ;? ?] (t :: s) =s * u]](t :: s) = t :: u]](s)

` ! ! !>! `

0 0 0

!

!

!>! 0

0 0

!

!

!>! 0 0

!

!

!>!>

0

`

`

`

Figure 4: Translation to the simply-typed -calculus The rule ( x t)t ! t t =x] de nes a rewrite relation on -terms that we again write ?!. Recall that the simply-typed -calculus terminates Kri92]. We write ?!+ , resp. ?! , its (resp. re exive) transitive closure. These notions are extended to lists: t1 :: : : : :: tn :: tn+1 ?! t1 :: : : : :: tn :: tn+1 if and only if ti ?! ti for every i, 1 i n+1; and t1 :: : : : :: tn :: tn+1 ?!+ t1 :: : : : :: tn :: tn+1 if in addition ti ?!+ ti for some i, 1 i n + 1.

0 0 0 0 0 0 0 0 0 0

4

We de ne the quasi-ordering and the strict ordering on typed -terms by: u v if and only if u and v have the same type and u]](s) ?! v]](s) for every list s of -terms of the right types. (Observe that is an ordering, in particular it is irre exive precisely because there are -terms of any given type, namely variables.) Similarly, u v if and only if u and v have the same type and u]](s) ?!+ v]](s) for every list s of -terms of the right types. We also let u v if and only if u]](s) = v]](s) for every list s of -terms of the right types. The interpretation is monotonic in the following sense: Lemma 2 If s ?! s , then u]](s) ?! u]](s ). Proof: We claim that for any terms t1, : : :, tn, tn+1 of the right types, for any fresh variables x1, : : :, xn, xn+1 of the right types: u]](t1 :: : : : :: tn :: tn+1) = u]](x1 :: : : : :: xn :: xn+1 ) t1=x1; : : :; tn=xn; tn+1=xn+1] where substitution is extended componentwise when u is a stack. The lemma follows immediately from the claim, while the claim is proved by structural induction on u. If u = v w], then u]](t1 :: : : : :: tn :: tn+1 ) = v]](t1 :: : : : :: tn :: tn +1 ), where t1 :: : : : :: tn :: tn +1 = w]](t1 :: : : : :: tn :: tn+1). By induction hypothesis, t1 :: : : : :: tn :: tn +1 = w]](x1 :: : : : :: xn :: xn+1) t1 =x1; : : :; tn=xn; tn+1=xn+1]. Let: (1) t1 :: : : : :: tn :: tn +1 be w]](x1 :: : : : :: xn :: xn+1), then for each i , 1 i n + 1: (2) ti = ti t1=x1; : : :; tn=xn]. Then: u]](t1 :: : : : :: tn :: tn+1) = v]](t1 :: : : : :: tn :: tn +1 ) = v]](x1 :: : : : :: xn :: xn +1 ) t1=x1; : : :; tn =xn ; tn +1 =xn +1 ] (by induction hypothesis again) = v]](x1 :: : : : :: xn :: xn +1 ) t1 t1=x1 ; : : :; tn=xn; tn+1=xn+1 ]=x1; : : :; tn +1 t1=x1 ; : : :; tn=xn; tn+1 =xn+1]=xn ] (by (2)) = v]](x1 :: : : : :: xn :: xn +1 ) t1 =x1; : : :; tn +1 =xn +1 ] t1=x1; : : :; tn=xn; tn+1=xn+1] = v]](t1 :: : : : :: tn :: tn +1 ) t1=x1; : : :; tn=xn; tn+1=xn+1] (by induction hypothesis again) = u]](x1 :: : : : :: xn :: xn+1) t1 =x1; : : :; tn=xn; tn+1=xn+1] (by (1)) If u = v w, then the argument is identical, while all other cases are trivial. 2 Recall that a context C is any term with a distinguished occurrence , which we call the hole. For any term t, Cftg denotes C with the hole replaced by t. Similarly if t is itself a context, in which case we get a new context. The interpretation is then also monotonic in the following sense: Lemma 3 If u v, then Cfug Cfvg for any context C. If u v, then Cfug Cfvg for any context C. Proof: The case of is trivial, because our de nition of ] is compositional. That is, for any context C, there is a functional C ] such that, for every u, Cfug] = C ] ( u]]): this is an easy structural induction on C . We prove the rst claim by structural induction on the context C as well. The base case, when C is the empty context , is clear. Otherwise, the induction case reduces to the elementary cases that whenever u v, then f(: : : ; u; : : :) f(: : : ; v; : : :) for each function symbol f in the language of and each argument position. For example, if f = : u]](s) = z u]](z :: s) ?! z v]](z :: s) (since u v) = v]](s). Since s is arbitrary, u v. The cases when f is the application symbol or the pair operator (whatever the argument position), or the * lift operator are equally easy. When f is the ] operator, we have two cases. At argument position 1, we must show that u v entails u w] v w]. But this is trivial, since u w]]](s) = u]]( w]](s)) ?! v]]( w]](s)) (by assumption) = v w]]](s). At argument position 2, we must show that u v entails w u] w v]. But w u]]](s) = w]]( u]](s)) ?! w]]( v]](s)) (since u v and by Lemma 2) = w v]]](s). The case of is entirely analogous. 2 Observe that the interpretation is not strictly monotonic, in that u v does not imply Cfug Cfvg, only Cfug Cfvg: consider the context C =" ( w) for some w. This leads to the following de nition:

0 0 0 0

0

0

0

0

0

0

0

0

0

0

0

0

0

00

00

0

00

0

0

0

0

0

0

00

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

0

00

0

00

0

0

0

0

0

0

0

0

00

0

00

0

0

0

00

00

0

00

0

5

De nition 1 A context C is called safe if and only if u v implies Cfug Cfvg for every terms u and v of the same type such that Cfug and Cfvg are typable.

We shall see in Section 4 that there are enough safe contexts to all typed form by reductions under safe contexts. -terms to be reduced to normal

Lemma 4 For each rule l ! r except ( ) in Figure 3, l r. For rule ( ), l r. Proof: We omit all type information unless strictly necessary.

l]](s) = ( u]](s))( v]](s)) = ( z u]](z :: s))( v]](s)) ?! ( u]](z :: s)) v]](s)=z] = u]]( v]](s) :: s) by Lemma 3, while r]](s) = u]]( v id]](s)) = u]]( v]](s) :: s). The cases of rules ( id]), ( id) and (id ) are obvious: l]](s) = r]](s) = u]](s) in all three cases. Rule ( ]): l]](s) = u v]]]( w]](s)) = u]]( v]]( w]](s))) = u]]( v w]](s)) = u v w]]](s), and similarly for rule ( ). Rule (1): l]](s) = 1]]( u v]](s)) = 1]]( u]](s) :: v]](s)) = u]](s) = r]](s). Rule ("): l]](s) = "] ( u v]](s)) = "] ( u]](s) :: v]](s)) = v]](s) = r]](s). Rule ( ): l]](s) = u v]]( w]](s)) = u]]( w]](s)) :: v]]( w]](s)) = u w]]](s) :: v w]](s) = (u w]) (v w)]](s) = r]](s). Rule ( ): l]](s) = u]]( w]](s)) = z u]](z :: w]](s)), while r]](s) = z u * w]]](z :: s) = z u]]( * w]](z :: s)) = z u]](z :: w]](s)). Rule (app): similar argument as for rule ( ). Rule ( *): l]](t :: s) = t :: w]](s), while r]](t :: s) = 1]](t :: s) :: w "] (t :: s) = t :: w "] (t :: s) = t :: w]]( "] (t :: s)) = t :: w]](s). Rule ( ): l]](t :: s) = 1]](t :: s) :: "] (t :: s) = t :: s = r]](t :: s); and t :: s is the most general form of argument to l]] by typing, so l r. Rule ( ): l = (1 u]) (" u) (1 ") u (by case ( ])) id u (by case ( )) u = r (by case (id )). Observe that we have used Lemma 3 (the part) implicitly throughout. All the other rules are dealt with similarly: Rule (1 *): l = 1 * u] 1 1 (u ")] (by ( *)) 1 = r (by (1)). Rule (1 * ): l = 1 * u v] 1 (1 (u ")) v] (by ( *)) 1 (1 v]) ((u ") v)] (by ( )) 1 v] = r (by (1)). Rule ("*): l =" * u " (1 (u ")) (by ( *)) u "= r (by (")). Rule ("* ): l =" (* u v) " ((1 (u ")) v) (by ( *)) " ((1 v]) ((u ") v)) (by ( )) (u ") v (by (")) u (" v) = r (by ( )). Rule (**): l =* u * v (1 (u ")) * v (by ( *)) (1 * v]) ((u ") * v) (by ( )) 1 ((u ") * v) (by (1 *)) 1 (u (" * v)) (by ( )) 1 (u (v ")) (by ("*)) 1 ((u v) ") (by ( ) used in the opposite direction) * (u v) = r (by ( *) used in the opposite direction). Rule (** ): l =* u (* v w) (* u * v) w (by ( ) used in the opposite direction) * (u v) w = r (by (**)). Rule (* ): l =* u (v w) (1 (u ")) (v w) (by ( *)) (1 v w]) ((u ") (v w)) (by ( )) v ((u ") (v w)) (by (1)) v (u (" (v w))) (by ( )) v (u w) = r (by (")). Rule (* id): l =* id 1 (id ") (by ( *)) 1 " (by (id )) id = r (by ( )). 2 It follows: Theorem 5 (Main Theorem) Every reduction in the typed -calculus, where every contracted ( )-redex

occurs under a safe context, is nite.

Rule ( ):

6

Proof: Any step in such a reduction is either a ( )-contraction Cf( u)vg ?! Cfu v id]g, then Cf( u)vg Cfu v id]g by Lemma 4 and the fact that C is safe; or a -contraction u ?! v, where u v by Lemma 4 and Lemma 3. Therefore each rewrite step is strictly decreasing in the lexicographic product of and ?!+ ,

which is well-founded since the typed -calculus terminates (for ) and terminates (by Lemma 1). 2

4 Some Safe Contexts

It remains to produce some non-trivial safe contexts: De nition 2 Let the syntactically safe contexts be de ned as those in ST SS , where: ST ::= j ST j ST T j T ST j ST S] j VT SS ] j 1 SS ] SS ::= SS j ST S j T SS j* SS j* S SS j SS S SS ::= VS SS j" SS j SS S

0 0 0 0 0 0

Before we show Lemma 7, we need the following technical lemma. Let tl be de ned by tl(t :: s) = s, and let tln be de ned by: tl0(s) = s, tl n+1 = tl tln . Lemma 6 For every context C in SS , there is a stack variable X , a proper subcontext C of C in SS and an integer m 2 N such that, for every term u such that C fug is well-typed, for every s of the right type, for some s, C fug] (s ) = tl m ( X]]( Cfug] (s))). Proof: By structural induction on C . This is obvious if C has the form X C, with C 2 SS : m = 0 and s=s. If C =" C with C 2 SS , then for every u such that C fug is well-typed, in particular C fug is welltyped, so by induction hypothesis C fug] (s ) = tlm ( X]]( Cfug] (s))) for some m 0 and some s. Then C fug] (s ) = "] ( C fug] (s )) = tl( C fug] (s )) = tlm+1 ( X]]( Cfug] (s))). If C = C w, where C 2 SS , then for every u such that C fug is well-typed, in particular C fug is well-typed, so by induction hypothesis, for every s1 of the right type, C fug] (s1 ) = tlm ( X]]( Cfug] (s1 ))) for some m 0 and some s1 . Then C fug] (s ) = C fug] ( w]](s )); letting s1 be w]](s ), C fug] (s ) = C fug] (s1) = tlm ( X]]( Cfug] (s1 ))). 2

0 0 0 0 0 0 0 0 0 0 0 00 00 0 0 00 00 0 0 0 00 0 00 0 0 00 00 0 0 00 0 00 0 0 0 00 0 0 0 0 0 00 0

Lemma 7 Every syntactically safe context is safe. Proof: We have to show that if u v, then Cfug Cfvg for any syntactically safe context C. This is by structural induction on C , using De nition 1. The base case, when C is the empty context , is clear. Otherwise: If C = C1 , where C1 2 ST , then Cfug] (s) = z C1fug] (z :: s) ?!+ z C1fvg] (z :: s) = Cfvg] (s) by induction hypothesis. Similarly when C = C1 w or C = wC1, or C = C1 w for some term w and some C1 2 ST , or C =* C1 or C = w C1 for some term w and some C1 2 SS . If C = C1 w] for some C1 2 ST and some stack w, then Cfug] (s) = C1fug] ( w]](s)) ?!+ C1fvg] ( w]](s)) = Cfvg] (s) by induction hypothesis. Similarly when C = C1 w for some C1 in SS and some stack w. If C = x C1] where x is an term variable and C1 2 SS , then Cfug] (s) = xt1 : : :tn tn+1 where t1 :: : : : :: ^ tn :: tn+1 = C1fug] (s) ?!+ C1fvg] (s) by induction hypothesis. Let (t1; : : :; tn; tn+1) be C1fvg] (s): this means that ti ?! ti for every i, 1 i n + 1, and that ti ?!+ ti for some i. So xt1 : : :tn tn+1 ?!+ ^ xt1 : : :tntn+1 = Cfvg] (s). ^ It remains to deal with the cases when C is in SS , and when C is of the form 1 C ] or * w C with C 2 SS . Consider rst the case where C is some context C in SS . By Lemma 6, there is a stack variable X, a proper subcontext C1 in SS and an integer m 0 such that for every u of the right type, for every s of the right type, there is a -term s such that C fug] (s ) = tlm ( X]]( C1fug] (s))). Let X be X? 1 ;:::; p ; where

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 `

7

by typing p m. Let also t1 :: : : : :: tn :: tn+1 be C1fug] (s), and t1 :: : : : :: tn :: tn+1 be C1fvg] (s). Then:

0 0 0

^ ^ ^ ^ (X1 t1 : : :tntn+1 ) :: : : : :: (Xm t1 : : :tntn+1 ) :: (Xm+1 t1 : : :tn tn+1) :: : : : :: (Xp+1 t1 : : :tntn+1 ) ^ ^ = (Xm+1 t1 : : :tn tn+1) :: : : : :: (Xp+1 t1 : : :tntn+1 ) + (Xm+1 t : : :t t ^ 1 n n+1) :: : : : :: (Xp+1 t1 : : :tntn+1 ) (by induction hypothesis) ^ ?! m (X t : : :t t ) :: : : : :: (X t : : :t t ) :: (X ^1 1 n n+1 ^m 1 n n+1 ^m+1 t1 : : :tn tn+1) :: : : : :: (Xp+1 t1 : : :tntn+1 ) ^ = tl = C fvg] (s ) = tlm

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

C fug] (s )

0 0

so Cfug Cfvg. If C = 1 C ], then taking the same notation as above:

0

^ = Xm+1 t1 : : :tn tn+1 ^ ?!+ Xm+1 t1 : : :tntn+1 (by induction hypothesis) = Cfvg] (s )

0 0 0 0

Cfug] (s )

0

(observe that now p > m by typing) so again Cfug Cfvg. And if C =* w C , then: Cfug] (s ) ^ = (Xm+1 t1 : : :tn tn+1) :: w]](tl( C fug] (s )) ^ ?! (Xm+1 t1 : : :tntn+1 ) :: w]](tl( C fvg] (s )) (by Lemma 3) + (X ?! ^m+1 t1 : : :tn tn+1) :: w]](tl( C fvg] (s )) (by induction hypothesis) = Cfvg] (s )

0 0 0 0 0 0 0 0 0 0 0 0

so Cfug Cfvg. 2

Lemma 8 Let Cfug be a -normal simply-typed term, where u 2 T . Then C is a syntactically safe context. Proof: Recall that the -normal forms ( R o93], p.76) are all elements of the languages described by the following grammar: In T: t ::= 1 j t j tt j VT j VT s] j 1 s ] In S: s ::= s j id j t s s ::="j VS j VS s j" s

0 0 0 0

(Although our is di erent from R os', it is easy to see that it has exactly the same normal forms.) Therefore the contexts having a hole accepting terms of T are elements of the languages de ned by the grammar: In T: Ct ::= j Ct j Ctt j tCt j Ct s] j VT Cs] j 1 Cs] In S: Cs ::= Cs j Ct s j t Cs Cs ::= VS Cs j" Cs

0 0 0 0

Corollary 9 In the simply-typed -calculus, every -eager rewrite is nite. Proof: In every -eager rewrite, every ( ) is performed under a syntactically safe context by Lemma 8.

This context is safe by Lemma 7, so Theorem 5 applies. 2 We can do the same thing with the -calculus and -eager rewrites: Lemma 10 Let Cfug be a -normal simply-typed term, where u 2 T . Then C is a syntactically safe context.

* * *

which clearly de nes sublanguages of ST , SS and SS respectively, proving the claim. 2

0

8

Corollary 11 In the simply-typed -calculus, every -eager rewrite is nite. Proof: In every -eager rewrite, every ( ) is performed under a syntactically safe context by Lemma 10.

* *

languages described by the following grammar: In T: t ::= 1 j t j tt j VT j VT s] j 1 s ] In S: s ::= s j id j t s j* s j* s s s ::="j VS j VS s j" s Indeed, we show by structural induction on the -normal term u that: (1) if u is in T, then u is in language t, (2) if u is a stack, then u is in language s, (3) if u is a stack and 1 u] is -normal, then u is in language s , (4) if u is a stack and " u is -normal, then u is in language s , and (5) if u is a stack and * v u is -normal, then u is in language s . First, observe that (2) implies (3): since 1 u] is -normal, u cannot be id (by rule ( id])), a cons v w (rule (1) would be applicable) or a lift * v (rule (1 *) would be applicable), or of the form * v w (rule (1 * ) would be applicable). Similarly, (2) implies (4), because of rules ( id), ("), ("") and ("* ). And (2) implies (5) because of rules ( id), (* ), (**) and (** ). We now show (2). Let u be a -normal stack. If u is in VS or is ", then u is clearly in s , hence in s. If u = id or if u is a cons v w or a lift * v, then u is also in s. Finally, if u is a composition v w, then in particular v is in s; but v cannot be id (rule (id ) would apply), or a cons v1 v2 (rule ( ) would apply), or a composition v1 v2 (rule ( ) would apply); so v must be of the form * v1 (then u has the form * v1 w with v1 2 s and w 2 s by induction hypothesis; since (2) implies (5), w is actually in s , so u is in s), or v =" (then u =" w, where w 2 s by induction hypothesis; since (2) implies (4), w is actually in s , so u is in s , hence in s), or v is a variable X in VS (then u = X w with w 2 s by induction hypothesis, so u is in s , hence in s). We now show (1). Let u be a -normal term in T. If u is a variable in VT , an abstraction v, an application vw or 1, then u is in t. Finally, if u is of the form v w], then v must be a variable in VT or be equal to 1: the other cases would be reducible by rules ( ), (app) or ( ]). Moreover, by induction hypothesis w is in s. If v is a variable x in VT , then u = x w] is in t. If v = 1, then u = 1 w] where w is in s, and since (2) implies (3), w is actually in s ; so u is in t again. It follows that the contexts having a hole accepting terms in T are in the languages de ned by the grammar: In T: Ct ::= j Ct j Ct t j tCt j Ct s] j VT Cs] j 1 Cs] In S: Cs ::= Cs j Ct s j t Cs j* Cs j* Cs s j* s Cs Cs ::= VS Cs j" Cs and it is easy to see that Ct , Cs, Cs are respective sublanguages of ST , SS and SS . 2 It follows:

0 0 0 0 0 * * 0 * 0 * 0 * * 0 0 0 0 0 * 0 0 0 0 0 0 0 0 0 *

Proof: An easy argument, similar to those found in R o93], shows that the -normal forms are all in the

*

This context is safe by Lemma 7, so Theorem 5 applies. 2

References

ACCL90] Mart n Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Levy. Explicit substitutions. In Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages, pages 31{46, San Francisco, California, January 1990. GL96] Jean Goubault-Larrecq. On computational interpretations of the modal logic S4 II. The evQ-calculus. Technical report, University of Karlsruhe, 1996. Available on ftp://theory.doc.ic.ac.uk/theory/guests/GoubaultJ/. GL97] Jean Goubault-Larrecq. On computational interpretations of the modal logic S4 IIIb. Con uence and conservativity of the evQH -calculus. Technical report, Inria, 1997. 9

HL89] Kri92] Mel94] Mel95]

R o93] Zan94]

Therese Hardin and Jean-Jacques Levy. A con uent calculus of substitutions. In France-Japan Arti cial Intelligence and Computer Science Symposium, December 1989. Jean-Louis Krivine. Lambda-calcul, types et modeles. Masson, 1992. Paul-Andre Mellies. Typed lambda-calculi with explicit substitutions may not terminate. In Proceedings of the CONFER workshop, Munchen, April 1994. Paul-Andre Mellies. Typed lambda-calculi with explicit substitutions may not terminate. In M. Dezani-Ciancaglini and G. Plotkin, editors, 2nd International Conference on Typed LambdaCalculi and Applications (TLCA'95), pages 328{334, Edinburgh, UK, April 1995. Springer Verlag LNCS 902. Alejandro R os. Contributions a l'etude des lambda-calculs avec substitutions explicites. PhD thesis, Ecole Normale Superieure, December 1993. Hans Zantema. Termination of term rewriting: Interpretation and type elimination. Journal of Symbolic Computation, 17:23{50, 1994.

10

Unite de recherche INRIA Lorraine, Technop^le de Nancy-Brabois, Campus scienti que, o 615 rue du Jardin Botanique, BP 101, 54600 VILLERS LES NANCY Unite de recherche INRIA Rennes, Irisa, Campus universitaire de Beaulieu, 35042 RENNES Cedex Unite de recherche INRIA Rh^ne-Alpes, 46 avenue Felix Viallet, 38031 GRENOBLE Cedex 1 o Unite de recherche INRIA Rocquencourt, Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex Unite de recherche INRIA Sophia-Antipolis, 2004 route des Lucioles, BP 93, 06902 SOPHIA-ANTIPOLIS Cedex

Editeur INRIA, Domaine de Voluceau, Rocquencourt, BP 105, 78153 LE CHESNAY Cedex (France) ISSN 0249-6399

赞助商链接

- The Theory of LEGO A Proof Checker for the Extended Calculus of Constructions
- A new proof of the weak pigeonhole principle
- A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory
- A Formalization of the Simply Typed Lambda Calculus in Coq
- Proof Pearl The Termination Analysis of Terminator
- A Calculus for Boxing Analysis of Polymorphically Typed Languages
- Soundness of the Simply Typed Lambda Calculus in ACL2
- On the proof theory of the modal mu-calculus
- The typed -calculus at work A proof of Jones's parallelisation theorem on concurrent object
- A proof search specification of the π-calculus
- Proof of the subject reduction property for a-calculus in COQ
- The Simply Typed Rewriting Calculus
- A Note on Observational Equivalence in the Simply Typed -calculus
- A proof search specification of the π-calculus
- A direct proof of strong normalization for an extended Herbelin’s calculus

更多相关文章：
更多相关标签：