1: \chapter{The Suspension Calculus}

2: \label{ch:susp}

3: 

4: The lambda calculus revolves around $\beta$-contraction. In turn,

5: $\beta$-contraction depends on a monolithic substitution operation

6: which is impractical for use in actual implementations. A solution to

7: this is to move the substitution operation down from the meta level

8: into the object level, \ie, make it explicitly part of the syntax of

9: the lambda calculus. This allows for direct manipulation of

10: substitutions and therefore fine-grained control over the substitution

11: process. The focus of this chapter is on a specific explicit

12: substitution calculus: the suspension calculus.

13: 

14: The first half of this chapter, extending from

15: \autoref{sec:motivation} to \autoref{sec:susp-metavars}, introduces

16: the suspension calculus and possible variations on it.  We start this

17: introduction by motivating the notation used to encode substitutions

18: in the suspension calculus and defining notation and rules based on

19: this motivation. We then describe the relationship between the

20: suspension calculus of this thesis and the original suspension

21: calculus from which it is created.  Next we show how the suspension

22: calculus admits typing in the style of the simply-typed lambda

23: calculus. We then discuss different ways in which meta variables can

24: be added to the calculus.

25: 

26: The second half of this chapter, comprising the remaining sections,

27: deals with proving important properties of the suspension calculus.

28: First, we prove that the rules governing substitution are terminating,

29: thus reflecting the finite nature of substitution in the lambda

30: calculus. Second, we show that these substitution rules are confluent,

31: thus the choices we make in performing substitution always result in

32: the same normal form. Third, we show that the suspension calculus

33: faithfully models the process of $\beta$-reduction in the lambda

34: calculus. Fourth, we prove that the property of confluence extends to

35: the full suspension calculus, thus making it a candidate for new

36: approaches to unification. Finally, we prove a property intrinsic to

37: the suspension calculus which relates different ways of representing

38: substitutions.

39: 

40: \section{Motivation for the Encoding of Substitutions}

41: \label{sec:motivation}

42: 

43: Before we formally and explicitly define the syntax of the suspension

44: calculus, it is beneficial to consider what information needs to be

45: reflected into the syntax. Note that we are doing this reflection in

46: the context of the de Bruijn notation since it provides a unique

47: representation of $\alpha$-equivalent terms. The first difficultly in

48: this respect is that substitution in the de Bruijn notation is an

49: operation with infinitely many arguments. For instance we have the

50: $\beta$-contraction rule which say

51: \[ ((\lambdadb t_1)\app t_2) \onebeta S(t_1; t_2, \#1, \#2,

52: \ldots). \] The substitution here is for infinitely many variables and

53: thus no naive embedding of this into the syntax will work. Instead, it

54: helps to start with a fresh view of the substitution needed for

55: $\beta$-reduction.

56: 

57: Consider the following term for which we want to perform

58: $\beta$-reduction but delay its effect on $t$,

59: \begin{equation}

60: \label{eq:before}

61: (\ldots ((\lambdadb \ldots(\lambdadb \ldots ((\lambdadb \ldots t

62: \ldots)\ s_1)\ldots )\ldots)\ s_2) \ldots)

63: \end{equation}

64: Here we have a redex with $s_2$ as an argument and within the body of

65: this redex we have another redex with $s_1$ as an argument. We want to

66: consider the effect on $t$ of contracting these redexes. That is, we

67: wish to produce a term of the following form:

68: \begin{equation}

69: \label{eq:after}

70: (\ldots (\ldots(\lambdadb \ldots ( \ldots t' \ldots)\ldots )\ldots)

71: \ldots)

72: \end{equation}

73: where $t'$ is an encoding of the term $t$ together with the

74: information needed to perform the substitutions generated by

75: contracting the two redexes. We call $t'$ a {\it suspension} since it

76: represents a suspended substitution. The information in this

77: suspension consists of substitutions for some variables and

78: renumberings for the other variables. In order to express this

79: information, it helps to distinguish between two types of variables in

80: $t$: those that referred to a variable bound within the outermost

81: lambda that is contracted and those that are free with respect to

82: the outermost lambda. We use the outermost lambda as the reference

83: point for this information since we hope to make all information

84: local to the contractions being made, \ie, the context of our redexes

85: should not affect the term $t'$. In the discussion that follows, we

86: shall fixate on the term starting with the outermost lambda that is

87: contracted and ignore the context in which it occurs.

88: 

89: For the variables that are free there is a renumbering which must be

90: done to account for the lambdas which occurred before the reduction

91: that are gone after the reduction. In order to define this, we

92: introduction the idea of an {\it embedding level} which is the depth

93: of a term counted by the number of lambdas between it and the

94: top level. The embedding level of $t$ in (\ref{eq:before}) is called the

95: {\it old embedding level}, $ol$, and the embedding level of $t'$ in

96: (\ref{eq:after}) is called the {\it new embedding level}, $nl$. For

97: example, if the lambdas shown are the only lambdas in the term, then

98: old embedding level is 3 and the new embedding level is 1. The number

99: of lambdas that are removed is $ol - nl$ and thus this is the

100: renumbering to be done on the free variables.  Furthermore, we can

101: easily find the free variables since they are the ones whose index is

102: greater than their embedding level, \eg, if $\#3$ occurs at embedding

103: level 2 then we know it occurs underneath two lambdas and represents

104: the first free variable outside of these lambdas.

105: 

106: In addition to renumberings for the free variables, we must provide

107: substitutions for the bound variables. In the case that a bound

108: variable does not need a substitution (since its binding lambda is not

109: contracted) we will create a dummy substitution which substitutes the

110: first free variable, $\#1$, thus preserving the term.  Now, the terms

111: within substitutions often come from a different embedding level than

112: where we are thinking of substituting them and must be renumbered so

113: that their free variables are not captured by the context into which

114: we substitute. In order to do this, for each substitution we keep a

115: number indicating the embedding level from which it came, say $l$.

116: Then when we need to perform a substitution we increment all free

117: variables in the substituted term by $nl - l$. We keep these

118: substitutions together with their embedding levels in a list, ordered

119: from the first bound variable to the last. This allows us to simply

120: add a dummy substitution to the front of this list in order to shift

121: all indices when we descend underneath an abstraction.

122: 

123: Given the previous information for encoding substitutions, we write

124: our encoding as $\env{t,ol,nl,e}$ where $t$ is the term over which

125: substitution is performed, $ol$ is the old embedding level, $nl$ is

126: the new embedding level, and $e$, called the environment, is a list of

127: substitutions for the bound variables. The overall term

128: $\env{t,ol,nl,e}$ is called a suspension. If we looked further into

129: $e$, its structure would be $(t_1,l_1)::(t_2,l_2)::\ldots::nil$ where

130: the $t_i$ are terms and $l_i$ are the corresponding embedding levels.

131: 

132: The general operation of the suspension calculus will be to perform

133: $\beta$-contractions which produce suspensions and then to apply

134: rewriting rules which move these suspensions deeper and deeper into

135: the tree until they are applied to a final term. During this, it is

136: natural that we might encounter a term of the form $\env{\env{t, ol_1,

137:     nl_1, e_1}, ol_2, nl_2, e_2}$, which represents a term $t$

138: together with two substitutions to be performed on it sequentially. We

139: can think of merging these two substitutions to produce a term of the

140: form $\env{t, ol', nl', e'}$, \ie, a single suspension which encodes

141: the information of both of the previous ones. This requires careful

142: consideration of the values for $ol'$ and $nl'$ together with new

143: syntax to represent the shape of $e'$.

144: 

145: We can determine values for $ol'$ and $nl'$ by thinking carefully

146: about the embedding levels in the term $\env{\env{t, ol_1, nl_1, e_1},

147:   ol_2, nl_2, e_2}$. Here we have two substitutions over $t$ which

148: possibly overlap with each other. In detail, the effect on $t$ is

149: first to substitute for the first $ol_1$ free variables and then to

150: raise all the free variables by $nl_1$. This raising has the effect of

151: embedding the term within $nl_1$ abstractions.  Then the second

152: substitution walks over the resulting term, substituting for the first

153: $ol_2$ free variables and then raising all the free variables by

154: $nl_2$. Note that some of these $ol_2$ substitutions will be vacuous

155: since the free variables have all been raised by $nl_1$. In fact, if

156: $nl_1 \geq ol_2$, then all of the substitutions of the second

157: suspension are vacuous. In this case we have $ol' = ol_1$ since only

158: the first $ol_1$ substitutions are performed. Also, $nl' = nl_2 +

159: (nl_1 - ol_2)$ since the raising done is that of $nl_2$ and $nl_1$

160: minus the $ol_2$ vacuous substitutions. In the case when $nl_1 <

161: ol_2$, we have $ol' = ol_1 + (ol_2 - nl_1)$ since we have the $ol_1$

162: substitutions and all but the first $nl_1$ of the $ol_2$

163: substitutions. Also, $nl' = nl_2$ since all of the $nl_1$ raisings are

164: consumed by the $ol_2$ substitutions and so the only raising left over

165: is from the second suspension. These two branching cases for

166: $ol'$ and $nl'$ can be coalesced by using the minus operator on

167: natural numbers. Then we have $ol' = ol_1 + (\monus{ol_2}{nl_1})$ and

168: $nl' = nl_2 + (\monus{nl_2}{ol_1})$ in both cases.

169: 

170: We must also determine the shape of $e'$ after merging

171: $\env{\env{t,ol_1,nl_1,e_1}, ol_2, nl_2, e_2}$ into

172: $\env{t,ol',nl',e'}$. The result should roughly be the substitutions

173: of $e_1$, modified by the substitutions in $e_2$, together with some

174: tail portion of $e_2$. For each term in $e_1$, we can use $nl_1$ to

175: compute the number of abstractions in which it is

176: embedded. Using this we can prune off the first elements of $e_2$

177: which correspond to these abstractions. When we have done this

178: for all elements of $e_1$, we only have left to determine which tail

179: portion of $e_2$ to include. The length of this tail portion should be

180: the number of abstractions consumed by the second suspension, $ol_2$,

181: minus the number of abstractions created by the first

182: suspension, $nl_1$. Thus we can compute the total shape of $e'$ by

183: knowing only $e_1$, $e_2$, $ol_2$, and $nl_1$. We write the resulting

184: form as $\menv{e_1,nl_1,ol_2,e_2}$ and we call this a {\it merged

185:   environment}.

186: 

187: \section{Syntax of the Suspension Calculus}

188: 

189: In this section we formally define the syntax of the suspension

190: calculus and present measures for assessing the wellformedness of

191: expressions in this calculus. We begin by defining the ``pre-syntax''

192: of suspension expressions, which is the raw syntax without any

193: constraints on wellformedness.

194: 

195: \begin{defn}[Pre-syntax of suspension expressions]

196: \label{def:presyntax}

197: The ``pre-syntax'' of suspension expressions is given by the following

198: definitions of the syntactic categories of ``terms'' and

199: ``environments.''

200: \begin{tabbing}

201: \qquad\=$t$\=\quad::=\quad\=\kill

202: \>$t$\>\quad::=\quad\>$c \ \vert \ \#i\ \vert\ (t\app t)\ \vert\

203: (\lambdadb t)\ \vert\ \env{t, n, n, e}$ \\

204: \>$e$\> \quad::=\quad \> $nil\ \vert\ ((t,l) :: e)\ \vert\ \menv{e, n,

205:   n, e}$

206: \end{tabbing}

207: Here $c$ ranges over an enumerable set of constants, $i$ ranges over

208: the natural numbers, and $n$ and $l$ ranges over the non-negative

209: integers.

210: \end{defn}

211: 

212: We call $\#i$ a variable index or reference, and we call $(t\app t)$

213: and $(\lambdadb t)$ application and abstraction, respectively. The

214: term $\env{t,n,n,e}$ is called a {\it suspension}. The operation $::$

215: is a consing operator on lists and the $(t,l)$ component of $((t,l) ::

216: e)$ is called an {\it environment term}. Finally, $\menv{e,n,n,e}$ is

217: called a {\it merged environment}. We collectively refer to all terms,

218: environments, and environment terms generated by the above definition

219: as {\it suspension expressions}. We will drop parenthesis by assuming

220: application is left associative, the scope of a lambda extends as far

221: right as possible, and $::$ is right associative. We will also assume

222: the obvious definition of subexpression.

223: 

224: In order to move from pre-syntax to syntax, we need to consider

225: constraints on expressions so that they ``make sense.'' For example,

226: in a term of the form $\env{t,ol_1,nl_1,e_1}$ we are thinking of

227: performing substitution for the first $ol_1$ free variables using the

228: substitutions in $e_1$. Thus the number of substitutions in $e_1$,

229: called the length of $e_1$, must be $ol_1$. Also, for each

230: substitution in $e_1$ we include an embedding level from which the

231: substitution came. Since substitutions will always move inward, it

232: must be that we keep moving to deeper embedding levels. Thus our

233: current embedding level, $nl_1$, must be greater than or equal to the

234: embedding level of every environment term in $e_1$. We enforce this by

235: defining a measure called the level of $e_1$. These measures are the

236: content of the following definitions.

237: 

238: \begin{defn}[Length of an environment]

239: \label{def:len}

240: The length of an environment $e$ is denoted by $len(e)$ and is defined

241: recursively by

242: \begin{align*}

243: len(nil) &= 0 \\

244: len((t,n) :: e) &= 1 + len(e) \\

245: len(\menv{e_1, nl_1, ol_2, e_2}) &= len(e_1) + (\monus{ol_2}{nl_1})

246: \end{align*}

247: \end{defn}

248: 

249: \begin{defn}[Level of an environment or environment term]

250: \label{def:lev}

251: The level of an environment $e$ is denote $lev(e)$ and is defined

252: recursively by

253: \begin{align*}

254: lev(nil) &= 0 \\

255: lev((t,n) :: e) &= n \\

256: lev(\menv{e_1, nl_1, ol_2, e_2}) &= lev(e_2) + (\monus{nl_1}{ol_2})

257: \end{align*}

258: \end{defn}

259: 

260: Given these two definitions, we can define the syntax of suspension

261: expressions

262: \begin{defn}[Syntax of suspension expressions]

263: \label{def:syntax}

264: The syntax of suspension expressions is those expressions in

265: \autoref{def:presyntax} with the following additional wellformedness

266: constraints,

267: \begin{enumerate}

268: \item In any subexpression of the form $\env{t,ol,nl,e}$, we

269:   must have $len(e) = ol$ and $lev(e) \leq nl$.

270: \item In any subexpression of the form $\menv{e_1,nl_1,ol_2,e_2}$, we

271:   must have $len(e_2) = ol_2$ and $lev(e_1) \leq nl_1$.

272: \item In any subexpression of the form $(t,n)::e$, we must have

273:   $lev(e) \leq n$.

274: \end{enumerate}

275: \end{defn}

276: 

277: \section{Rules of the Suspension Calculus}

278: 

279: Now that we have created syntax which embeds substitutions we can

280: consider rules which operate on this modified syntax. The effect of

281: these rules should be in three parts: (1) to contract beta redexes to

282: produce suspensions, (2) to move these suspensions down in the syntax

283: tree until they can be applied, and (3) to merge suspensions and

284: compute the resulting merged environment. The complete rules of the

285: suspension calculus are listed in \autoref{fig:susprules} and are

286: divided into three categories described above: the $\beta_s$ rules,

287: the reading rules, and the merging rules.

288: 

289: The $\beta_s$ rule simulates $\beta$-contraction in the suspension

290: calculus using the suspension syntax to encode the effect of

291: substitution. This rule rewrites the $\beta$-redex $((\lambdadb

292: t_1)\app t_2)$ to $\env{t_1, 1, 0, (t_2, 0)::nil}$ which says that we

293: substitute $t_2$ in for the first free variable in $t_1$ and decrement

294: all other free variables by one.

295: 

296: The second category of rules is the reading rules, (r1)-(r6), which

297: provide a means for moving suspensions down in a term and also

298: performing substitutions. Taken together, the $\beta_s$ rule and the

299: reading rules form an adequate simulation of the de Bruijn calculus, as

300: we shall prove in \autoref{sec:simulation}.

301: 

302: The merging rules, (m1)-(m6), are the final category of rules. The

303: (m1) rule enables us to merge two suspension into a single suspension,

304: at the cost of creating a merged environment. The rules (m2)-(m6)

305: then allow us to evaluate this merged environment in a lazy way.

306: 

307: \begin{figure}[t]

308: \begin{tabbing}

309: \quad\=(r11)\quad\=\kill

310: \> ($\beta_s$)\>$((\lambdadb t_1)\app t_2) \ra \env{t_1, 1, 0, (t_2,0)

311:   :: nil}$.\\[7pt] 

312: \> (r1)\> $\env{c,ol,nl,e} \ra c$, provided $c$ is a constant.\\[5pt]

313: \> (r2)\>$\env{\#i,0,nl,nil} \ra \#j$, where $j = i + nl$.\\[5pt] 

314: \> (r3)\> $\env{\#1,ol,nl,(t,l) :: e} \ra \env{t,0,nl',nil}$, where

315: $nl' = nl - l$.\\[5pt] 

316: \> (r4)\> $\env{\#i, ol, nl, (t,l) :: e} \ra \env{\# i',

317:   ol',nl,e},$\\

318: \>\> where $i' = i - 1$ and $ol' = ol -1$, provided $i > 1$.\\[5pt] 

319: \> (r5)\> $\env{(t_1\app t_2),ol,nl,e} \ra (\env{t_1,ol,nl,e}\app

320: \env{t_2,ol,nl,e})$.\\[5pt] 

321: \> (r6)\>$\env{(\lambdadb t), ol, nl, e} \ra (\lambdadb \env{t,

322:   ol', nl', (\#1, nl') :: e})$,\\

323: \>\> where $ol' = ol + 1$ and $nl' = nl + 1$.\\[7pt]

324: \> (m1)\>$\env{\env{t,ol_1,nl_1,e_1},ol_2,nl_2,e_2} \ra

325: \env{t,ol',nl', \menv{e_1,nl_1,ol_2,e_2}}$,\\

326: \>\>where $ol' = ol_1 + (\monus{ol_2}{nl_1})$ and $nl' = nl_2 +

327: (\monus{nl_1}{ol_2})$.\\[5pt]

328: \> (m2)\>$\menv{e_1, nl_1, 0, nil} \ra e_1$.\\[5pt] 

329: \> (m3)\>$\menv{nil, 0, ol_2, e_2} \ra e_2$.\\[5pt] 

330: \> (m4)\>$ \menv{nil, nl_1, ol_2, (t,l) :: e_2} \ra \menv{nil, nl_1',

331:   ol_2', e_2}$,\\

332: \>\> where $nl_1' = nl_1 - 1$ and $ol_2' = ol_2 - 1$, provided $nl_1

333: \geq 1$.\\[5pt]

334: \> (m5)\> $ \menv{(t,n) :: e_1, nl_1, ol_2, (s,l) ::

335:   e_2} \ra \menv{(t,n) :: e_1, nl_1', ol_2', e_2}$,\\

336: \>\>where $nl_1' = nl_1 - 1$ and $ol_2' = ol_2 - 1$, provided $nl_1 >

337: n$.\\[5pt] 

338: \> (m6)\> $\menv{(t,n) :: e_1, n, ol_2, (s,l) :: e_2} \ra

339: (\env{t, ol_2, l, (s,l) :: e_2}, m) :: \menv{e_1, n, ol_2, (s,l) :: e_2}$,\\

340: \>\>where $m = l + (\monus{n}{ol_2})$.

341: \end{tabbing}

342: \caption{Rewrite rules for the suspension calculus}

343: \label{fig:susprules}

344: \end{figure}

345: 

346: \begin{defn}

347: The reduction relations generated by the rules in

348: \autoref{fig:susprules} are denoted by $\onebetas$, $\oneread$, and

349: $\onemerge$. The relations $\onereadmerge$, $\onereadbetas$, and

350: $\oneall$ are the appropriate unions of those relations. If $R$

351: corresponds to any of these relations then we will use $R^*$ to denote

352: its reflexive and transitive closure.

353: \end{defn}

354: 

355: The following example illustrates a use of these rules where $t$,

356: $s_1$, and $s_2$ are arbitrary suspension expressions. This example is

357: a simplified version of (\ref{eq:before}).

358: \begin{align*}

359: & (\lambdadb \lambdadb ((\lambdadb t)\app s_1))\app s_2 \\

360: &\betas \env{\lambdadb \env{t, 1, 0, (s_1,0)::nil}, 1, 0, (s_2,

361:   0)::nil} \\

362: &\oneread \lambdadb \env{\env{t, 1, 0, (s_1, 0)::nil}, 2, 1, (\#1,

363:   1)::(s_2, 0)::nil} \\

364: &\onemerge \lambdadb \env{t, 3, 1, \menv{(s_1, 0)::nil, 0, 2, (\#1,

365:     1)::(s_2, 0)::nil}} \\

366: &\merge \lambdadb \env{t, 3, 1, (\env{s_1, 2, 1, (\#1,

367:     1)::(s_2,0)::nil}, 1)::(\#1,1)::(s_2,0)::nil}

368: \end{align*}

369: The outermost suspension here encodes three substitutions to be made

370: over $t$. The first substitution is $s_1$, modified by substituting

371: $s_2$ for its second free variable. The second substitution is a dummy

372: substitution which corresponds to the lambda that remains after

373: contraction. Finally, the last substitution corresponds to

374: substituting in $s_2$ and since the embedding level of this is one

375: less than the new embedding level, we will have to raise all the free

376: variables of $s_2$ which corresponds to our substituting of $s_2$

377: underneath a lambda.

378: 

379: In order for our rules to make sense, they need to produce terms

380: that make sense. In formal terms, we need to ensure that

381: using a rule on a well-formed expression produces a well-formed

382: expression.

383: 

384: \begin{theorem}

385: Let $e$ be a well-formed suspension expression and let $e \oneall

386: e'$. Then $e'$ is a well-formed suspension expression.

387: \end{theorem}

388: \begin{proof}

389: This property must be proved simultaneously with two other properties:

390: if $e$ is an environment then $lev(e) \geq lev(e')$ and $len(e) =

391: len(e')$. The reason is that if we could rewrite an environment so

392: that its level increases or so its length changes, then we might break

393: the wellformedness of an expression such as $\env{t,ol,nl,e}$ where

394: $lev(e) \leq nl$ and $len(e) = ol$ by rewriting $e$ to $e'$ such that

395: $lev(e') > nl$ or $len(e) \neq ol$. The proof of all three properties

396: simultaneously is a simple case analysis on the rewrite from $e$ to

397: $e'$. We give two examples here in order to give the flavor of the

398: argument.

399: 

400: Consider (r3) and suppose that the left hand side is well-formed. This

401: means that $ol = len((t,l)::e)$ and $nl \geq lev((t,l)::e) = l$. In

402: order for the right hand side to be well-formed we must have $0 =

403: len(nil)$ and $nl' \geq lev(nil) = 0$. The first is trivially true,

404: and the second requires that we show $nl - l \geq 0$ which follows

405: from $nl \geq l$.

406: 

407: As a second example, consider (m6). Assuming the left hand side is

408: well formed yields $n \geq lev((t,n)::e_1)$, $ol_2 = len((s,l)::e_2)$,

409: and $lev(et) \geq lev(e)$. In order to show the right hand side is

410: well-formed we must have $l \geq lev((s,l)::e_2)$, $ol_2 =

411: len((s,l)::e_2)$, $lev(et) \geq lev((s,l)::e_2)$, $m \geq

412: lev(\menv{e_1,n,ol_2,(s,l)::e_2}$, $n \geq lev(e_1)$, $ol_2 =

413: len((s,l)::e_2)$, and $l \geq lev(e_2)$. All of these follow

414: directly. Since (m6) is a rule on environments, we must also verify

415: that this rewriting does not cause the level of this environment to

416: increase. The level of the left hand side is $lev((s,l)::e_2) +

417: (\monus{n}{ol_2})$ and the level of the right hand side is $m = l +

418: (\monus{n}{ol_2})$. Since $l = lev((s,l)::e_2)$, this follows

419: easily. Finally, it is plain to see that the length is preserved.

420: \end{proof}

421: 

422: From here on we will speak only of well-formed suspension expressions

423: and thus drop the ``well-formed'' label on them. The final definition

424: and lemma of this section are ones that allows us to massage

425: environments into a convenient form for use with the rewrite

426: rules. This will be of importance in \autoref{sec:original} and

427: \autoref{sec:confluence-rm}.

428: 

429: \begin{defn}[Simple environments and truncating]

430: A simple environment is one of the form $(t_0,l_0) :: (t_1,l_1) ::

431: \ldots :: (t_{n-1}, l_{n-1}) :: nil$, with $n$ possibly zero.  For $0

432: \leq i < n$, we write $e\{i\}$ to denote the truncated environment

433: with the first $i$ elements removed, \ie, $(t_i,l_i) :: \ldots ::

434: (t_{n-1},l_{n-1}) :: nil$, with $i$ possibly zero. We extend this

435: notation by letting $e\{i\}$ denote $nil$ in the case that $i \geq

436: len(e)$ for any simple environment $e$.

437: \end{defn}

438: 

439: \begin{lemma}

440: \label{lem:eval-simple}

441: Let $e$ be an environment. Then there exists a simple environment $e'$

442: such that $e \merge e'$.

443: \end{lemma}

444: \begin{proof}

445: The proof is by case analysis on the structure of $e$, basically

446: showing that if $e$ is not a simple environment then we can always

447: apply a rule (m2)-(m6) to it. Connecting this to the result requires

448: that we also know that the rewrite rules are terminating, which is

449: shown in \autoref{sec:termination}.

450: \end{proof}

451: 

452: \section{Relationship to the Original Suspension Calculus}

453: \label{sec:original}

454: 

455: The current suspension calculus is based on the original suspension

456: calculus by Nadathur and Wilson \cite{nadathur-98-suspension}. There

457: are two differences between these calculi: the way dummy substitutions

458: are handled in the rule (r6) and the way merging is performed using

459: (m2)-(m6). In this section we highlight these differences and explain

460: the connection between these two calculi. Before we begin, however, we

461: note that the original suspension calculus had a separate syntactic

462: class for environments terms because it had more possibilities for

463: such expressions. Hence, in this section we will treat environment

464: terms as a separate syntactic class in both calculi.

465: 

466: The first difference is how dummy substitutions are handled in the

467: case of rule (r6). When pushing a suspension underneath an abstraction

468: there is a need to generate a substitution for the bound

469: variable. Since we are not actually contracting a redex, this

470: substitution should have no net effect and is thus a

471: dummy substitution compared to those substitutions generated by

472: $\beta$-contraction. In the original calculus, the rule for pushing a

473: suspension underneath an abstraction had the form

474: \[ \env{\lambdadb t, ol, nl, e} \ra \lambdadb \env{t, ol+1, nl+1,

475:   @nl::e} \] This new $@nl$ environment term was conceived of as an

476: optimization to separate real and dummy substitutions, and it also has

477: the benefit of simplifying the proof of termination for the reading

478: and merging rules. Nevertheless, we can simplify the calculus

479: significantly by using the environment term $(\#1, nl+1)$

480: instead. This environment term has the same effect the same effect and

481: also allows us to have a simpler system since we can exclude all the

482: old rules for manipulating $@nl$ forms. With this change, the results

483: of the original suspension calculus paper still hold, which we will

484: assume \cite{nadathur-98-suspension}.

485: 

486: The larger difference between the two calculi is the way merging is

487: performed using (m2)-(m6). Taking into account the change above, the

488: $\beta_s$ and reading rules are the same in both calculi, but the

489: merging rules are still significantly different. The merging rules for

490: the original calculus are presented in \autoref{fig:original}. The

491: rule (m8') makes use of a measure called the index which we will say

492: more about later in this section. For now, it is sufficient to think

493: of the index as a measure very similar to the level. Pay special

494: attention to (m5') which says

495: \[ \menv{et::e_1, nl_1, ol_2, e_2} \ra \menvt{et, nl_1, ol_2, e_2} ::

496: \menv{e_1, nl_1, ol_2, e_2} \] The effect of this rule is to eagerly

497: propagate the effects of $e_2$ onto the environment term $et$ by

498: creating a new environment term $\menvt{et, nl_1, ol_2, e_2}$. This

499: new form is then used to prune $e_2$ using rules (m6') and (m7') until

500: only the portion relevant to $et$ was left. In the current calculus,

501: this pruning is done using the form $\menv{e_1, nl_1, ol_2, e_2}$

502: using rule (m5) and thus the work of this pruning is shared for each

503: environment term of $e_1$. This change in the current calculus allows

504: us to use fewer syntactic forms and also fewer rules, both of which

505: reduce the energy required to understand the calculus.

506: 

507: A possible downside of these simplifications is that we might lose

508: some desirable theoretical properties of the calculus. This turns out

509: not to be the case as we prove later in this chapter. In fact, the

510: simplifications to the calculus allow new results such as a typed

511: version of the calculus in \autoref{sec:typed-suspension} and a

512: translation to another explicit substitution calculus in

513: \autoref{sec:lambdasigma}. In the rest of this section, we will look

514: at a more formal relationships between our calculus and its

515: predecessor.

516: 

517: \begin{figure}[t]

518: \begin{tabbing}

519: \qquad (r11)\qquad\=\kill \qquad (m1')\>

520: $\env{\env{t,ol_1,nl_1,e_1},ol_2,nl_2,e_2} \ra

521: \env{t,ol',nl', \menv{e_1,nl_1,ol_2,e_2}}$,\\

522: \>where $ol' = ol_1 + (\monus{ol_2}{nl_1})$ and $nl' = nl_2 +

523: (\monus{nl_1}{ol_2})$.\\

524: [5pt]

525: \qquad (m2')\>$\menv{nil, nl, 0, nil} \ra nil$.\\

526: [5pt]

527: \qquad (m3')\> $\menv{nil, 0, ol, e} \ra e$.\\

528: [5pt] \qquad (m4')\>$\menv{nil, nl, ol, et :: e} \ra \menv{nil,

529:   nl', ol', e}$,\\

530: \>where $nl,ol \geq 1$, $nl' = nl - 1$ and $ol' = ol - 1$.\\

531: [5pt] \qquad (m5')\> $\menv{et :: e_1, nl,ol,e_2} \ra \menvt{et,nl,ol,e_2}

532: :: \menv{e_1,nl,ol,e_2}$.\\

533: [5pt]

534: \qquad (m6')\> $\menvt{et,nl,0,nil} \ra et$.\\

535: [5pt] \qquad (m7') \>$\menvt{et,nl,ol,et' :: e} \ra \menvt{et, nl',ol', e},$\\

536: \>where $nl' = nl - 1$ and $ol' = ol - 1$, provided $ind(et) < nl$.\\

537: [5pt] \qquad (m8')\>$\menvt{(t,nl),nl,ol,et :: e} \ra (\env{t,ol,l',et :: e}, m)$\\

538: \>where $l' = ind(et)$ and $m = l' + (\monus{nl}{ol})$.

539: \end{tabbing}

540: \caption{Merging rules for the original suspension calculus}

541: \label{fig:original}

542: \end{figure}

543: 

544: Suspension expressions in our context are a subset of the original

545: suspension expressions. The only difficultly in showing this is that

546: wellformedness rules for the original suspension calculus are defined

547: the same as in \autoref{def:syntax} except with the measure

548: level replaced by the measure index, defined as follows.

549: 

550: \begin{defn}[Index of an environment or environment term]

551: \label{def:ind}

552: Given a natural number $i$, the $i$-th index of an environment $e$ is

553: denoted by $ind_{i}(e)$ and is defined as follows:

554: \begin{enumerate}

555: \item If $e$ is $nil$ then $ind_{i}(e) = 0$.

556: \item If $e$ is $(t,k) :: e'$

557: then $ind_{i}(e)$ is $k$ if $i = 0$ and $ind_{i-1}(e')$ otherwise.

558: \item If $e$ is $\menv {e_1,nl,ol,e_2 }$, let

559:  $m = (\monus{nl}{ind_{i}(e_1)})$ and $l = len(e_1)$. Then

560: \begin{tabbing}

561: \qquad\=\kill

562: \>$ind_{i}(e) = \left\{ \begin{array}{ll}

563:       ind_{m}(e_2) + (\monus{nl}{ol}) &

564:                 \mbox{ if $i < l$ and  $len(e_2) > m$}\\ 

565:       ind_{i}(e_1)   & \mbox{ if $i < l$ and  $len(e_2) \leq  m$}\\

566:       ind_{(i - l+nl)}(e_2) & \mbox{ if $i \geq l$.}

567:                         \end{array} 

568:                \right.$

569: \end{tabbing}

570: \end{enumerate}

571: The index of an environment, denoted by $ind(e)$, is

572: $ind_{0}(e)$.

573: \end{defn}

574: 

575: Intuitively, the index of an environment is the embedding level of its

576: first environment term and zero if the environment is nil. The index

577: of an environment term $et$ is the value of $n$ for which $et \merge

578: (t,n)$.  We can consider the index measure on expressions in the

579: current calculus as well. Note that this measure is equal to the level

580: on environments terms in the current calculus because they already

581: have the form $(t,n)$. The only difference in the current calculus

582: between index and level is in the case of merged environments, where

583: the level is an upper bound on the index.

584: 

585: \begin{lemma}

586: Let $e$ be a well-formed environment in the current calculus. Then

587: $lev(e) \geq ind(e)$.

588: \end{lemma}

589: \begin{proof}

590: First generalize to $lev(e) \geq ind_i(e)$ for all $i$. Then the proof

591: proceeds by induction on the structure of $e$.

592: \end{proof}

593: 

594: \begin{lemma}

595: Well-formed terms in the current suspension calculus are well-formed

596: in the original suspension calculus.

597: \end{lemma}

598: \begin{proof}

599: This is a direct consequence of the previous lemma. For example, if

600: $\env{t, ol, nl, e}$ is a well-formed term of the current calculus

601: then we have $ol = len(e)$ and $nl \geq lev(e) \geq ind(e)$. Thus it

602: is a well-formed term in the original suspension calculus.

603: \end{proof}

604: 

605: We now know that the well-formed expressions we are working with in

606: the current calculus are also well-formed in the original calculus. We

607: can also show that the rules of the current calculus are either

608: derived or admissible rules for the original calculus. We will

609: consider each rule of the current calculus in turn, ignoring rules

610: that are the same in both calculi, \ie, (m1), (m3), and (m4).

611: 

612: The rule (m2) operates on an environment of the form $\menv{e_1, nl_1,

613:   0, nil}$. By \autoref{lem:eval-simple}, the environment $e_1$ can

614: be rewritten to the form $et_0::et_1::\ldots::et_{n-1}::nil$.  Then by

615: applying (m5') $n$ times we can get

616: \[ \menvt{et_0, nl_1, 0, nil} :: \menvt{et_1, nl_1, 0, nil}

617: :: \ldots :: \menvt{et_{n-1}, nl_1, 0, nil} :: \menv{nil, nl_1, 0,

618:   nil} \]

619: Using (m2') and $n$ applications of (m6') this rewrites to $et_0 ::

620: et_1 :: \ldots :: et_{n-1} :: nil$. Thus both $\menv{e_1, nl_1, 0, nil}$

621: and $e_1$ can rewrite to a common term and therefore the rule (m2) is

622: admissible.

623: 

624: For rule (m5) we cite the original suspension paper where Lemma 6.10

625: states that $\menv{e_1, nl + 1, ol + 1, et::e_2}$ and $\menv{e_1, nl,

626:   ol, e_2}$ rewrite to a common term if $ind(e_1) \leq nl$

627: \cite{nadathur-98-suspension}. Restricting this to the case where

628: $e_1 = (t,n)::e_1'$ and restating the requirement as $n < nl + 1$

629: yields the rule (m5). Thus (m5) is admissible.

630: 

631: Finally consider (m6). Assuming $\menv{(t,n)::e_1, n, ol_2, et::e_2}$

632: is a term in the current suspension calculus, we can rewrite it using

633: (m5') followed by (m8') to produce

634: \[ (\env{t,ol_2,l,et::e_2},m)::\menv{e_1, n, ol_2, et::e_2} \] where

635: $l = ind(et)$ and $m = l + (\monus{n}{ol_2})$. Since $et$ is an

636: environment term in the current calculus we have $l = lev(et)$ and

637: thus (m6) is a derived rule of the original calculus.

638: 

639: We can formalize our observations into the following theorem which

640: will be useful in \autoref{sec:simulation} when we show that the

641: current calculus properly simulates $\beta$-contraction.

642: 

643: \begin{theorem}[Same normal form]

644: \label{thm:same-nf}

645: Let $x$ be a well-formed (current) suspension expression. Then the

646: $\onereadmerge$-normal form of $x$ is also the $\onereadmergep$-normal

647: form of $x$.

648: \end{theorem}

649: \begin{proof}

650: This theorem depends on result that the reading and merging rules are

651: confluent and terminating in both calculi (See

652: \autoref{sec:termination} and \autoref{sec:confluence-rm} for the

653: current calculus, \cite{nadathur-98-suspension} for the original

654: calculus). The result then follows by induction on the rewrite

655: sequence which takes $x$ to its $\onereadmerge$-normal form.

656: \end{proof}

657: 

658: \section{Typed Version of the Suspension Calculus}

659: \label{sec:typed-suspension}

660: 

661: In this section we present a typed version of the suspension calculus

662: which was not previously possible with the original suspension

663: calculus. This typed version is is consistent with the simply-typed

664: lambda calculus from \autoref{sec:typed} and motivated in the same

665: way. In fact our typing judgment for terms of the

666: form $c$, $(\lambdadb t)$, and $(t_1\app t_2)$ is the same as in the

667: simply-typed lambda calculus, but significant complexity is introduce

668: to handle the new judgment for $\env{t,ol,nl,e}$. The issue is that

669: we must interpret the term $t$ in the context of the substitutions

670: encoded in $e$ and relative to $nl$. This necessitates a new judgment

671: which talks about the effect of an environment (relative to an

672: embedding level) on a typing context. The form of this judgment is

673: $\Gamma \yields e \one{nl} \Gamma'$. Where $\Gamma$ and $\Gamma'$ are

674: contexts, $\Sigma$ is a signature, $e$ is an environment, and $nl$ is

675: an integer for the embedding level. All of typing rules are presented

676: in \autoref{fig:typed-suspension}.

677: 

678: \begin{figure}[t]

679: \begin{align*}

680: &\infer[\mbox{where $c : A \in \Sigma$}]{\Gamma \yields c : A}{}

681: &

682: &\infer{A.\Gamma \yields \#1 : A}{} \\

683: \\

684: &\infer[\mbox{where $i > 1$}]{A.\Gamma \yields \#i : A'}{\Gamma

685:   \yields \#(i-1) : A'}

686: &

687: &\infer{\Gamma \yields (t_1\app t_2) : A}{\Gamma \yields

688:   t_1 : B \to A & \Gamma \yields t_2 : B} \\

689: \\

690: &\infer{\Gamma \yields (\lambdadbann{A} t) : A \to B}{A.\Gamma

691:   \yields t : B}

692: &

693: &\infer{\Gamma \yields \env{t,ol,nl,e} : A}{\Gamma \yields

694:   e \one{nl} \Gamma' & \Gamma' \yields t : A} \\

695: \\ \\

696: &\infer{\Gamma \yields nil \one{0} \Gamma}{}

697: &

698: &\infer[\mbox{where $nl > 0$}]{A.\Gamma \yields nil \one{nl}

699:   \Gamma'}{\Gamma \yields nil \one{nl-1} \Gamma'} \\

700: \\

701: &\infer[\mbox{where $nl > n$}]{A.\Gamma \yields (t,n)::e \one{nl}

702:   \Gamma'}{\Gamma \yields (t,n)::e \one{nl-1} \Gamma'}

703: &

704: &\infer{\Gamma \yields (t,n)::e \one{n} A.\Gamma'}{\Gamma \yields t :

705:   A & \Gamma \yields e \one{n} \Gamma'} \\

706: \\

707: &\infer{\Gamma \yields \menv{e_1, nl', ol', e_2} \one{nl}

708:   \Gamma''}{\Gamma \yields e_2 \one{nl - (\monus{nl'}{ol'})}

709:   \Gamma' & \Gamma' \yields e_1 \one{nl'} \Gamma''} \\

710: \end{align*}

711: \caption{Typing rules for the typed suspension calculus}

712: \label{fig:typed-suspension} 

713: \end{figure}

714: 

715: The following result establish the wellformedness of our typing

716: judgments.

717: 

718: \begin{theorem}

719: Type judgments are preserved by the rewrite relations

720: \end{theorem}

721: \begin{proof}

722: The critical thing to show is that if $\ell \to r$ is a rewrite rule

723: and $\Gamma \yields \ell : A$ (respectively $\Gamma \yields \ell

724: \one{nl} \Gamma'$) then $\Gamma \yields r : A$ (respectively $\Gamma

725: \yields r \one{nl} \Gamma'$). The proof proceeds by cases on the

726: rewrite rule and we focus here on a few interesting cases.

727: 

728: Let the rewrite rule be $(\beta_s)$. Then we are given that $\Gamma

729: \yields ((\lambdadbann{A} t_1)\app t_2) : B$ from which we know the

730: derivation tree must be

731: \[

732: \infer{\Gamma \yields ((\lambdadbann{A} t_1)\app t_2) : B}{

733:   \infer{\Gamma \yields (\lambdadbann{A} t_1) : A \to B}{

734:     \infer{A.\Gamma \yields t_1 : B}{D_1}}

735:   && \infer{\Gamma \yields t_2 : A}{D_2}}

736: \]

737: Where $D_1$ and $D_2$ are appropriate derivations. We can then use

738: these derivations to construct the following typing judgment.

739: \[

740: \infer{\Gamma \yields \env{t_1,1,0,(t_2,0)::nil}}{

741:   \infer{\Gamma \yields (t_2,0)::nil \one{0} A.\Gamma}{

742:     \infer{\Gamma \yields t_2 : A}{D_2}

743:     && \Gamma \yields nil \one{0} \Gamma}

744:   && \infer{A.\Gamma \yields t_1 : B}{D_1}}

745: \]

746: This completes the argument for $(\beta_s)$.

747: 

748: Consider the case of (r3). Then we must have the following typing

749: derivation.

750: \[

751: \infer{A_{nl}.A_{nl-1}.\cdots.A_{l+1}.\Gamma \yields

752:   \env{\#1,ol,nl,(t,l)::e} : A}{

753:   \infer{A_{nl}.A_{nl-1}.\cdots.A_{l+1}.\Gamma \yields

754:     (t,l)::e \one{nl} A.\Gamma'}{

755:     \infer{A_{nl-1}.\cdots.A_{l+1}.\Gamma \yields

756:       (t,l)::e \one{nl-1} A.\Gamma'}{

757:       \infer{\vdots}{

758:         \infer{\Gamma \yields (t,l)::e \one{l} A.\Gamma'}{

759:           \infer{\Gamma \yields t : A}{D_1}

760:           && \infer{\Gamma \yields e \one{l} \Gamma'}{D_2}}}}}

761:   && A.\Gamma' \yields \#1 : A}

762: \]

763: From this we can construct the typing judgment,

764: \[

765: \infer{A_{nl}.A_{nl-1}.\cdots.A_{l+1}.\Gamma \yields

766:   \env{t,0,nl-l,nil} : A}{

767:   \infer{A_{nl}.A_{nl-1}.\cdots.A_{l+1}.\Gamma \yields nil \one{nl-l}

768:     \Gamma}{

769:     \infer{A_{nl-1}.\cdots.A_{l+1}.\Gamma \yields nil \one{nl-l-1}

770:       \Gamma}{

771:       \infer{\vdots}{\Gamma \yields nil \one{0} \Gamma}}}

772:   && \infer{\Gamma \yields t : A}{D_1}}

773: \]

774: 

775: As a final example, consider the rule (m3) which yields the following

776: typing derivation.

777: \[

778: \infer{\Gamma \yields \menv{nil, 0, ol_2, e_2} \one{nl} \Gamma'}{

779:   \infer{\Gamma \yields e_2 \one{nl} \Gamma'}{D_1}

780:   && \Gamma' \yields nil \one{0} \Gamma'}

781: \]

782: And this directly contains the needed typing judgment.

783: \[

784: \infer{\Gamma \yields e_2 \one{nl} \Gamma'}{D_1}

785: \]

786: \end{proof}

787: 

788: \section{Meta Variables and the Suspension Calculus}

789: \label{sec:susp-metavars}

790: 

791: The syntax of suspension expressions does not presently allow for meta

792: variables, as described in \autoref{sec:metavars}. We can remedy

793: this by adding modifying the syntax of terms to

794: \begin{tabbing}

795: \qquad\=$t$\=\quad::=\quad\=\kill

796: \>$t$\>\quad::=\quad\>$v\ \vert\ c \ \vert \ \#i\ \vert\ (t\app t)\ \vert\

797: (\lambdadb t)\ \vert\ \env{t, n, n, e}$,

798: \end{tabbing}

799: where $v$ represents the category of meta variables. Because such

800: variables have a logical interpretation, any substitution for them

801: must avoid capturing local variables. This means that any outer

802: context cannot effect the value of such variables. To accommodate this

803: interpretation, we can add the following to our reading rules:

804: \begin{tabbing}

805: \qquad (r7)\qquad\=\kill

806: \qquad (r7)\> $\env{v,ol,nl,e} \ra v$, if $v$ is a meta variable.

807: \end{tabbing}

808: This rule has the same character as the (r1) rule for constants, and

809: as a result, all the properties of the suspension calculus without

810: logical meta variables carry over to the suspension calculus with

811: logical meta variables.

812: 

813: An alternative interpretation for meta variables in one in which

814: substitution is performed without renaming to avoid variable

815: capture. This is referred to as the {\it graftable} interpretation of

816: meta variables, and it has been found useful in higher-order

817: unification procedures \cite{dowek-95-higherorder}. The benefit of

818: using graftable meta variables is that dependencies of meta variables

819: on the outside context no longer need to be explicitly specified,

820: which turns out to be a significant cost in the traditional

821: higher-order unification algorithm \cite{huet-75-unification}. On the

822: other hand, it may seem that using graftable meta variables removes

823: any possibility of control over dependencies, but we can in fact

824: enforce some restrictions using explicit raising. For example, to

825: prevent the metavariable $X$ from depending the the de Bruijn indices

826: $\#1$ and $\#2$, we can replace it with the term

827: $\env{X,0,2,nil}$. This also us to simulate logical meta variables

828: using graftable meta variables simply by lifting such graftable

829: variables so that they can not depend on any of the bound variables in

830: the term.

831: 

832: In order to support graftable meta variables in the calculus, we

833: extend the syntax as before, but instead of adding the rule (r7), we

834: leave the rules unchanged. This is consistent with the graftable

835: interpretation: because we know nothing about such meta variables, we

836: cannot say what effect a suspension will have on them. Adding

837: graftable meta variables to the calculus, however, introduces some new

838: complications with respect to confluence. For example, consider the

839: term $((\lambdadb ((\lambdadb X)\app t_1))\app t_2)$ in which $X$ is a

840: graftable meta variable and $t_1$ and $t_2$ are terms in

841: $\onereadmerge$-normal form. This term can be rewritten to

842: \begin{tabbing}

843: \qquad\=\kill

844: \> $\env{\env{X,1,0,(t_1,0)::nil},1,0,(t_2,0)::nil}$

845: \end{tabbing}

846: and also to 

847: \begin{tabbing}

848: \qquad\=\kill

849: \> $\env{\env{X,2,1,(\#1,1)::(t_2,0)::nil},1,0,

850:       (\env{t_1,1,0,(t_2,0)::nil},0)::nil}$,

851: \end{tabbing}

852: amongst other terms. It is easy to see that these terms cannot now be

853: rewritten to a common form using only the reading and $(\beta_s)$

854: rules. The merging rules are essential to this ability and, as we see

855: in \autoref{sec:confluence-rm}, these also suffice for this

856: purpose. Another impact of graftable meta variables is that normal

857: forms with respect to the reading and merging rules now include the

858: possibility of remaining suspensions, whereas without graftable meta

859: variables such normal forms are always de Bruijn terms.

860: 

861: We assume henceforth that the suspension calculus includes meta

862: variables under the graftable interpretation. For reasons already

863: mentioned, it is easy to see that the properties we establish for the

864: resulting calculus will hold also under the logical interpretation.

865: 

866: \section{Termination of Reading and Merging Rules}

867: \label{sec:termination}

868: 

869: The first significant property we prove for the suspension calculus is

870: that the reading and merging rules are terminating, \ie, that all

871: $\onereadmerge$-sequences are finite. This is useful in all future

872: sections because it allows us to induct on $\onereadmerge$-sequences,

873: and it tells that $\onereadmerge$-normal forms always exist. On a

874: deeper level, the substitution process in the lambda calculus is

875: inherently finite and by showing that our elaboration of this

876: substitution process is also finite, we argue convincingly for the

877: well behaved nature of our rules.

878: 

879: We prove the termination of the reading and merging rules in two

880: steps. First, we describe a collection of first-order terms and a

881: wellfounded order on those terms using a lexicographic recursive path

882: ordering \cite{dershowitz-82-orderings,

883:   ferreira-94-wellfoundedness}. Second, we define a mapping from

884: suspension expressions to newly described terms such that each of the

885: reading and merging rules produces a smaller term with respect to the

886: defined order. The desired conclusion follows from these facts. The

887: key points of this work have been verified in Coq.\footnote{\url{http://www-users.cs.umn.edu/~agacek/pubs/gacek-masters/Termination/}}

888: 

889: We imagine the terms we describe here to be an abstract view of the

890: suspension calculus such that only details relevant to the termination

891: of the reading and merging rules are considered. These terms 

892: are constructed using the following (infinite) vocabulary:

893: the following (infinite) vocabulary: the 0-ary function symbol {\it

894:   *}, the unary function symbol {\it lam}, and the binary function

895: symbols {\it app}, {\it cons} and, for each positive number $i$,

896: $s_i$. We denote this collection of terms by $\cal T$. We assume the

897: following partial ordering $\sqsupset$ on the signature underlying

898: $\cal T$: $s_i \sqsupset s_j$ if $i > j$ and, for every $i$, $s_i

899: \sqsupset {\it app}$, $s_i \sqsupset {\it lam}$, $s_i \sqsupset {\it

900:   cons}$ and $s_i \sqsupset {\it *}$. This ordering is now extended to

901: the collection of terms.

902: 

903: \begin{defn}[Term Order]

904: \label{def:termorder}

905: The relation $\succ$ on $\cal T$ is inductively defined by the

906: following property: Let $s = f(s_1,\ldots,s_m)$ and $t =

907: g(t_1,\ldots,t_n)$; both $s$ and $t$ may be {\it *}, \ie, the number

908: of arguments for either term may be $0$. Then $s \succ t$ if 

909: \begin{enumerate}

910: \item $f = g$ (in which case $n = m$), $(s_1, \ldots, s_n) \succ_{lex}

911:   (t_1,\ldots,t_n)$, and, $s \succ t_i$ for all $i$ such that $1 \leq

912:   i \leq n$, or

913: \item $f \sqsupset g$ and $s \succ t_i$ for all $i$ such that $1 \leq

914:   i \leq n$, or

915: \item $s_i = t$ or $s_i \succ t$ for some $i$ such that $1 \leq i \leq

916:   m$.

917: \end{enumerate}

918: Here $\succ_{lex}$ denotes the lexicographic ordering induced by

919: $\succ$. 

920: \end{defn}

921: 

922: In the terminology of \cite{ferreira-94-wellfoundedness}, $\succ$ is

923: an instance of a recursive path ordering based on $\sqsupset$. It is

924: easily seen that $\sqsupset$ is a well-founded ordering on the

925: signature underlying $\cal T$. The results in

926: \cite{ferreira-94-wellfoundedness} then imply the following:

927: 

928: \begin{lemma}

929: \label{lem:succ-wellfounded}

930: $\succ$ is a well-founded partial order on $\cal T$.

931: \end{lemma}

932: 

933: We now consider the translation from suspension expressions to $\cal

934: T$. The critical part of this mapping is the treatment of expressions

935: of the form $\env{t,ol,nl,e}$ and $\menv{e_1,nl,ol,e_2}$. Because of

936: (m1) and (m6), there is a tight relationship between the encoding of

937: these two types of expressions. It turns out that we can ignore the

938: differences between them when looking at our abstract view of the

939: suspension calculus, thus we drop the $ol$ and $nl$ from each and

940: encode them as $s_i$ for some $i$.

941: 

942: To determine the appropriate value for $i$ in $s_i$, we must consider

943: how this $i$ will be needed. We will focus on the case for

944: $\env{t,ol,nl,e}$, but the same ideas will carry over to

945: $\menv{e_1,nl,ol,e_2}$. A first attempt to translate $\env{t,ol,nl,e}$

946: as $s_i$ for some fixed $i$ would fail since the rule (r3) would not

947: yield a smaller term when applied due to the lexicographic component

948: of our ordering. Instead, we use the the value of $i$ as a coarse

949: measure of the remaining substitution work, so that this value

950: decreases in the rule (r3). In order for this to work we must count

951: the $\#1$ on the left-hand side of (r3) for some positive amount. This

952: then passes the problem onto (r6) where we add a $\#1$ to the

953: right-hand side. In order to balance this, we assign lambdas a weight

954: based on the number of suspensions in which they are embedded. This

955: results in our family of measures $\eta_j$ where $j$ represents the

956: number of levels of suspensions or merged environments that the

957: current term is embedded underneath. In defining this measure we must

958: be aware that the rule (m1) allows the environment $e_2$ to become

959: embedded underneath an additional level. Thus the embedding level of

960: an environment must be based on the number of suspensions in the term

961: over which the environment applies. We call this count of suspensions

962: the ``internal embedding potential'' and denote it by $\mu$ in the

963: following definitions. In these definitions, {\it max} is the function

964: that picks the larger of its two integer arguments.

965: 

966: \begin{defn}\label{def:intembedding} 

967: The measure $\mu$ that estimates the

968:   internal embedding potential of a suspension expression is defined as

969:   follows:

970: \begin{enumerate}

971: \item For a term $t$, $\mu(t)$ is $0$ if $t$ is a constant, a meta

972:   variable or a de Bruijn index, $\mu(s)$ if $t$ is $(\lambdadb

973:   s)$, ${\it  max}(\mu(s_1),\mu(s_2))$ if $t$ is $(s_1\app

974:   s_2)$, and  $\mu(s) + \mu(e) + 1$ if $t$ is

975:   $\env{s,ol,nl,e}$.  

976: 

977: \item For an environment $e$, $\mu(e)$ is $0$ if $e$ is nil,

978:   ${\it max}(\mu(s),\mu(e_1))$ if $e$ is $(s,l) :: e_1$ and

979:   $\mu(e_1) + \mu(e_2) + 1$ if $e$ is $\menv{e_1,nl,ol,e_2}$.

980: \end{enumerate}

981: \end{defn}

982: 

983: \begin{defn}\label{def:suspsize}

984: The measures $\eta_i$ on terms and environments for each natural

985: number $i$ are defined simultaneously by recursion as follows:

986: \begin{enumerate}

987: \item For a term $t$, $\eta_i(t)$ is $1$ if $t$ is a constant, a meta

988:   variable or a de Bruijn index, $\eta_i(s) + 1$ if $t$ is $(\lambdadb

989:   s)$, ${\it  max}(\eta_i(s_1),\eta_i(s_2)) + 1$ if $t$ is $(s_1\app

990:   s_2)$,and  $\eta_{i+1}(s) + \eta_{i+1+\mu(s)}(e) + 1$ if $t$ is

991:   $\env{s,ol,nl,e}$.  

992: 

993: \item For an environment $e$, $\eta_i(e)$ is $0$ if $e$ is nil,

994:   ${\it max}(\eta_i(s),\eta_i(e_1))$ if $e$ is $(s,l) :: e_1$ and

995:   $\eta_{i+1}(e_1) + \eta_{i+1+\mu(e_1)}(e_2) + 1$ if $e$ is

996:   $\menv{e_1,nl,ol,e_2}$.

997: \end{enumerate}

998: \end{defn}

999: 

1000: \begin{defn}\label{def:susptoessence}

1001: The translation $\ess$ of suspension expressions to $\cal

1002: T$ is defined as follows:

1003: \begin{enumerate}

1004: \item For a term $t$, $\ess(t)$ is {\it *} if $t$ is a

1005:   constant a meta variable or a de Bruijn index,

1006:   ${\it app}(\ess(t_1),\ess(t_2))$ if $t$ is $(t_1\app t_2)$,

1007:   ${\it lam}(\ess(t'))$ if $t$ is $(\lambdadb t')$ and

1008:   $s_i(\ess(t'),\ess(e'))$ where $i = \eta_0(t)$ if $t$ is

1009:   $\env{t',ol,nl,e'}$. 

1010: 

1011: \item For an environment $e$, $\ess(e)$ is {\it *} if $e$ is

1012:   {\it nil}, ${\it cons}(\ess(t'),\ess(e'))$ if $e$ is

1013:   $(t',l) :: e'$ and $s_i(\ess(e_1), \ess(e_2))$ where $i =

1014:   \eta_0(e)$ if $e$ is $\menv{e_1,nl,ol,e_2}$.

1015: \end{enumerate}

1016: \end{defn}

1017: 

1018: Using this translation we now lift our ordering on this collection of

1019: first-order terms to suspension expressions.

1020: 

1021: \begin{defn}[Suspension Expression Order]

1022: \label{def:exprorder}

1023: For suspension expressions $s$ and $t$ we say $s \gg t$ if and only if

1024: $\ess(s) \succ \ess(t)$.

1025: \end{defn}

1026: 

1027: There key properties of the $\succ$ relation carry over to the $\gg$

1028: relation. First, subexpressions are smaller than their parent

1029: expressions. Second, the relation is monotonic in the sense that if

1030: $v$ results from $u$ by replacement of a subpart $x$ by $y$ such that

1031: $x \gg y$, then $u \gg v$. Third, the relation is wellfounded.  These

1032: properties together with the following theorem will make this relation

1033: a powerful tool for performing induction over suspension expressions.

1034: 

1035: \begin{theorem}

1036: \label{thm:rm-termination}

1037: Every rewriting sequence based on the reading and merging rules

1038: terminates.

1039: \end{theorem}

1040: \begin{proof}

1041: A tedious but straightforward inspection of each of the reading and

1042: merging rules verifies the following: If $l \ra r$ is an instance of

1043: these rules, then $l \gg r$, $\mu(l) \geq \mu(r)$, and, for every

1044: natural number $i$, $\eta_i(l) \geq \eta_i(r)$.  Further, it is easily

1045: seen that if $x$ and $y$ are both either terms or environments such

1046: that $\mu(x) \geq \mu(y)$ and $\eta_i(x) \geq \eta_i(y)$ for each

1047: natural number $i$ and if $v$ is obtained from $u$ by substituting $y$

1048: for $x$, then $\eta_i(u) \geq \eta_i(v)$ for each natural number

1049: $i$. From these observations it follows easily that if $t_1

1050: \onereadmerge t_2$ then $t_1 \gg t_2$. The theorem is

1051: now a consequence of \autoref{lem:succ-wellfounded}.

1052: \end{proof}

1053: 

1054: \section{Confluence of Reading and Merging Rules}

1055: \label{sec:confluence-rm}

1056: 

1057: In this section we prove that the reading and merging rules are

1058: confluent, \ie, that the choices we make in rewriting can always be

1059: reconciled. Thus $\onereadmerge$-normal forms are unique, which is

1060: another argument for the coherence of our reading and merging rules.

1061: 

1062: The property of confluence states that given terms $f$, $g$, and $h$

1063: such that $f \readmerge g$ and $f \readmerge h$, there exists a term

1064: $k$ such that $g \readmerge k$ and $h \readmerge k$. This can be

1065: expressed using the diagrams described in \autoref{sec:confluence}

1066: as,

1067: \begin{center}

1068: \begin{minipage}{5cm}

1069: \xymatrix{

1070: f \ar@{->}[dd]_{\readmerge} \ar@{->}[rr]^{\readmerge} &&

1071: g \ar@{-->}[dd]^{\readmerge} \\

1072: \\

1073: h \ar@{-->}[rr]^{\readmerge} && k \\

1074: }

1075: \end{minipage}

1076: \end{center}

1077: A well known result (proved, for instance, in

1078: \cite{huet-80-confluent}) in rewriting is that a terminating rewriting

1079: system is confluent if it is weakly confluent. Weak confluence is

1080: states that given terms $f$, $g$, and $h$ such that $f \onereadmerge

1081: g$ and $f \onereadmerge h$, there exists a term $k$ such that $g

1082: \readmerge k$ and $h \readmerge k$, \ie, that the following figure

1083: holds.

1084: \begin{center}

1085: \begin{minipage}{5cm}

1086: \xymatrix{

1087: f \ar@{->}[dd]_{\onereadmerge} \ar@{->}[rr]^{\onereadmerge} &&

1088: g \ar@{-->}[dd]^{\readmerge} \\

1089: \\

1090: h \ar@{-->}[rr]^{\readmerge} && k \\

1091: }

1092: \end{minipage}

1093: \end{center}

1094: This is much easier to show since we only need to consider one rewrite

1095: step from $f$ to $g$ and from $f$ to $h$. In doing this, we must

1096: consider each possible overlap between any two rules. The most

1097: complicated of these is the overlap of (m1) with itself when applied

1098: to a term of the form

1099: \[ \env{\env{\env{t, ol_1, nl_1, e_1}, ol_2, nl_2, e_2}, ol_3, nl_3,

1100: e} \] This leads us to develop an associativity property for

1101: merged environments which is the content of the following

1102: section.

1103: 

1104: \subsection{An Associativity Property for Environment Merging}

1105: \label{sec:assoc}

1106: 

1107: Here we show that the following two environments rewrite to a

1108: common environment.

1109: \[ A = \menv{\menv{e_1, nl_1, ol_2, e_2}, nl_2 +

1110:   (\monus{nl_1}{ol_2}), ol_3, e_3} \]

1111: \[ B = \menv{e_1, nl_1, ol_2 + (\monus{ol_3}{nl_2}), \menv{e_2,

1112:     nl_2, ol_3, e_3}} \]

1113: Essentially this tells us that to compute the effect of $e_2$ on

1114: $e_1$ and then compute the effect of $e_3$ on the result is the

1115: same as computing the effect of $e_3$ on $e_2$ and then computing

1116: the effect of that result on $e_1$. Ignoring the details for a moment,

1117: suppose that $e_1 = (t_1,n_1)::e_1'$ and we are able to apply the rule

1118: (m6) to both terms (that is twice to $A$ and once to $B$). Then the

1119: term portion of the environment term for $A$ is roughly 

1120: \[ \env{\env{t_1,ol_2,nl_2,e_2},ol_3,nl_3,e_3} \]

1121: and for $B$ it is roughly

1122: \[ \env{t_1, ol_2 + (\monus{ol_3}{nl_2}), nl_3 + (\monus{nl_2}{ol_3}),

1123:   \menv{e_2,nl_2,ol_3,e_3}} \]

1124: Then we can apply (m1) to bring these two terms back together. This is

1125: the heart of the proof. The vast majority of the proof is taken up by

1126: details and corner cases. For instance, we might not be able to apply

1127: (m6) to a term $\env{(t_1,n_1)::e_1,nl_1,ol_2,e_2}$ because $nl_1 >

1128: n_1$, $e_2$ is nil, or $e_2$ isn't of the form $(t_2,n_2)::e_2'$. All

1129: of these cases must be handled and often doubly so since we have to

1130: apply (m6) twice to the term $A$. In order to ease these pains, we

1131: introduce a few lemmas which we can use to massage expressions into the

1132: proper form.

1133: 

1134: The rules (m4), (m5), and (m6) require their second environment to be

1135: of the form $(t,n)::e$ which isn't the case with merged environments like

1136: in the term $B$. Ideally we could use the rules (m5) and (m6) to turn

1137: a term of the form $\menv{e,nl,ol,e'}$ into one of the form $(t,n)::e$,

1138: but if we do this we will not be able to use our inductive hypothesis.

1139: To accommodate this issue we introduce the following lemmas which

1140: essentially state that applying the rules (m5) and (m6) does not

1141: interfere with the process of rewriting.

1142: 

1143: \begin{lemma}\label{lem:prune-back} 

1144: Let $A$ be the environment $\menv{e_1, nl_1, ol_1, \menv{e_2, nl_2,

1145: ol_3, e_3}}$ where $e_3$ is a simple environment and $e_2$ is of

1146: the form $(t_2,n_2) :: e'_2$. Further, for any positive number $i$ such

1147: that $i \leq nl_2 - n_2$ and $i \leq ol_3$, let $B$ be the environment

1148: \begin{tabbing}

1149: \qquad\=\kill

1150: \>$\menv{e_1, nl_1, ol_1, \menv{e_2, nl_2 - i, ol_3 - i,

1151:     e_3\{i\}}}$.

1152: \end{tabbing}

1153: If $A \readmerge C$ for any simple environment $C$ then also $B

1154: \readmerge C$.

1155: \end{lemma}

1156: 

1157: \begin{proof} It suffices to verify the claim when $i = 1$; an easy

1158:   induction on $i$ then extends the result to the cases where $i >

1159:   1$. For the case of $i = 1$, the argument is by induction on the

1160:   length of the reduction sequence from $A$ to $C$ with the

1161:   essential part being a consideration of the first 

1162:   rule used. The details are straightforward and hence

1163:   omitted. 

1164: \end{proof}

1165: 

1166: 

1167: \begin{lemma}\label{lem:unfold-back} 

1168: Let $A$ be the environment $\menv{e_1, nl_1, ol_1, \menv{e_2, nl_2,

1169: ol_3, e_3}}$ where $e_2$ and $e_3$ are environments of the form

1170: $(t_2,nl_2) :: e'_2$ and $(t_3,n_3) :: e'_3$, respectively. Further,

1171: let $B$ be the environment 

1172: \begin{tabbing}

1173: \qquad\=\kill

1174: \>$\menv{e_1, nl_1, ol_1, (\env{t_2,ol_3,n_3,e_3}, n_3 +

1175:   (\monus{nl_2}{ol_3}))::\menv{e'_2,nl_2, ol_3, e_3}}$.

1176: \end{tabbing}

1177: If $A \readmerge C$ for any simple environment $C$ then also $B

1178: \readmerge C$.

1179: \end{lemma}

1180: 

1181: \begin{proof}

1182: The proof is again by induction on the length of the reduction

1183: sequence from $A$ to $C$. The first rule in this sequence either

1184: produces $B$, in which case the lemma follows immediately, or it can

1185: be used on $B$ (perhaps at more than one place) to produce a form that

1186: is amenable to the application of the induction hypothesis. 

1187: \end{proof}

1188: 

1189: In evaluating the composition of $e_2$ and $e_3$, it may be the case

1190: that some part of $e_3$ is inconsequential. The last observation that

1191: we need is that this part can be ``pruned'' immediately in calculating

1192: the composition of the combination of $e_1$ and $e_2$ with $e_3$. The

1193: following lemma is consequential in establishing this fact. 

1194: 

1195: \begin{lemma}\label{lem:remvac}

1196: Let $A$ be the environment $\menv{e_1,nl_1,ol_2,e_2}$ where

1197: $e_2$ is a simple environment.

1198: \begin{enumerate}

1199: \item If $ol_2 \leq nl_1 - {\it lev}(e_1)$ then $A$ reduces to any

1200:   simple environment that $e_1$ reduces to.

1201: \item For any positive number $i$ such that $i \leq nl_1 - {\it

1202:   lev}(e_1)$ and $i \leq ol_2$, $A$ reduces to any simple environment

1203:   that $\menv{e_1,nl_1 - i, ol_2 - i, e_2\{i\}}$ reduces to.

1204: \end{enumerate}

1205: \end{lemma}

1206: 

1207: \begin{proof} Let $e_1$ be reducible to the simple environment

1208:   $e'_1$. Then we may transform $A$ to the form

1209:   $\menv{e'_1,nl_1,ol_2,e_2}$. Recalling that the level of an

1210:   environment is never increased by rewriting, we have that ${\it

1211:   lev}(e'_1) \leq {\it lev}(e_1)$. From this it follows that

1212:   $A$ can be rewritten to $e'_1$ using rules (m5) and (m2) if $ol_2

1213:   \leq nl_1 - {\it lev}(e_1)$. This establishes the first part of the

1214:   lemma.  

1215: 

1216: The second part is nontrivial only if $nl_1 - {\it lev}(e_1)$ and

1217:   $ol_2$ are both nonzero. Suppose this to be the case and let $B$ be

1218:   $\menv{e_1,nl_1-1,ol_2-1,e_2\{1\}}$. The desired result follows by

1219:   an induction on $i$ if we can show that $A$ can be rewritten to any

1220:   simple environment that $B$ reduces to. We do this by an induction

1221:   on the length of the reduction sequence from $B$ to the simple

1222:   environment. This sequence must evidently be of length at least

1223:   one. If a proper subpart of $B$ is rewritten by the first rule in

1224:   this sequence, then the same rule can be applied to $A$ as well and

1225:   the induction hypothesis easily yields the desired conclusion. If

1226:   $B$ is rewritten by one of the rules (m3)-(m6), then it must be the

1227:   case that $A \onereadmerge B$ via either rule (m4) or (m5) from

1228:   which the claim follows immediately. Finally, if $B$ is

1229:   rewritten using rule (m2), then $ol_2 \leq nl_1 - {\it

1230:   lev}(e_1)$. The second part of the lemma is now a consequence of the

1231:   first part.

1232: \end{proof}

1233: 

1234: We now prove the associativity property for environment

1235: composition: 

1236: 

1237: \begin{lemma}

1238: \label{lem:assoc}

1239: Let $A$ and $B$ be environments of the form

1240: \begin{tabbing}

1241: \qquad\=\kill

1242: \>$\menv{\menv{e_1, nl_1, ol_2, e_2}, nl_2 + (\monus{nl_1}{ol_2}),

1243:   ol_3, e_3} $

1244: \end{tabbing}

1245: and

1246: \begin{tabbing}

1247: \qquad\=\kill

1248: \>$\menv{e_1, nl_1, ol_2 + (\monus{ol_3}{nl_2}), \menv{e_2, nl_2,

1249:     ol_3, e_3}}$,

1250: \end{tabbing}

1251: respectively. Then there is a simple environment $C$ such that $A

1252: \readmerge C$ and $B \readmerge C$.

1253: \end{lemma}

1254: 

1255: \begin{proof}

1256: We assume that $e_1$, $e_2$ and $e_3$ are simple environments; if this

1257: is not the case at the outset, then we may rewrite them to such

1258: a form in both $A$ and $B$ before commencing the proof we provide. Our

1259: argument is now based on an induction on the structure of $e_3$ with

1260: possibly further inductions on the structures of $e_2$ and $e_1$. 

1261: 

1262: \medskip

1263: 

1264: \noindent {\it Base case for first induction.} When $e_3$ is {\it

1265:   nil}, the lemma is seen to be true by observing that both $A$ and

1266:   $B$ rewrite to $\menv{e_1,nl_1,ol_2,e_2}$ by virtue of rule (m2). 

1267: 

1268: \medskip

1269: 

1270: \noindent {\it Inductive step for first induction.} Let $e_3 =

1271: (t_3,n_3) :: e'_3$. We now proceed by an induction on the structure

1272: of $e_2$. 

1273: 

1274: \smallskip

1275: 

1276: \noindent {\it Base case for second induction.} When $e_2$ is {\it

1277:   nil}, it can be seen that, by virtue of rules (m2), (m3) and either

1278:   (m4) or (m5), $A$ and $B$ reduce to $\menv{e_1,nl_1,ol_3   - nl_2,

1279:   e_3\{nl_2\}}$ when $ol_3 > nl_2$ and to $e_1$ otherwise. The

1280:   truth of the lemma follows immediately from this.

1281: 

1282: \smallskip

1283: 

1284: \noindent {\it Inductive step for second induction.} Let $e_2 = (t_2,n_2) ::

1285: e'_2$. We consider first the situation where $nl_1 >

1286: lev(e_1)$. Suppose further that $ol_3 \leq (nl_2 - n_2)$. Using rules

1287: (m5) and (m2), we see then that 

1288: \begin{tabbing}

1289: \qquad\=\kill

1290: \>$B \readmerge \menv{e_1,nl_1,ol_2,e_2}$.

1291: \end{tabbing}

1292: We also note that $ol_3 \leq (nl_2 + (\monus{nl_1}{ol_2})) -

1293: lev(\menv{e_1,nl_1,ol_2,e_2})$ in this case. \autoref{lem:remvac}

1294: assures us now that $A$ can be rewritten to any simple

1295: environment that $\menv{e_1,nl_1,ol_2,e_2}$ reduces to and thereby

1296: verifies the lemma in this case.

1297: 

1298: It is possible, of course, that $ol_3 > (nl_2 - n_2)$. Here we see

1299: that   

1300: \begin{tabbing}

1301: \qquad\=\kill

1302: \>$B \readmerge \menv{e_1,nl_1 - 1, ol_2 + (\monus{ol_3}{nl_2}) - 1,

1303:   \menv{e'_2,n_2,ol_3 - (nl_2 - n_2),e_3\{nl_2 - n_2\}}}$.

1304: \end{tabbing}

1305: using rules (m5) and (m6). Using rule (m5), we also have that

1306: \begin{tabbing}

1307: \qquad\=\kill

1308: \>$A \readmerge \menv{\menv{e_1,nl_1 - 1, ol_2 - 1, e'_2},nl_2 +

1309:   (\monus{nl_1}{ol_2}),ol_3,e_3}$.

1310: \end{tabbing}

1311: Invoking the induction hypothesis, it follows that $A$ and 

1312: \begin{tabbing}

1313: \qquad\=\kill

1314: \>$\menv{e_1,nl_1 - 1, ol_2 + (\monus{ol_3}{nl_2}) -

1315:   1,\menv{e'_2,nl_2,ol_3,e_3}}$ 

1316: \end{tabbing}

1317: reduce to a common simple environment. By \autoref{lem:prune-back}

1318: it follows that $B$ must also reduce to this environment.

1319: 

1320: The only remaining situation to consider, then, is that when $nl_1 = 

1321: lev(e_1)$. For this case we need the last induction, that on the

1322: structure of $e_1$.

1323: 

1324: \smallskip

1325: 

1326: \noindent {\it Base case for final induction.} If $e_1$ is {\it nil},

1327:   then $nl_1$ must be $0$. It follows easily that both $A$ and $B$

1328:   reduce to $\menv{e_2,nl_2,ol_3,e_3}$ and that the lemma must

1329:   therefore be true.

1330: 

1331: \smallskip

1332: 

1333: \noindent {\it Inductive step for final induction.} Here $e_1$ must be of the

1334: form $(t_1,nl_1) :: e'_1$. We dispense first with the

1335: situation where $n_2 < nl_2$. In this case, by rule (m5)

1336: \begin{tabbing}

1337: \qquad\=\kill

1338: \>$B \readmerge

1339: \menv{e_1,nl_1,ol_2+(\monus{ol_3}{nl_2}),\menv{e_2,nl_2 - 1, ol_3 - 1,

1340:     e'_3}}$.

1341: \end{tabbing}

1342: By the induction hypothesis used relative to $e'_3$, $B$ and the

1343: expression 

1344: \begin{tabbing}

1345: \qquad\=\kill

1346: \>$\menv{\menv{e_1,nl_1,ol_2,e_2},nl_2 + (\monus{nl_1}{ol_2}) - 1,ol_3

1347:   - 1, e'_3}$

1348: \end{tabbing}

1349: must reduce to a common simple environment. By \autoref{lem:remvac},

1350: $A$ must also reduce to this environment. 

1351: 

1352: Thus, it only remains for us to consider the situation in which $n_2 =

1353: nl_2$. In this case by using rule (m1) twice we may transform $A$ to

1354: the expression $A_h :: A_t$ where 

1355: \begin{tabbing}

1356: \qquad\=\kill

1357: \>$A_h = (\env{\env{t_1,ol_2,n_2,e_2},ol_3,n_3,e_3}, n_3 + (\monus{(nl_2 +

1358:   (\monus{nl_1}{ol_2}))}{ol_3}))$

1359: \end{tabbing}

1360: and

1361: \begin{tabbing}

1362: \qquad\=\kill

1363: \>$A_t = \menv{\menv{e_1', nl_1, ol_2, e_2}, nl_2 +

1364:   (\monus{nl_1}{ol_2}), ol_3, e_3}$.

1365: \end{tabbing}

1366: Similarly, $B$ may be rewritten to the expression $B_h :: B_t$ where  

1367: \begin{tabbing}

1368: \qquad\=$B_h = $\=$($\=\qquad\qquad\=\kill

1369: \>$B_h =$\>$($\>$\lenv t_1, ol_2 + (\monus{ol_3}{nl_2}), n_3 +

1370: (\monus{nl_2}{ol_3}),$ \\

1371: \>\>\>\>$(\env{t_2, ol_3, n_3, e_3}, n_3 +

1372:   (\monus{nl_2}{ol_3}))::\menv{e_2',nl_2,ol_3,e_3} \renv,$\\

1373: \>\>\>$n_3 + (\monus{nl_2}{ol_3}) + (\monus{nl_1}{(ol_2 +

1374:   (\monus{ol_3}{nl_2}))}))$

1375: \end{tabbing}

1376: and

1377: \begin{tabbing}

1378: \qquad\=\kill

1379: \> $B_t = \menv{e_1', nl_1, ol_2 + (\monus{ol_3}{nl_2}),

1380:   (\env{t_2,ol_3,n_3,e_3}, n_3 + (\monus{nl_2}{ol_3}))::\menv{e_2',

1381:     nl_2, ol_3, e_3}}$.

1382: \end{tabbing}

1383: Now, using straightforward arithmetic identities, it can be seen that

1384: the ``index'' components of $A_h$ and $B_h$ are equal. Further, the

1385: term component of $A_h$ can be rewritten to a form identical to the

1386: term component of $B_h$ by using the rules (m1) and (m6). Finally, by

1387: virtue of the induction hypothesis, it follows that $A_t$ and the

1388: expression 

1389: \begin{tabbing}

1390: \qquad\=\kill

1391: \>$\menv{e_1', nl_1, ol_2 +

1392: (\monus{ol_3}{nl_2}), \menv{e_2, nl_2, ol_3, e_3}}$

1393: \end{tabbing}

1394: reduce to a common simple environment. \autoref{lem:unfold-back}

1395: allows us to conclude that $B_t$ can also be rewritten to this

1396: expression. Putting all these observations together it is seen that

1397: $A$ and $B$ can be reduced to a common simple environment in this case

1398: as well.

1399: \end{proof}

1400: 

1401: \subsection{Proof of Confluence for Reading and Merging Rules}

1402: 

1403: We are now in a position to prove the confluence of the reading and

1404: merging rules, using the ideas outlined in the beginning of this

1405: section.

1406: 

1407: \begin{lemma}

1408: \label{lem:rm-weak-confluence}

1409: The relation $\onereadmerge$ is weakly confluent.

1410: \end{lemma}

1411: \begin{proof}

1412: We recall the method of proof from \cite{huet-80-confluent}. An

1413: expression $t$ constitutes a nontrivial overlap of the rules $R_1$ and

1414: $R_2$ at a subexpression $s$ if (a)~$t$ is an instance of the lefthand

1415: side of $R_1$, (b)~$s$ is an instance of the lefthand side of $R_2$

1416: and also does not occur within the instantiation of a variable on the

1417: lefthand side of $R_1$ when this is matched with $t$ and (c)~either

1418: $s$ is distinct from $t$ or $R_1$ is distinct from $R_2$. Let $r_1$ be

1419: the expression that results from rewriting $t$ using $R_1$ and let

1420: $r_2$ result from $t$ by rewriting $s$ using $R_2$. Then the pair

1421: $\langle r_1, r_2 \rangle$ is called the conflict pair corresponding

1422: to the overlap in question. Relative to these notions, the theorem can

1423: be proved by establishing the following simpler property: for every

1424: conflict pair corresponding to the reading and merging rules, it is

1425: the case that the two terms can be rewritten to a common form using

1426: these rules.

1427: 

1428: In completing this line of argument, the nontrivial overlaps that we

1429: have to consider are those between (m1) and each of the rules

1430: (r1)-(r6), between (m1) and itself and between (m2) and (m3).  The

1431: last of these cases is easily dealt with: the two expressions

1432: constituting the conflict pair are identical, both being $nil$. The

1433: overlap between (m1) and itself occurs over a term of the form

1434: $\env{\env{\env{t,ol_1,nl_1,e_1},ol_2,nl_2,e_2},ol_3,nl_3,e_3}$. By

1435: using rule (m1) once more on each of the terms in the conflict pair,

1436: these can be rewritten to expressions of the form $\env{t,ol',nl',e'}$

1437: and $\env{t,ol'',nl'',e''}$, respectively, whence we can see that $ol'

1438: = ol''$ and $nl'=nl''$ by simple arithmetic reasoning and that $e'$

1439: and $e''$ reduce to a common form using \autoref{lem:assoc}. The

1440: overlaps between (m1) and the reading rules are also easily dealt

1441: with. For instance, consider the case of (m1) and (r2) where we

1442: have \[ \env{\env{\#i,0,nl_1,nil},ol_2,nl_2,e_2} \] Rewriting with

1443: (r2) first produces \[ \env{\#(i+nl_1),ol_2,nl_2,e_2} \] while

1444: rewriting with (m1) first yields \[ \env{\#i, \monus{ol_2}{nl_1},

1445:   nl_2+(\monus{nl_1}{ol_2}), \menv{nil,nl_1,ol_2,e_2}}. \] For both

1446: expressions we can rewrite $e_2$ to a simple environment $e_2'$ using

1447: \autoref{lem:eval-simple}. Now if $ol_2 \geq nl_1$ then both terms

1448: can be reconciled to \[ \env{\#i,ol_2 - nl_1, nl_2, e_2'\{nl_1\}} \]

1449: In the case of $ol_2 < nl_1$, both terms rewrite to

1450: $\#(i+nl_1-ol_2)$. Thus the conflict pair is resolved.  The other

1451: cases of overlaps between (m1) and the reading rules are similar and

1452: require roughly the same reasoning.

1453: \end{proof}

1454: 

1455: As observed already, the main result of this section follows directly

1456: from \autoref{lem:rm-weak-confluence} and \autoref{thm:rm-termination}.

1457: 

1458: \begin{theorem}

1459: \label{th:rm-confluence}

1460: The relation $\onereadmerge$ is confluent.

1461: \end{theorem}

1462: 

1463: The uniqueness of $\onereadmerge$-normal forms is an immediate

1464: consequence of \autoref{th:rm-confluence}. In the sequel, a notation

1465: for referring to such forms will be useful.

1466: 

1467: \begin{defn}[Reading and merging normal form]

1468: The notation $|t|$ denotes the $\onereadmerge$-normal form of a

1469: suspension expression $t$.

1470: \end{defn}

1471: 

1472: It is easily seen that the $\onereadmerge$-normal form for a term 

1473: that does not contain meta variables is a a term that is devoid of

1474: suspensions, \ie, a de Bruijn term. A further observation is that if

1475: the all the environments appearing in the original term are simple,

1476: then just the reading rules suffice in reducing it to the de Bruijn

1477: term that is its unique $\onereadmerge$-normal form.

1478: 

1479: \section{Simulation of Beta Reduction}

1480: \label{sec:simulation}

1481: 

1482: A fundamental property of all explicit substitution calculi is

1483: that they properly simulate the lambda calculus. In particular,

1484: we must ensure that our $\beta_s$ rule corresponds to the $\beta$

1485: rule of the lambda calculus, modulo the reading and merging

1486: rules. The following two theorems establish this result. The first

1487: shows that a $\beta_s$ rewrite on suspension terms corresponds to

1488: some number of $\beta$ rewrites in the lambda calculus. One

1489: might think of this theorem as proving the soundness of our

1490: calculus. The second theorem shows that any $\beta$ rewrite can be

1491: simulated using the rules of our calculus.  One might think of

1492: this theorem as proving the completeness of our calculus.

1493: 

1494: \begin{theorem}

1495: If $x_1$ and $x_2$ are suspension expressions such that $x_1

1496: \onebetas x_2$ then $\rnf{x_1} \mbeta \rnf{x_2}$.

1497: \end{theorem}

1498: \begin{proof}

1499: This result is proven for the original suspension calculus in

1500: \cite{nadathur-98-suspension}. We know from \autoref{thm:same-nf} that

1501: $\onereadmerge$-normal forms of $x_1$ and $x_2$ are the same as in the

1502: original suspension calculus, thus we can carry over the previous

1503: result.

1504: \end{proof}

1505: 

1506: \begin{theorem}

1507: If $x_1$ and $x_2$ are suspension expressions in

1508: $\onereadmerge$-normal form such that $x_1 \onebeta x_2$ then $x_1

1509: \all x_2$.

1510: \end{theorem}

1511: \begin{proof}

1512: A stronger version of this property, where the result is replaced with

1513: $x_1 \readbetas x_2$, is proved as Lemma 8.2 of the original

1514: suspension paper. Since the $\beta_s$ and the reading rules are

1515: essentially the same for the two calculi, the result carries over.

1516: \end{proof}

1517: 

1518: \section{Confluence of Overall Calculus}

1519: \label{sec:confluence-all}

1520: 

1521: In this section we prove that the full suspension calculus is

1522: confluent even in the presence of graftable meta variables.  One

1523: important distinction between the proof of this property and the proof

1524: of confluence for the reading and merging rules is that the latter is

1525: proven in spite of the merging rules while the former will be proven

1526: only because of the merging rules (see \autoref{sec:susp-metavars}

1527: for a discussion of why the merging rules are required). Thus this

1528: property speaks to the well designed nature of the merging

1529: rules. Moreover, this property makes the suspension calculus a

1530: candidate for unification procedures designed specifically for

1531: graftable meta variables \cite{dowek-95-higherorder} because with this

1532: confluence property we are guaranteed that $\oneall$-normal forms are

1533: unique even with graftable meta variables.

1534: 

1535: For most explicit substitution calculi, confluence of the full

1536: calculus is proven using Hardin's Interpretation Method

1537: \cite{hardin-89-confluence}.  The interpretation method starts with

1538: the lambda calculus which is already confluent and it uses the

1539: confluence and strong termination of the substitution rules (in our

1540: case, the reading and merging rules) to close a confluence diagram for

1541: the overall calculus. This method is inadequate, however, when we

1542: allow for graftable meta variables. The problem is that the lambda

1543: calculus with graftable meta variables does not make sense and is not

1544: confluent. Instead, we follow the method presented in

1545: \cite{curien-96-confluence} which is based the on the following key

1546: lemma.

1547: \begin{lemma}

1548: \label{lem:RSR}

1549: Let $\mathcal{R}$ and $\mathcal{S}$ be two

1550: relations defined on the same set $X$, $\mathcal{R}$ being

1551: confluent and strongly normalizing, and $\mathcal{S}$ being

1552: strongly confluent, i.e. such that the following diagrams hold for

1553: any $f,g,h\in X$:

1554: \begin{center}

1555: \begin{minipage}{5cm}

1556: \centerline{

1557: \xymatrix{

1558: f \ar@{->}[dd]_{\mathcal{S}} \ar@{->}[rr]^{\mathcal{S}} &&

1559: g \ar@{-->}[dd]^{\mathcal{S}} \\

1560: \\

1561: h \ar@{-->}[rr]^{\mathcal{S}} && k \\

1562: }}

1563: \end{minipage}

1564: \hspace{1in}

1565: \begin{minipage}{5cm}

1566: \centerline{

1567: \xymatrix{

1568: f \ar@{->}[dd]_{\mathcal{R}} \ar@{->}[rr]^{\mathcal{S}} &&

1569: g \ar@{-->}[dd]^{\mathcal{R}^*} \\

1570: \\

1571: h \ar@{-->}[rr]^{\mathcal{R^*SR^*}} && k \\

1572: }}

1573: \end{minipage}

1574: \end{center}

1575: Then the relation $\mathcal{R}^*\mathcal{S}\mathcal{R}^*$ is

1576: confluent.

1577: \end{lemma}

1578: 

1579: We will apply the lemma using the reading and merging rules as

1580: $\mathcal{R}$ and parallel $\beta_s$-reduction as $\mathcal{S}$.

1581: 

1582: \begin{defn}[Parallel $\beta_s$-reduction]

1583: Parallel $\beta_s$-reduction is defined by the rules in

1584: \autoref{fig:parallel} and is denoted by $\one{\beta_s||}$.

1585: \end{defn}

1586: 

1587: \begin{figure}[t]

1588: \begin{align*}

1589: &\infer{t \to t}{}

1590: &

1591: &\infer{e \to e}{} \\

1592: \\

1593: &\infer{t_1\app t_2 \to t_1'\app t_2'}{t_1 \to t_1' && t_2 \to t_2'}

1594: &

1595: &\infer{(t,l) :: e \to (t',l) :: e'}{t \to t' && e \to e'} \\

1596: \\

1597: &\infer{\lambdadb t \to \lambdadb t'}{t \to t'}

1598: &

1599: &\infer{\menv{e_1,nl_1,ol_2,e_2} \to \menv{e_1',nl_1,ol_2,e_2'}}{

1600:   e_1 \to e_1' && e_2 \to e_2'} \\

1601: \\

1602: &\infer{\env{t,ol,nl,e} \to \env{t',ol,nl,e'}}{t \to t' && e \to e'}

1603: &

1604: &\infer{(t,n) \to (t',n)}{t \to t'} \\

1605: \\

1606: &\infer{(\lambdadb t_1)\app t_2 \to \env{t_1', 1, 0, (t_2',0)::nil}}{

1607:   t_1 \to t_1' && t_2 \to t_2'}

1608: \end{align*}

1609: \caption{Parallel $\beta_s$-reduction}

1610: \label{fig:parallel}

1611: \end{figure}

1612: 

1613: \begin{lemma}

1614: $\onereadmerge$ and $\one{\beta_s||}$ satisfy the condition of

1615: \autoref{lem:RSR}.

1616: \end{lemma}

1617: \begin{proof}

1618: $\one{\beta_s||}$ is obviously strongly confluent since $\onebetas$ is

1619: is a left linear system with no critical pairs. This proves that the

1620: first diagram in \autoref{lem:RSR} holds.

1621: 

1622: For the second diagram, the interesting case is the critical pair

1623: for $f = \env{(\lambdadb t_1)\app t_2, ol, nl, e}$. In this case, we

1624: have $g = \env{\env{t_1', 1, 0, (t_2',0)::nil}, ol, nl, e'}$ and $h =

1625: \env{\lambdadb t_1, ol, nl, e}\app \env{t_2, ol, nl, e}$, where $t_1

1626: \one{\beta_s||} t_1'$, $t_2 \one{\beta_s||} t_2'$, and $e

1627: \one{\beta_s||} e'$. We must find a $k$ such that $g \readmerge k$ and

1628: $h \readmerge h' \one{\beta_s||} h'' \readmerge k$. This is

1629: straightforward since

1630: \begin{align*}

1631: g &= \env{\env{t_1', 1, 0, (t_2',0)::nil}, ol, nl, e'} \\

1632: &\onemerge \env{t_1', ol+1, nl, \menv{(t_2',0)::nil, 0, ol, e'}} \\

1633: &\readmerge \env{t_1', ol+1, nl, (\env{t_2', ol, nl, e'}, nl)::e'}

1634: \end{align*}

1635: and

1636: \begin{align*}

1637: h &= \env{\lambdadb t_1, ol, nl, e}\app \env{t_2, ol, nl, e} \\

1638: &\oneread \lambdadb \env{t_1, ol+1, nl+1, (\#1,nl+1)::e}\app \env{t_2,

1639:   ol, nl, e} \\

1640: &\one{\beta_s||} \env{\env{t_1', ol+1, nl+1, (\#1,nl+1)::e'}, 1, 0,

1641:   (\env{t_2', ol, nl, e'}, 0)::nil} \\

1642: &\onemerge \env{t_1', ol+1, nl, \menv{(\#1,nl+1)::e', nl+1, 1,

1643:     (\env{t_2', ol, nl, e'}, 0)::nil}} \\

1644: &\readmerge \env{t_1', ol+1, nl, (\env{t_2', ol, nl, e'}, nl)::e'}

1645: \end{align*}

1646: \end{proof}

1647: 

1648: \begin{theorem}

1649: \label{thm:full-confluence}

1650: The relation $\oneall$ is confluent.

1651: \end{theorem}

1652: \begin{proof}

1653: Note that $\oneall \subseteq \mathcal{R}^*\mathcal{S}\mathcal{R}^*

1654: \subseteq \all$.

1655: \end{proof}

1656: 

1657: \section{Similarity in the Suspension Calculus}

1658: \label{sec:similarity}

1659: 

1660: The purpose of this section is to introduce a notion of similarity in

1661: the suspension calculus which relates suspension expressions that

1662: differ only in the renumbering and indices of environment terms. This

1663: allows us to formally capture the notion that two environments are

1664: similar enough that they act the same during rewriting which will be

1665: useful when we translate from another explicit substitution calculus

1666: into the suspension calculus (\autoref{sec:lambdasigma-to-susp}). The

1667: notion of similarity stems from the fact that there are two ways to

1668: represent the renumbering to be done on an environment term. One is

1669: using the difference between the new embedding level of the suspension

1670: and the embedding level of the environment term. The other is with an

1671: explicit renumbering substitution applied to the term in the

1672: environment term. This section proves that these two notions are

1673: equivalent for the purpose of finding normal forms.

1674: 

1675: \begin{defn}

1676: \label{def:similar}

1677: The similarity relation $\sim$ is defined in \autoref{fig:similar}.

1678: \begin{figure}[t]

1679: \begin{align*}

1680: &\infer{t \sim t}{}

1681: &

1682: &\infer{e \sim e}{} \\

1683: \\

1684: &\infer{t_1\app t_2 \sim t_1'\app t_2'}{t_1 \sim t_1' && t_2 \sim t_2'}

1685: &

1686: &\infer{(t,n)::e \sim (t',n)::e'}{t \sim t' && e \sim e'} \\

1687: \\

1688: &\infer{\lambdadb t \sim \lambdadb t'}{t \sim t'}

1689: &

1690: &\infer{\menv{e_1,nl_1,ol_2,e_2} \sim \menv{e_1',nl_1,ol_2,e_2'}}{

1691:   e_1 \sim e_1' && e_2 \sim e_2'} \\

1692: \\

1693: &\infer{\env{t,ol,nl,e} \sim \env{t',ol,nl,e'}}{t \sim t' && e \sim e'}

1694: &

1695: &\infer{(t,n) \sim (t',n)}{t \sim t'}

1696: \end{align*}

1697: \begin{align*}

1698: \infer{(\env{t,ol,nl,r}, nl + k)::e \sim (\env{t',ol,nl',r'}, nl'

1699:   + k)::e'}{t \sim t' && r \sim r' && e \sim e'}

1700: \end{align*}

1701: \caption{The similarity relation, $\sim$}

1702: \label{fig:similar}

1703: \end{figure}

1704: \end{defn}

1705: 

1706: The main result of this section is to prove that similar terms rewrite

1707: to the same normal form. This first requires proving the following

1708: lemma.

1709: 

1710: \begin{lemma}

1711: \label{lem:backwards-m5}

1712: Let $\menv{e_1,nl_1,ol_2,e_2} \readmerge e$ where $e$ is a simple

1713: environment.

1714: \begin{itemize}

1715: \item If $nl_1 - lev(e_1) \geq k$ and $ol_2 \geq k$, then

1716: $\menv{e_1,nl_1-k,ol_2-k,e_2\{k\}} \readmerge e$.

1717: \item If $nl_1 - lev(e_1) \geq ol_2$, then $e_1 \readmerge e$.

1718: \end{itemize}

1719: \end{lemma}

1720: \begin{proof}

1721: The proof is by induction on the length of the sequence

1722: $\menv{e_1,nl_1,ol_2,e_2} \readmerge e$.

1723: \end{proof}

1724: 

1725: \begin{theorem}

1726: If $t \sim t'$ for terms $t$ and $t'$ then they rewrite by reading and

1727: merging rules to the same de Bruijn term. If $e \sim e'$ for

1728: environments $e$ and $e'$ then they rewrite by reading and merging

1729: rules to similar simple environments.

1730: \end{theorem}

1731: \begin{proof}

1732: We prove the general case of $exp \sim exp'$ for suspension

1733: expressions $exp$ and $exp'$. We do this by induction using the

1734: relation $\gg$ defined in \autoref{def:exprorder}. Note that this

1735: relation decreases when an expression is rewritten using the reading

1736: and merging rules and also a subpart is always smaller than the

1737: original expression.

1738: 

1739: Because we are inducting using $\gg$, we can assume that the result

1740: already holds for any similar subparts of $exp$ and $exp'$. Then we can

1741: rewrite these similar subparts to be equal in the case of terms or

1742: simple environments in the case of environments. This decreases the

1743: measure of the overall terms $exp$ and $exp'$ and thus the inductive

1744: hypothesis then applies to them. By this reasoning, we can assume that

1745: whenever two subparts of $exp$ and $exp'$ are similar they are in fact

1746: equal in the case of terms and simple in the case of environments. We

1747: will also use the convention that $x$ and $x'$ are always similar.

1748: 

1749: Let us consider cases based on the structure of $exp$ and $exp'$,

1750: first looking at the case when both are terms. If they are both

1751: constants or de Bruijn indices then the result is trivial. If $exp =

1752: (t_1\app t_2)$ then $exp' = (t_1'\app t_2')$ and $t_1 = t_1'$ and $t_2

1753: = t_2'$ so the result follows trivially. A similar result holds in the

1754: case where $exp$ and $exp'$ are lambda abstractions.

1755: 

1756: The first nontrivial case is when $exp$ and $exp'$ are both

1757: suspensions, say $exp = \env{t,ol,nl,e}$ and $exp' =

1758: \env{t,ol,nl,e'}$. Now consider which rewrite rules apply to the

1759: toplevel of these terms, keeping in mind that $t$ is in normal

1760: form. If $t$ is an application or an abstraction then (r5) or (r6)

1761: applies and the result follows from the inductive hypothesis. If $t$

1762: is a de Bruijn term and (r2) or (r4) applies then the result again

1763: follows from the inductive hypothesis. If (r3) applies and $e$ and

1764: $e'$ have the same head then the result is trivial. The key case is

1765: when (r3) applies and $e$ and $e'$ have different heads, in which case

1766: we have,

1767: \begin{align*}

1768: exp

1769: &= \env{\#1,ol,nl,(\env{t_r,ol_r,nl_r,r}, nl_r + k)::e_1}\\

1770: &\one{(r3)} \env{\env{t_r,ol_r,nl_r,r}, 0, nl - (nl_r + k), nil}\\

1771: &\one{(m1)} \env{t_r, ol_r, nl - (nl_r + k) + nl_r, \menv{r, nl_r, 0,

1772:     nil}}\\

1773: &\one{(m2)} \env{t_r, ol_r, nl - k, r}\\

1774: \\

1775: exp'

1776: &= \env{\#1,ol,nl,(\env{t_r,ol_r,nl_r',r'}, nl_r' +

1777:   k)::e_1'}\\

1778: &\one{(r3)} \env{\env{t_r,ol_r,nl_r',r'}, 0, nl - (nl_r' + k), nil}\\

1779: &\one{(m1)} \env{t_r, ol_r, nl - (nl_r' + k) + nl_r', \menv{r', nl_r',

1780:     0, nil}}\\

1781: &\one{(m2)} \env{t_r, ol_r, nl - k, r'}

1782: \end{align*}

1783: The two resulting suspensions are similar and smaller than their

1784: original terms, thus the inductive hypothesis finishes this case.

1785: 

1786: The other half of the proof is to show that when $exp$ and $exp'$ are

1787: similar environments then they rewrite to similar simple

1788: environments. The cases when $exp$ and $exp'$ are either $nil$ or a

1789: cons follow trivially from the inductive hypothesis. The important

1790: case is when $exp = \menv{e_1,nl_1,ol_2,e_2}$ and $exp' =

1791: \menv{e_1',nl_1,ol_2,e_2'}$. Consider the cases for which rewrites can

1792: apply to the toplevel of both expressions. If (m2), (m3), or (m4)

1793: applies to the first expression then the same rewrite applies to the

1794: second environment and the result follows easily. The case when (m5)

1795: applies to both is also direct using the inductive hypothesis. The two

1796: remaining cases are the most interesting: when (m6) applies to both,

1797: and when (m5) applies to one and (m6) to the other.

1798: 

1799: Consider when (m6) applies to both expressions. Here the head terms of

1800: $e_1$ and $e_1'$ must be the same. If the head terms of $e_2$ and

1801: $e_2'$ are also the same then the result is trivial. Otherwise we

1802: have,

1803: \begin{align*}

1804: exp

1805: &= \menv{(t_1,nl_1)::e_3,nl_1,ol_2,(\env{t_r,ol_r,nl_r,r},

1806:   nl_r+k)::e_4}\\

1807: &\one{(m6)} (\env{t_1,ol_2,nl_r+k,(\env{t_r,ol_r,nl_r,r},

1808:   nl_r+k)::e_4}, nl_r+k+(\monus{nl_1}{ol_2}))\\

1809: &\hspace{1in}::\menv{e_3,nl_1,ol_2,(\env{t_r,ol_r,nl_r,r}, nl_r+k)::e_4}\\

1810: \\

1811: exp'

1812: &= \menv{(t_1,nl_1)::e_3',nl_1,ol_2,(\env{t_r',ol_r,nl_r',r'},

1813:   nl_r'+k)::e_4'}\\

1814: &\one{(m6)} (\env{t_1,ol_2,nl_r'+k,(\env{t_r',ol_r,nl_r',r'},

1815:   nl_r'+k)::e_4'}, nl_r'+k+(\monus{nl_1}{ol_2}))\\

1816: &\hspace{1in}::\menv{e_3',nl_1,ol_2,(\env{t_r,ol_r,nl_r',r'},

1817:   nl_r'+k)::e_4'}\\

1818: \end{align*}

1819: These two environments are still similar and the inductive hypothesis

1820: now applies.

1821: 

1822: The final case is when (m5) applies to one expression and (m6) to the

1823: other. Without loss of generality, assume that (m6) applies to $exp$

1824: and (m5) to $exp'$. There are two subcases based on whether the heads

1825: of $e_2$ and $e_2'$ are the same or not. Here we will only consider

1826: hardest case where the heads differ. The other case is a

1827: simplification of the following argument,

1828: \begin{align*}

1829: exp

1830: &= \menv{(\env{t_s,ol_s,nl_s,s},nl_s+k_s)::e_3,nl_1,ol_2,

1831:          (\env{t_r,ol_r,nl_r,r},nl_r+k_r)::e_4}\\

1832: &\one{(m6)} (\env{\env{t_s,ol_s,nl_s,s}, ol_2, nl_r+k_r,e_2},

1833:          nl_r+k_r+(\monus{nl_1}{ol_2})) :: \menv{e_3,nl_1,ol_2,e_2}\\

1834: &\one{(m1)} (\env{t_s,ol_s+(\monus{ol_2}{nl_s}),

1835:          nl_r+k_r+(\monus{nl_s}{ol_2}), \menv{s,nl_s,ol_2,e_2}},\\

1836: &\hspace{1in} nl_r+k_r+(\monus{nl_1}{ol_2})) ::

1837:                   \menv{e_3,nl_1,ol_2,e_2}\\

1838: \\

1839: exp'

1840: &= \menv{(\env{t_s',ol_s,nl_s',s'},nl_s'+k_s)::e_3',nl_1,ol_2, e_2'}

1841: \end{align*}

1842: Consider first the case when $nl_1-(nl_s'+k_s) \geq ol_2$.

1843: Since (m6) applies to the first expression we know that $nl_1 = nl_s +

1844: k_s$ and thus $nl_s - nl_s' \geq ol_2$. The first expression then

1845: rewrites to

1846: \begin{multline*}

1847: (\env{t_s,ol_s,nl_r+k_r+nl_s-ol_2, \menv{s,nl_s,ol_2,e_2}},\\

1848: nl_r+k_r+nl_1-ol_2))

1849: :: \menv{e_3,nl_1,ol_2,e_2}

1850: \end{multline*}

1851: The second expression rewrites using (m5) multiple times to

1852: \[ (\env{t_s',ol_s,nl_s',s'},nl_s'+k_s)::e_3' \] It is easily seen

1853: that $exp \gg \menv{s,nl_s,ol_2,e_2}$ and $exp' \gg

1854: \menv{s',nl_s,ol_2,e_2'}$. Moreover, $\menv{s,nl_s,ol_2,e_2}$ and

1855: $\menv{s',nl_s,ol_2,e_2'}$ are similar so the inductive hypothesis

1856: applies and tells us these merged environments rewrite to similar

1857: simple environments. Since $nl_s - ol_2 \geq nl_s' \geq lev(s')$,

1858: applying \autoref{lem:backwards-m5} yields that

1859: $\menv{s,nl_s,ol_2,e_2}$ and $s'$ also rewrite to similar simple

1860: environments. By applying these rewrites, the heads of our two

1861: environments are now similar. By the inductive hypothesis we also know

1862: that $\menv{e_3,nl_1,ol_2,e_2}$ and $\menv{e_3',nl_1,ol_2,e_2'}$

1863: rewrite to similar simple environments. Since $nl_1 - lev(e_3') \geq

1864: ol_2$ we can apply \autoref{lem:backwards-m5} to know that

1865: $\menv{e_3,nl_1,ol_2,e_2}$ and $e_3'$ rewrite to similar simple

1866: environments, thus finishing this case.

1867: 

1868: The other case is when $nl_1-(nl_s'+k_s) < ol_2$. Then we can apply

1869: (m5) multiple times to $exp'$ and then eventually (m6),

1870: \begin{align*}

1871: exp'

1872: &= \menv{(\env{t_s',ol_s,nl_s',s'},nl_s'+k_s)::e_3',nl_1,ol_2, e_2'}\\

1873: &\many{(m5)} \lmenv (\env{t_s',ol_s,nl_s',s'},nl_s'+k_s)::e_3',

1874:  nl_s'+k_s, ol_2-nl_s+nl_s',\\

1875: &\hspace{1in} e_2'\{nl_s-nl_s'\} \rmenv\\

1876: &\one{(m6)} (\env{\env{t_s',ol_s,nl_s',s'}, ol_2-nl_s+nl_s',

1877:  l, e_2'\{nl_s-nl_s'\}},\\

1878: &\hspace{1in}l + (\monus{k_s}{(ol_2-nl_s)}))::\\

1879: &\hspace{2in} \menv{e_3', nl_s'+k_s, ol_2-nl_s+nl_s',

1880:   e_2'\{nl_s-nl_s'\}}

1881: \end{align*}

1882: Where $l = lev(e_2'\{nl_s-nl_s'\})$. Let us focus first on the tail

1883: portions of our two environments. By the inductive hypothesis

1884: $\menv{e_3,nl_1,ol_2,e_2}$ and $\menv{e_3',nl_1,ol_2,e_2'}$ rewrite to

1885: similar simple environments. Then by applying \autoref{lem:backwards-m5},

1886: $\menv{e_3,nl_1,ol_2,e_2}$ and

1887: $\menv{e_3',nl_s'+k_s,ol_2-nl_s+nl_s',e_2'\{nl_1-nl_s'\}}$ rewrite

1888: to similar simple environments.

1889: 

1890: Finally we focus on the heads of our environments. The head for

1891: $exp'$ can now be rewritten using (m1),

1892: \begin{align*}

1893: &\env{\env{t_s',ol_s,nl_s',s'}, ol_2-nl_s+nl_s',

1894:  l, e_2'\{nl_s-nl_s'\}}\\

1895: &\one{(m1)} \env{t_s', ol_s + ol_2 - nl_s, l, \menv{s', nl_s',

1896:     ol_2-nl_s+nl_s', e_2'\{nl_s-nl_s'\}}}

1897: \end{align*}

1898: Note that as before $exp \gg \menv{s,nl_s,ol_2,e_2}$ and $exp' \gg

1899: \menv{s',nl_s,ol_2,e_2'}$, also $\menv{s,nl_s,ol_2,e_2}$ and

1900: $\menv{s',nl_s,ol_2,e_2'}$ are similar, so by the inductive hypothesis

1901: these merged environments rewrite to similar simple environments.

1902: Since $nl_s-lev(s')\geq nl_s-nl_s'$ and $ol_2 \geq nl_s-nl_s'$,

1903: applying \autoref{lem:backwards-m5} yields that

1904: $\menv{s,nl_s,ol_2,e_2}$ and

1905: $\menv{s',nl_s',ol_2-nl_s+nl_s',e_2'\{nl_s-nl_s'\}}$ rewrite to

1906: similar simple environments. Using this rewriting results in the heads

1907: being similar.

1908: \end{proof}

1909: 

1910: %%% Local Variables:

1911: %%% mode: latex

1912: %%% TeX-master: "root"

1913: %%% End:

1914: