Interconnecting Between CPS Terms and Non-CPS Terms ^{∗}

Jung-taek Kim and Kwangkeun Yi ^{†}

ROPAS ^{‡}

Department of Computer Science KAIST ^{§}

Abstract

We present a type-based partial CPS transformation (CPStransforming only a sub-part of a program) and its correctness proof. A program’s sub-parts which need to be CPStransformed are initially annotated as such. Partial CPStransformation scans the expressions and selectively apply the transformation depending on the annotation. Wherever an interface between CPS-transformed and direct-style expressions is needed, proper conversion code is padded based on expression types. The correctness of the partial CPS transformation is proven similarly to that of Plotkin’s simulation theorem[Plo75].

1 This Work

Is it possible to CPS-transform only a sub-part of a program, leaving others in direct-style? Such partial CPStransformation is needed, for example, to link CPS-transformed modules with non-CPS modules or to minimize the performance overhead by the transformation[KYD98].

In this article we present a type-based partial CPS transformation. The partial CPS transformation transforms only parts of a program and connects the results to the rest, direct-style parts. A program’s sub-parts which need to be CPS-transformed is initially annotated as such. Partial CPS-transformation scans the expressions and selectively apply the transformation depending on the annotation. Wherever an interface between CPS-transformed and direct-style expressions is needed, proper conversion code is padded based on expression types.

Let’s consider an example code:

((λx.x) 1) + 1

Assume that we want to CPS-transform only the function part - λx.x. A CPS transformed version of the function part is: λK.K (λx.λK.K x). To use the CPS-transformed function inside the non-CPS context ([] 1) + 1, we wrap the CPS-function position with a conversion code as follows:

λy.([](λx.x) y (λx.x))

where the first identity continuation is for the function expression itself and the second identity continuation is for the function’s result. By merging all components, we get a partially CPS transformed code :

((λy.(λK.K (λx.λK.K x)) (λx.x) y (λx.x))1) + 1.

2 Source Language and CPS Transformation

We consider ML’s core language with annotations. Its abstract syntax reads as follows. (κ denotes a data constructor)

expressions e ::= t^{a}
t ::= 1
| λx.e
| fix f λx.e
| x
| e_{1}@e_{2}

                                                                                 | con κ e
                                                                                 | decon e

| case e_{1} κ e_{2} e_{3}
annotation a ::= N | C

Annotation C denotes that the expression needs CPS transformation and N otherwise. Value κ·v is constructed by “con κ e” where evaluating e yields v. Symmetrically, value κ·v denoted by e is deconstructed into v by evaluating “decon e”. Evaluating the case expression “case e_{1} κ e_{2} e_{3}” yields the value of e_{2} if the value of e_{1} is κ·v; otherwise, it yields the value of e_{3}.

We assume that the source programs are type-checked before processing. Types range over τ :

types τ ::= ι
| τ → τ
| α
| μ α.τ_{κ_{1}}+τ_{κ_{2}}

ι denotes basic types, τ → τ denotes function types and μ α.τ_{κ_{1}}+τ_{κ_{2}} denotes user-defined recursive types where data constructor κ_{1} has type τ_{κ_{1}} → (μ α.τ_{κ_{1}}+τ_{κ_{2}}) and κ_{2} has type τ_{κ_{2}} → (μ α.τ_{κ_{1}}+ τ_{κ_{2}}). And we use the conventional mono-morphic type system for the ML core language.

Figure 1 shows the conventional call-by-value CPS transformation [Plo75] which transforms the whole program(we ignore the annotations).

∗This work is supported by Creative Research Initiatives of Korean Ministry of Science and Technology.

†email:{judaigi,kwang}@ropas.kaist.ac.kr

‡

Research On Program Analysis System

(http://ropas.kaist.ac.kr)

§

Korea Advanced Institute of Science and Technology

(http://www.kaist.ac.kr)

[[1]] = λK.K@1
[[x]] = λK.K@x
[[con κ e]] = λK.[[e]]@(λv.K@(con κ v))
[[decon e]] = λK.[[e]]@(λv.K@(decon v))
[[λx.e]] = λK.K@(λx.[[e]])
[[fix f λx.e]] = λK.K@(fix f λx.[[e]])
[[e_{1}@e_{2}]] = λK.[[e_{1}]]@(λf.[[e_{2}]] (λv.f@v@K))
[[case e_{1} κ e_{2} e_{3}]] =

λK.[[e_{1}]]@(λv.case v κ ([[e_{2}]]@K) ([[e_{3}]]@K))

Figure 1: Base CPS transformation [[·]]

3 Conversion Functions and Partial CPS Transformation

Partial CPS transformation receives an annotated program and outputs a partially CPS transformed version of it. Cannotated expressions are targets for CPS transformation.

Not all annotations lead to correct translations. If a variable occurs at multiple positions, they all should have the same annotation. In case that a variable is bound, its annotation should match with that of its binding expression. Annotated programs satisfying these constraints are called consistent:

Definition 1 (Consistency of Annotations) Annotations in an expression e is called consistent whenever the following holds :

• If x^{a} and x^{a′} are free variables in e then a and a′ are equal.

• If x^{a} is bounded by a sub-expression (λx.e)^{a′}, (fixfλx.e)^{a′}, or (fix x λy.e)^{a′} in e then a and a′ are equal.

In partial CPS transformation, we need conversion codes that interface CPS transformed expressions with non-CPS contexts and vice versa. We have to consider three cases according to the types of the expressions to be converted:

• For expressions of base type ι :

No conversion is necessary. CPS version of a basetyped expression just passes to the continuation the value computed by the non-CPS version.

• For expressions of function type τ_{1} → τ_{2} :

We eta-expand them to set up conversion codes around their arguments and results. For example, let’s assume a CPS function is used in a non-CPS part. Then its argument should be a non-CPS value. So, we convert the argument to a CPS expression and apply it to the function. Because function’s result is a CPS expression, we convert the result to a non-CPS expression.

• For expressions of user-defined type μ α.τ_{κ_{1}}+τ_{κ_{2}} : An expression of this user-defined type will be evaluated to κ_{1}·v or κ_{2}·v. In order to convert the argument value v, because the argument value v can also be κ_{1}·v′ or κ_{2}·v′ (due to recursive type), we should make a recursive conversion function. This conversion function deconstructs the value, converts the argument value recursively, and reconstructs.

The conversion codes are generated by two mutually recursive functions c2n (CPS to non-CPS) and n2c (non-CPS to CPS) which are inductively defined over the types as follows:

• The c2n function, given the type of a non-CPS expression, generates a conversion code that converts the values of the type into their CPS versions, to be used inside a CPS context:

c2n(ι)  = λv.v
c2n(τ_{1} → τ_{2}) = λv.λx.v@(n2c(τ_{1})@x)@c2n(τ_{2})

c2n(μ α.τ_{κ_{1}}+τ_{κ_{2}}) =

(fix f λy. case y κ_{1}

(con κ_{1} (c2n([α^{f} /α]τ_{κ_{1}})@(decon y))) (con κ_{2} (c2n([α^{f} /α]τ_{κ_{2}})@(decon y))))

c2n(α^{f})  = f

Note that the conversion code for a recursive type μ α.τ_{κ_{1}}+τ_{κ_{2}} is a recursive function “fix f λx.−.” The code for a recursive call to f is generated when n2c is called with the recursive type α^{f}.

• The n2c receives the original type of CPS expression. The output is a conversion code that will convert the CPS values into their non-CPS versions, to be used inside a non-CPS context.

n2c(ι)  = λv.v
n2c(τ_{1} → τ_{2}) =

λv.λx.λK.K@(n2c(τ_{2})@(v@(c2n(τ_{1})@x)))

n2c(μ α.τ_{κ_{1}}+τ_{κ_{2}}) =

(fix f λy. case y κ_{1}

(con κ_{1} (n2c([α^{f} /α]τ_{κ_{1}})@(decon y))) (con κ_{2} (n2c([α^{f} /α]τ_{κ_{2}})@(decon y))))

n2c(α^{f})  = f

The conversion codes can be generated at compile time because sizes of types are finite.

The partial CPS transformation [[·]]_{N} and [[·]]_{C} by using the two conversion-code-generators (c2n and n2c) are defined in Figure 2. For a term t, we write τ_{t} for its type.

4 Correctness of Partial CPS transformation

To prove the correctness of our partial CPS transformation, we extend our annotated language to have annotation sequences, not just a single annotation. These annotation sequences are used to trace the changes of annotations (hence the conversions between CPS and non-CPS styles) during the evaluation.

[[1^{N}]]_{N} = 1
[[(λx.e)^{N}]]_{N} = λx.[[e]]_{N}
[[(fix f λx.e)^{N}]]_{N} = fix f λx.[[e]]_{N}
[[x^{N}]]_{N} = x
[[(e_{1}@e_{2})^{N}]]_{N} = [[e_{1}]]_{N}@[[e_{2}]]_{N}
[[(con κ e)^{N}]]_{N} = con κ [[e]]_{N}
[[(decon e)^{N}]]_{N} = decon [[e]]_{N}
[[(case e_{1} κ e_{2} e_{3})^{N}]]_{N} = case [[e_{1}]]_{N} κ [[e_{2}]]_{N} [[e_{3}]]_{N}
[[t^{C}]]_{N} = [[t^{C}]]_{C}@c2n(τ_{t})
[[1^{C}]]_{C} = λK.K@1
[[(λx.e)^{C}]]_{C} = λK.K@λx.[[e]]_{C}
[[(fix f λx.e)^{C}]]_{C} = λK.K@fix f λx.[[e]]_{C}
[[x^{C}]]_{C} = λK.K@x
[[(e_{1}@e_{2})^{C}]]_{C} = λK.[[e_{1}]]_{C}@

(λf.[[e_{2}]]_{C}@(λv.f@v@K))

[[(con κ e)^{C}]]_{C} = λK.[[e]]_{C}@(λv.K@(con κ v))
[[(decon e)^{C}]]_{C} = λK.[[e]]_{C}@(λv.K@(decon v))
[[(case e_{1} κ e_{2} e_{3})^{C}]]_{C} = λK.[[e_{1}]]_{C}@(λv.case v κ

([[e_{2}]]_{C}@K) ([[e_{2}]]_{C}@K))

[[t^{N}]]_{C} = λK.K@(n2c(τ_{t})@[[t^{N}]]_{N})

Figure 2: Partial CPS transformation

annotated expressions

e ::= t^{a} | e^{a}
t ::= 1
| λx.e
| fix f λx.e
| κ·v
| x
| e_{1}@e_{2}

| con κ e
| decon e

| case e_{1} κ e_{2} e_{3}

annotated values

v ::= w^{a} | v^{a}
w ::= 1
| λx.e
| fix f λx.e
| κ·v

annotation

a ::= N | C

For convenience, we use the following notation:

annotation sequence  l ::= a | la
annotated expressions t^{la} = (t^{l})^{a}
reversal of annotations \overline{a} = a
\overline{al} = \overline{l}a

We now define the semantics of annotated expressions. This semantics is equivalent to that of ML core language except that we book-keep the annotations during reduction. The annotated evaluation context E is defined by the following grammar:

annotated contexts

E ::= D^{a}
D ::= [ ]
| E@e
| v@E

                       | con κ E
                       | decon E

| case E κ e_{1} e_{2}

This context defines a left-to-right, call-by-value reduction. As usual, we write E[e] if the hole in context E is filled with e. We use this context to define the reduction rules for arbitrary expressions :

{e ↦ e′ \atop E[e] → E[e′]}

The single reduction step e ↦ e′ for a redex e is defined as :

((λx.e)^{l}@v)^{a} ↦ [v^{a\overline{l}}/x]e^{la}
((fix f λx.e)^{l}@v)^{a′} ↦ [(fix f λx.e)^{a}/f][v^{a′\overline{l}}/x]e^{la′}

(head of l is a)

(con κ v)^{a} ↦ (κ·v)^{a}
(decon (κ·v)^{l})^{a} ↦ (v)^{la}
(case (κ·v)^{l} κ e_{1} e_{2})^{a} ↦ e_{1}^{a}
(case (κ·v)^{l} κ′ e_{1} e_{2})^{a} ↦ e_{2}^{a}  (κ ≠ κ′)

Notation [v/x]e denotes, as usual, the new expression that results from substituting v for every free occurrence of x in e.

Definition 2 The semantics of a closed annotated expression e is defined to be the sequence of reduction steps

e → e_{1} → e_{2} → · · · .

If the sequence terminates with a value v after zero or more reductions, we write

e →^{∗} v

Now we can define a correctness theorem for our partial CPS transformation similarly to the simulation theorem in [Plo75].

Theorem 1 (Correctness of Partial CPS transformation) For any closed expression e with consistent annotations,

e →^{∗} v ⟺ [[e]]_{N} →^{∗} Ψ_{N}(v)

where the auxiliary functions Ψ_{N} and Ψ_{C} coerces direct-style values to partial CPS values:

Ψ_{N}(1^{N}) = 1
Ψ_{N}((λx.e)^{N}) = λx.[[e]]_{N}
Ψ_{N}((fix f λx.e)^{N}) = fix f λx.[[e]]_{N}
Ψ_{N}((κ·v)^{N}) = κ·Ψ_{N}(v)
Ψ_{N}(v^{N}) = Ψ_{N}(v)
Ψ_{N}(w^{C}) = w′ (c2n(τ_{w})@Ψ_{C}(w^{C}) →^{∗} w′)
Ψ_{N}(v^{C}) = v′  (c2n(τ_{v})@Ψ_{C}(v^{C}) →^{∗} v′)
Ψ_{C}(1^{C}) = 1
Ψ_{C}((λx.e)^{C}) = λx.[[e]]_{C}
Ψ_{C}((fix f λx.e)^{C}) = fix f λx.[[e]]_{C}
Ψ_{C}((κ·v)^{C}) = κ·Ψ_{C}(v)
Ψ_{C}(v^{C}) = Ψ_{C}(v)
Ψ_{C}(w^{N}) = w′ (n2c(τ_{w})@Ψ_{N}(w^{N}) →^{∗} w′)
Ψ_{C}(v^{N}) = v′  (n2c(τ_{v})@Ψ_{N}(v^{N}) →^{∗} v′)

[[v]]_{N} = Ψ_{N}(v)
[[(λx.e)^{N}]]_{N} = λx.[[e]]_{N}
[[(fix f λx.e)^{N}]]_{N} = fix f λx.[[e]]_{N}
[[x^{N}]]_{N} = x
[[(e_{1}@e_{2})^{N}]]_{N} = [[e_{1}]]_{N}@[[e_{2}]]_{N}
[[(con κ e)^{N}]]_{N} = con κ [[e]]_{N}
[[(decon e)^{N}]]_{N} = decon [[e]]_{N}
[[(case e_{1} κ e_{2} e_{3})^{N}]]_{N} = case [[e_{1}]]_{N} κ [[e_{2}]]_{N} [[e_{3}]]_{N}
[[e^{N}]]_{N} = [[e]]_{N}
[[t^{C}]]_{N} = [[t^{C}]]_{C}@c2n(τ_{t})
[[e^{C}]]_{N} = [[e^{C}]]_{C}@c2n(τ_{e})
[[v]]_{C} = λK.K@Ψ_{C}(v)
[[(λx.e)^{C}]]_{C} = λK.K@λx.[[e]]_{C}
[[(fix f λx.e)^{C}]]_{C} = λK.K@fix f λx.[[e]]_{C}
[[x^{C}]]_{C} = λK.K@x
[[(e_{1}@e_{2})^{C}]]_{C} = λK.[[e_{1}]]_{C}@

(λf.[[e_{2}]]_{C}@(λv.f@v@K))

[[(con κ e)^{C}]]_{C} = λK.[[e]]_{C}@(λv.K@(con κ v))
[[(decon e)^{C}]]_{C} = λK.[[e]]_{C}@(λv.K@(decon v))
[[(case e_{1} κ e_{2} e_{3})^{C}]]_{C} = λK.[[e_{1}]]_{C}@(λv.case v κ

([[e_{2}]]_{C}@K) ([[e_{2}]]_{C}@K))

[[e^{C}]]_{C} = [[e]]_{C}
[[t^{N}]]_{C} = λK.K@(n2c(τ_{t})@[[t^{N}]]_{N})
[[e^{N}]]_{C} = λK.K@(n2c(τ_{e})@[[e^{N}]]_{N})

Figure 3: Extended Partial CPS transformation

We use a similar approach to [Plo75] to prove the above theorem.

At first, we extend the partial CPS transformation to be defined also for the intermediate expressions during reduction. Then we define two colon operators : and :K to represent the expressions after the administrative reduction. Operator : is used for [[·]]_{N} and :K for [[·]]_{C}. In partially CPS-transforming the intermediate expressions, computed values (closed expressions without redices) are transformed by a special transformers Ψ_{N} and Ψ_{C}. The extended partial CPS transformation is defined in Figure 3.

Figure 4 defines the two colon operators (: and :K) which represent the transformed terms (respectively from the [[·]]_{N} and [[·]]_{C}) after the administrative reductions.

Value transformation preserves the structure of the values: Lemma 1

Ψ_{N}((κ·v)^{l}) = κ·Ψ_{N}(v^{l}) and Ψ_{C}((κ·v)^{l}) = κ·Ψ_{C}(v^{l})

Proof. Proof by induction on the length of l. The details of the proof are in Appendix A. □

Following three Lemmas correspond to the Plotkin’s ones [Plo75]. Substitution Lemma enables substitions to penetrate [[·]]_{N} and [[·]]_{C}:

Lemma 2 (Substitution) For any expression e with consistent annotation and any value v, if free variable x is annotated as N then

\begin{aligned}[Ψ_{N}(v)/x][[e]]_{N} & = & [[[v/x]e]]_{N} \\ [Ψ_{N}(v)/x][[e]]_{C} & = & [[[v/x]e]]_{C} \end{aligned}

v: = Ψ_{N}(v)
(v_{1}@v_{2})^{N}: = (Ψ_{N}(v_{1}))@(Ψ_{N}(v_{2}))
(v@e)^{N}: = (Ψ_{N}(v))@(e:)
(e_{1}@e_{2})^{N}: = (e_{1}:)@[[e_{2}]]_{N}
(con κ v)^{N}: = con κ (Ψ_{N}(v))
(con κ e)^{N}: = con κ (e:)
(decon v)^{N}: = decon (Ψ_{N}(v))

                                                                  (decon e)^{N}: = decon (e:)

(case v κ e_{1} e_{2})^{N}: = case (Ψ_{N}(v)) κ [[e_{1}]]_{N} [[e_{2}]]_{N}
(case e_{1} κ e_{2} e_{3})^{N}: = case (e_{1}:) κ [[e_{2}]]_{N} [[e_{3}]]_{N}
e^{N}: = e:
t^{C}: = t^{C}:c2n(τ_{t})
e^{C}: = e^{C}:c2n(τ_{e})
v:K = K@Ψ_{C}(v)
(v_{1}@v_{2})^{C}:K = Ψ_{C}(v_{1})@Ψ_{C}(v_{2})@K
(v@e)^{C}:K = e:λv.Ψ_{C}(v)@v@K
(e_{1}@e_{2})^{C}:K = e_{1}:λf.[[e_{2}]]_{C}@(λv.f@v@K)
(con κ v)^{C}:K = K@(con κ (Ψ_{C}(v)))
(con κ e)^{C}:K = e:λv.K@(con κ v)
(decon v)^{C}:K = K@(decon (Ψ_{C}(v)))
(decon e)^{C}:K = e:λv.K@(decon v)
(case v κ e_{1} e_{2})^{C}:K = case (Ψ_{C}(v)) κ
([[e_{1}]]_{C}@K) ([[e_{2}]]_{C}@K)
(case e_{1} κ e_{2} e_{3})^{C}:K = e_{1}:(λv.case v κ
([[e_{2}]]_{C}@K)([[e_{3}]]_{C}@K))
e^{C}:K = e:K
t^{N}:K = K@(n2c(τ_{t})@(t^{N}:))
e^{N}:K = K@(n2c(τ_{e})@(e^{N}:))

Figure 4: The Colon Operators

and if free variable x is annotated as C then

\begin{aligned}[Ψ_{C}(v)/x][[e]]_{N} & = & [[[v/x]e]]_{N} \\ [Ψ_{C}(v)/x][[e]]_{C} & = & [[[v/x]e]]_{C} \end{aligned}

Proof. Proof by mutual structural induction on e with a case for type of expression. The details of the proof are in Appendix B. □

Static reduction Lemma establishes the relation between partial CPS transformation and colon operator:

Lemma 3 (Static Reduction) For any closed expression e with consistent annotation and any closed value K,

\begin{matrix}[[e]]_{N} & →^{∗} & e: \\ [[e]]_{C}@K & →^{∗} & e:K \end{matrix}

Proof. Proof by mutual structural induction on e with a case for type of expression. The details of the proof are in Appendix C. □

Single-Step Simulation Lemma shows that a reduction from an original expression corresponds to reductions between partially CPS transformed expressions:

Lemma 4 (Single-Step Simulation) For any closed expression e with consistent annotations and any closed value K,

e → e′ ⟹ e: →^{+} e′: and e:K →^{+} e′:K

Proof. Proof by mutual structural induction on the reduction e → e′ with a case for type of reduction rules. The details of the proof are in Appendix D. □

Proof of Theorem 1. Using the lemmas, we can prove the correctness theorem easily. If the original program evaluates to a value, that is , e →^{∗} v then

[[e]]_{N}

→^{∗} e:  (Lemma 3)
→^{∗} v:  (repeated use of Lemma 4)
= Ψ_{N}(v)  (def. of :)

Note that non-termination is also preserved by the single step simulation.

□

5 Conclusion

We presented a type-based partial CPS transformation. The partial CPS transformation transforms only parts of a program and connects the results to the rest, direct-style parts. A program’s sub-parts which need to be CPS-transformed is initially annotated as such. Partial CPS-transformation scans the expressions and selectively apply the transformation depending on the annotation. Wherever an interface between CPS-transformed and direct-style expressions is needed, proper conversion code is padded based on expression types. The correctness of the partial CPS transformation is proven similarly to that of Plotkin’s simulation theorem[Plo75].

There are analogous works in literature. Our n2c and c2n functions can be seen as the retraction pairs in the setting of Meyer and Wand[MW85]. Danvy, Dussart, and Hatcliff [DD95, DH93a, DH93b]’s works are analogous to ours. They switch between call-by-value and call-by-name CPS transformations interconnecting the two transformations by “delay” and “force” operators. Another analogous one is Leroy’s “box” and “unbox” operators[Ler92] that are used to handle mixed representations of values.

References

[DD95] Olivier Danvy and Dirk Dussart. CPS transformation after binding-time analysis. Unpublished note, Department of Computer Science, University of Aarhus, April 1995.

[DH93a] Olivier Danvy and John Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems, 1(3):195– 212, 1993.

[DH93b] Olivier Danvy and John Hatcliff. On the transformation between direct and continuation semantics. In Stephen Brookes, Michael Main, Austin Melton, Michael Mislove, and David Schmidt, editors, Proceedings of the 9th Conference on Mathematical Foundations of Programming Semantics, number 802 in Lecture Notes in Computer Science, pages 627–648, New Orleans, Louisiana, April 1993. Springer-Verlag.

[KYD98] Jung-taek Kim, Kwangkeun Yi, and Olivier Danvy. Assessing the overhead of ML exceptions by selective CPS transformation. In Greg Morrisett, editor, Record of the 1998 ACM SIG-PLAN Workshop on ML and its Applications, Baltimore, Maryland, September 1998. Also appears as BRICS technical report RS-98-15.

[Ler92] Xavier Leroy. Unboxed objects and polymorphic typing. In Proceedings of ACM Symposium on Principles of Programming Languages, pages 177– 188, January 1992.

[MW85] Albert R. Meyer and Mitchell Wand. Continuation semantics in typed lambda-calculi. In R. Parikh, editor, Logics of Programs, volume 193 of Lecture Notes in Computer Science, pages 219– 224. Springer, Brooklyn, June 1985.

[Plo75] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

A Proof of Lemma 1

Lemma 1

Ψ_{N}((κ·v)^{l}) = κ·Ψ_{N}(v^{l}) and Ψ_{C}((κ·v)^{l}) = κ·Ψ_{C}(v^{l})

Proof.

Proof by induction on the length of l.

In proof, we abbreviate some expressions as “(⋯)” when they are omittable. For Ψ_{N} cases,

• base case (κ·v)^{N}

Ψ_{N}((κ·v)^{N})

= κ·Ψ_{N}(v)  (def. of Ψ_{N})
= κ·Ψ_{N}(v^{N})  (def. of Ψ_{N})

• base case (κ·v)^{C}

c2n(μ α.τ_{κ}+τ_{κ′})@Ψ_{C}((κ·v)^{C})

= (fix f λy.case y κ

(con κ c2n([α^{f} /α]τ_{κ})@(decon y)) (⋯))

@(κ·Ψ_{C}(v))  (def. of n2c and Ψ_{N})
→ case (κ·Ψ_{C}(v)) κ

(con κ (c2n([α^{f′}/α]τ_{κ})

@(decon (κ·Ψ_{C}(v))))) (⋯)

(where f′ is fix f ⋯)

→^{+} con κ (c2n([α^{f′}/α]τ_{κ})@(Ψ_{C}(v)))
= con κ (c2n([α^{f′}/α]τ_{κ})@(Ψ_{C}(v^{C})))
(def. of Ψ_{N})
→^{∗} con κ (Ψ_{N}(v^{C}))

(Because [α^{f′}/α]τ_{κ} is indeed the type of v,

c2n([α^{f′}/α]τ_{κ})@Ψ_{C}(v^{C}) →^{∗} v′ = Ψ_{N}(v^{C})

by definition of Ψ_{N}.)

→ κ·(Ψ_{N}(v^{C}))

By above and definition of Ψ_{N},

\begin{matrix}Ψ_{N}((κ·v)^{C}) \\ = & κ·Ψ_{N}(v^{C}) \end{matrix}

• induction step case (κ·v)^{lN}

Ψ_{N}((κ·v)^{lN})

= Ψ_{N}((κ·v)^{l})  (def. of Ψ_{N})
= κ·Ψ_{N}((v)^{l})  (I.H.)
= κ·Ψ_{N}((v)^{lN})  (def. of Ψ_{N})

• induction step case (κ·v)^{lC}

c2n(μ α.τ_{κ}+τ_{κ′})@Ψ_{C}((κ·v)^{lC})

= c2n(μ α.τ_{κ}+τ_{κ′})@Ψ_{C}((κ·v)^{l})  (def. of Ψ_{C})
= (fix f λy.case y κ

(con κ c2n([α^{f} /α]τ_{κ})@(decon y)) (⋯))

@(κ·Ψ_{C}(v^{l}))  (def. of n2c and I.H.)
→ case (κ·Ψ_{C}(v^{l})) κ

(con κ (c2n([α^{f′}/α]τ_{κ})

@(decon (κ·Ψ_{C}(v^{l}))))) (⋯) (where f′ is fix f ⋯)

→^{+} con κ (c2n([α^{f′}/α]τ_{κ})@(Ψ_{C}(v^{l})))
= con κ (c2n([α^{f′}/α]τ_{κ})@(Ψ_{C}(v^{lC})))

(def. of Ψ_{C})

→^{∗} con κ (Ψ_{N}(v^{lC}))

(Because [α^{f′}/α]τ_{κ} is indeed the type of v,

c2n([α^{f′}/α]τ_{κ})@Ψ_{C}(v^{lC}) →^{∗} v′ = Ψ_{N}(v^{lC})

by definition of Ψ_{N}.)

→ κ·(Ψ_{N}(v^{lC}))

By above and definition of Ψ_{N},

Ψ_{N}((κ·v)^{lC})

= κ·Ψ_{N}(v^{lC})  (def. of Ψ_{N})

Because Ψ_{T} and Ψ_{N} are duals, we can prove Ψ_{T} cases similarly to Ψ_{N} cases. □

B Proof of Substitution Lemma

Lemma 2 (Substitution) For any expression e with consistent annotation and any value v, if free variable x is annotated as N then

\begin{aligned}[Ψ_{N}(v)/x][[e]]_{N} & = & [[[v/x]e]]_{N} \\ [Ψ_{N}(v)/x][[e]]_{C} & = & [[[v/x]e]]_{C} \end{aligned}

and if free variable x is annotated as C then

\begin{aligned}[Ψ_{C}(v)/x][[e]]_{N} & = & [[[v/x]e]]_{N} \\ [Ψ_{C}(v)/x][[e]]_{C} & = & [[[v/x]e]]_{C} \end{aligned}

Proof.

Proof by mutual structural induction on e, firstly taking the [[·]]_{N} for the N annotated expressions and [[·]]_{C} for the C annotated expressions.

For [[·]]_{N} cases,

• case v, (λx.e_{1})^{N}, (fix f λx.e_{1})^{N}, or (fix x λy.e_{1})^{N}

[Ψ_{a}(v)/x][[e]]_{N}

= [[e]]_{N}  (x is not free)
= [[[v/x]e]]_{N}  (x is not free)

a is N or C according to the annotation of the free variable x.

• case (λy.e)^{N} (x ≠ y)

[Ψ_{a}(v)/x][[(λy.e)^{N}]]_{N}

= [Ψ_{a}(v)/x]λy.[[e]]_{N}  (def. of [[·]]_{N})
= λy.[Ψ_{a}(v)/x][[e]]_{N}  (def. of [/])
= λy.[[[v/x]e]]_{N}  (I.H.)
= [[(λy.[v/x]e)^{N}]]_{N}  (def. of [[·]]_{N})
= [[[v/x](λy.e)^{N}]]_{N}  (def. of [/])

a is N or C according to the annotation of the free variable x.

• case (fix f λy.e)^{N} (x ≠ y, x ≠ f)

We can prove similarly to the above (λy.e)^{N} case.

• case x^{N} Because the variable x is annotated as N, we need to prove only for Ψ_{N}.

[Ψ_{N}(v)/x][[x^{N}]]_{N}

= [Ψ_{N}(v)/x]x  (def. of [[·]]_{N})
= Ψ_{N}(v)  (def. of [/])
= Ψ_{N}(v^{N})  (def. of Ψ_{N})
= [[v^{N}]]_{N}  (def. of [[·]]_{N})
= [[[v/x]x^{N}]]_{N}  (def. of [/])

• case (e_{1}@e_{2})^{N} The annotations of the free variable x in both e_{1} and e_{2} are equal.

[Ψ_{a}(v)/x][[(e_{1}@e_{2})^{N}]]_{N}

= [Ψ_{a}(v)/x]([[e_{1}]]_{N}@[[e_{2}]]_{N})  (def. of [[·]]_{N})
= ([Ψ_{a}(v)/x][[e_{1}]]_{N})@([Ψ_{a}(v)/x][[e_{2}]]_{N})
(def. of [/])
= [[[v/x]e_{1}]]_{N}@[[[v/x]e_{2}]]_{N}  (I.H. twice)
= [[(([v/x]e_{1})@([v/x]e_{2}))^{N}]]_{N}  (def. of [[·]]_{N})
= [[[v/x](e_{1}@e_{2})^{N}]]_{N}  (def. of [/])

a is N or C according to the annotation of the free variable x.

• case (con κ e)^{N}, (decon e)^{N}, (case e_{1} κ e_{2} e_{3})^{N}, or e^{N}

We can prove similarly to the above (e_{1}@e_{2})^{N} case.

• case e^{C}

[Ψ_{a}(v)/x][[e^{C}]]_{N}

= [Ψ_{a}(v)/x]([[e^{C}]]_{C}@c2n(τ_{e}))  (def. of [[·]]_{N})
= ([Ψ_{a}(v)/x][[e^{C}]]_{C})@c2n(τ_{e})  (def. of [/])
= [[[v/x]e^{C}]]_{C}@c2n(τ_{e})  (I.H. about [[·]]_{C})
= [[[v/x]e^{C}]]_{N}  (def. of [[·]]_{N})

• case t^{C} We can prove similarly to the above e^{C} case.

For [[·]]_{C} cases,

• case v, (λx.e_{1})^{C}, (fix f λx.e_{1})^{C}, or (fix x λy.e_{1})^{C}

[Ψ_{a}(v)/x][[e]]_{C}

= [[e]]_{C}  (x is not free)
= [[[v/x]e]]_{C}  (x is not free)

a is N or C according to the annotation of the free variable x.

• case (λy.e)^{C} (x ≠ y)

[Ψ_{a}(v)/x][[(λy.e)^{C}]]_{C}

= [Ψ_{a}(v)/x]λK.K@λx.[[e]]_{C}  (def. of [[·]]_{C})
= λK.K@λx.[Ψ_{a}(v)/x][[e]]_{C}  (def. of [/])
= λK.K@λx.[[[v/x]e]]_{C}  (I.H.)
= [[(λy.[v/x]e)^{C}]]_{C}  (def. of [[·]]_{C})
= [[[v/x](λy.e)^{C}]]_{C}  (def. of [/])

a is N or C according to the annotation of the free variable x.

• case (fix f λy.e)^{C} (x ≠ y, x ≠ f)

We can prove similarly to the above (λy.e)^{C} case.

• case x^{C} Because the variable x is annotated as C, we need to prove only for Ψ_{C}.

[Ψ_{C}(v)/x][[x^{C}]]_{C}

= [Ψ_{C}(v)/x]λK.K@x  (def. of [[·]]_{C})
= λK.K@Ψ_{C}(v)  (def. of [/])
= λK.K@Ψ_{C}(v^{C})  (def. of Ψ_{C})
= [[v^{C}]]_{C}  (def. of [[·]]_{C})
= [[[v/x]x^{C}]]_{C}  (def. of [/])

• case (e_{1}@e_{2})^{C} The annotations of the free variable x in both e_{1} and e_{2} are equal.

[Ψ_{a}(v)/x][[(e_{1}@e_{2})^{C}]]_{C}

= [Ψ_{a}(v)/x]λK.[[e_{1}]]_{C}@(λf.[[e_{2}]]_{C}@(λv.f@v@K))
(def. of [[·]]_{C})
= λK.([Ψ_{a}(v)/x][[e_{1}]]_{C})@
(λf.([Ψ_{a}(v)/x][[e_{2}]]_{C})@(λv.f@v@K))
(def. of [/])
= λK.[[[v/x]e_{1}]]_{C}@(λf.[[[v/x]e_{2}]]_{C}@(λv.f@v@K))

(I.H.)

= [[(([v/x]e_{1})@([v/x]e_{2}))^{C}]]_{C}  (def. of [[·]]_{C})
= [[[v/x](e_{1}@e_{2})^{C}]]_{C}  (def. of [/])

a is N or C according to the annotation of the free variable x.

• case (con κ e)^{C}, (decon e)^{C}, (case e_{1} κ e_{2} e_{3})^{C}, or e^{C}

We can prove similarly to the above (e_{1}@e_{2})^{C} case.

• case e^{N}

[Ψ_{a}(v)/x][[e^{N}]]_{C}

= [Ψ_{a}(v)/x](λK.K@(n2c(τ_{e})@[[e^{N}]]_{N}))
(def. of [[·]]_{C})
= λK.K@(n2c(τ_{e})@([Ψ_{a}(v)/x][[e^{N}]]_{N}))
(def. of [/])
= λK.K@(n2c(τ_{e})@[[[v/x]e^{N}]]_{N})
(I.H. about [[·]]_{N})
= [[[v/x]e^{N}]]_{C}  (def. of [[·]]_{C})

a is N or C according to the annotation of the free variable x.

• case t^{N} We can prove similarly to the above e^{N} case.

□

C Proof of Static Reduction Lemma

Lemma 3 (Static Reduction) For any closed expression e with consistent annotation and any closed value K,

\begin{matrix}[[e]]_{N} & →^{∗} & e: \\ [[e]]_{C}@K & →^{∗} & e:K \end{matrix}

Proof.

Proof by mutual structural induction on e, firstly taking the [[·]]_{N} for the N annotated expressions and [[·]]_{C} for the C annotated expressions. For [[·]]_{N} cases,

• case v [[v]]_{N}

= Ψ_{N}(v)  (def. of [[·]]_{N})
= v:  (def. of :)

• case (v_{1}@v_{2})^{N}

[[(v_{1}@v_{2})^{N}]]_{N}

= [[v_{1}]]_{N}@[[v_{2}]]_{N}  (def. of [[·]]_{N})
= Ψ_{N}(v_{1})@Ψ_{N}(v_{2})  (def. of [[·]]_{N})
= (v_{1}@v_{2})^{N}:  (def. of :)

• case (v@e)^{N}

[[(v@e)^{N}]]_{N}

= [[v]]_{N}@[[e]]_{N}  (def. of [[·]]_{N})
= (Ψ_{N}(v))@[[e]]_{N}  (def. of [[·]]_{N})
→^{∗} (Ψ_{N}(v))@(e:)  (I.H.)
= (v@e)^{N}:  (def. of :)

• case (e_{1}@e_{2})^{N}, (con κ v)^{N}, (con κ e)^{N}, (decon v)^{N}, (decon e)^{N}, (case v κ e_{1} e_{2})^{N}, (case e_{1} κ e_{2} e_{3})^{N}, or e^{N} We can prove similarly to one of the above two cases - (v_{1}@v_{2})^{N}, (v@e)^{N}.

• case e^{C} [[e^{C}]]_{N}

= [[e^{C}]]_{C}@c2n(τ_{e})  (def. of [[·]]_{N})
→^{∗} [[e^{C}]]_{C}:c2n(τ_{e})  (I.H. about [[·]]_{C})
= e^{C}:  (def. of :)

• case t^{C} We can prove similarly to the above e^{C} case.

For C-annotated expressions and [[·]]_{C} cases,

• case v

[[v]]_{C}@K

→ K@Ψ_{C}(v)  (def. of [[·]]_{C})
= v:K  (def. of :K)

• case (v_{1}@v_{2})^{C}

[[(v_{1}@v_{2})^{C}]]_{C}@K

→ [[v_{1}]]_{C}@(λf.[[v_{2}]]_{C}@(λv.f@v@K))

(def. of [[·]]_{C})

= (λK.K@Ψ_{C}(v_{1}))@(λf.[[v_{2}]]_{C}@(λv.f@v@K))

(def. of [[·]]_{C})

→^{+} [[v_{2}]]_{C}@(λv.Ψ_{C}(v_{1})@v@K)
= (λK.K@Ψ_{C}(v_{2}))@(λv.Ψ_{C}(v_{1})@v@K)

(def. of [[·]]_{C})

→^{+} Ψ_{C}(v_{1})@Ψ_{C}(v_{2})@K
= (v_{1}@v_{2})^{C}:K  (def. of :K)

• case (v@e)^{C}

[[(v@e)^{C}]]_{C}@K

→ [[v]]_{C}@(λf.[[e]]_{C}@(λv.f@v@K)) (def. of [[·]]_{C})
= (λK.K@Ψ_{C}(v))@(λf.[[e]]_{C}@(λv.f@v@K))

(def. of [[·]]_{C})

→^{+} [[e]]_{C}@(λv.Ψ_{C}(v)@v@K)
→^{∗} e:λv.Ψ_{C}(v)@v@K  (I.H.)
= (v@e)^{C}:K  (def. of :K)

• case (e_{1}@e_{2})^{C}, (con κ v)^{C}, (con κ e)^{C}, (decon v)^{C}, (decon e)^{C}, (case v κ e_{1} e_{2})^{C}, (case e_{1} κ e_{2} e_{3})^{C}, ore^{C} We can prove similarly to one of the above two cases - (v_{1}@v_{2})^{C}, (v@e)^{C}.

• case e^{N}

[[e^{N}]]_{C}@K

→ K@(n2c(τ_{e})@[[e^{N}]]_{N})  (def. of [[·]]_{C})
→^{∗} K@(n2c(τ_{e})@(e^{N}:))  (I.H. about [[·]]_{N})
= e^{N}:K  (def. of :K)

• case t^{N} We can prove similarly to the above e^{N} case.

□

D Proof of Single Step Simulation Lemma

Lemma 4 (Single Step Simulation) For any closed expression e with consistent annotations and any closed value K,

e → e′ ⟹ e: →^{+} e′: and e:K →^{+} e′:K

Proof.

Proof by mutual structural induction on e, firstly taking : for the N annotated expressions and :K for the C annotated expressions.

For : cases,

• ((λx.e)^{l}@v)^{N} → [v^{N\overline{l}}/x]e^{lN} Prove this case by induction on the length of l.

– ((λx.e)^{N}@v)^{N} → [v^{NN}/x]e^{NN} By the consistency, free variable x in e should be annotated as N. ((λx.e)^{N}@v)^{N}:

= Ψ_{N}((λx.e)^{N})@(Ψ_{N}(v))  (def. of :)
= (λx.[[e]]_{N})@(Ψ_{N}(v))  (def. of Ψ_{N})
→ [Ψ_{N}(v)/x][[e]]_{N}
= [Ψ_{N}(v^{NN})/x][[e^{NN}]]_{N}

(def. of Ψ_{N} and [[·]]_{N})

= [[[v^{NN}/x]e^{NN}]]_{N}  (Lemma 2)
→^{∗} [v^{NN}/x]e^{NN}:  (Lemma 3)

– ((λx.e)^{C}@v)^{N} → [v^{NT} /x]e^{CN} By the consistency, free variable x in e should be annotated as C. And λx.e’s type should be τ_{1} → τ_{2}.

((λx.e)^{C}@v)^{N}:

= Ψ_{N}((λx.e)^{C})@Ψ_{N}(v)  (def. of :)
= (λx.Ψ_{C}((λx.e)^{C})@(n2c(τ_{1})@x)@
c2n(τ_{2}))@Ψ_{N}(v^{N})  (def. of Ψ_{N})
→ Ψ_{C}((λx.e)^{C})@(n2c(τ_{1})@Ψ_{N}(v^{N}))@c2n(τ_{2})
→^{∗} Ψ_{C}((λx.e)^{C})@Ψ_{C}(v^{N})@c2n(τ_{2})
(def. of Ψ_{C})
= (λx.[[e]]_{C})@Ψ_{C}(v^{N})@c2n(τ_{2}) (def. of Ψ_{C})
→ ([Ψ_{C}(v^{N})/x][[e]]_{C})@c2n(τ_{2})
= ([Ψ_{C}(v^{NC})/x][[e^{C}]]_{C})@c2n(τ_{2})
(def. of Ψ_{C} and [[·]]_{C})
= [[[v^{NC}/x]e^{C}]]_{C}@c2n(τ_{2})  (Lemma 2)
= [[[v^{NC}/x]e^{C}]]_{N}  (def. of [[·]]_{N})
→^{∗} [v^{NC}/x]e^{C}:  (Lemma 3)
= [v^{NC}/x]e^{CN}:  (def. of :)

– ((λx.e)^{lN}@v)^{N} → [v^{NN\overline{l}}/x]e^{lNN}

((λx.e)^{lN}@v)^{N}:

= Ψ_{N}((λx.e)^{lN})@(Ψ_{N}(v))  (def. of :)
= Ψ_{N}((λx.e)^{l})@(Ψ_{N}(v^{N}))  (def. of Ψ_{N})
= ((λx.e)^{l}@v^{N})^{N}:  (def. of :)
→^{+} [v^{NN\overline{l}}/x]e^{lN}:

(I.H. about the length of l)

= [v^{NN\overline{l}}/x]e^{lNN}:  (def. of :)

– ((λx.e)^{lT} @v)^{N} → [v^{NT \overline{l}}/x]e^{lT N} λx.e’s type should be τ_{1} → τ_{2}. ((λx.e)^{lT} @v)^{N}:

= Ψ_{N}((λx.e)^{lT})@(Ψ_{N}(v))  (def. of :)
= (λx.Ψ_{C}((λx.e)^{lT})@(n2c(τ_{1})@x)@c2n(τ_{2}))
@(Ψ_{N}(v^{N}))  (def. of Ψ_{N})
→ Ψ_{C}((λx.e)^{lT})
@(n2c(τ_{1})@Ψ_{N}(v^{N}))@c2n(τ_{2})
→^{∗} Ψ_{C}((λx.e)^{l})@Ψ_{C}(v^{N})@c2n(τ_{2})
(def. of Ψ_{C})
= ((λx.e)^{l}@v^{N})^{C}:c2n(τ_{2})  (def. of :K)
→^{+} ([v^{NT \overline{l}}/x]e^{lT}):c2n(τ_{2})

(I.H. about the length of l)

= ([v^{NT \overline{l}}/x]e^{lT}):
= ([v^{NT \overline{l}}/x]e^{lT N}):  (def. of :)

By induction, (((λx.e)^{l}@v)^{N}:) →^{+} ([v^{N\overline{l}}/x]e^{lN}:)

• ((fix f λx.e)^{al}@v)^{N} → [(fix f λx.e)^{a}/f][v^{N\overline{l}a}/x]e^{alN} (head of l is a) We can prove similarly to the above case except that f should annotated as the head of l.

• (con κ v)^{N} → (κ·v)^{N}

(con κ v)^{N}:

= con κ (Ψ_{N}(v))  (def. of :)
→ κ·(Ψ_{N}(v))
= Ψ_{N}(κ·v)  (def. of Ψ_{N})
= (κ·v):  (def. of :)
= (κ·v)^{N}:  (def. of :)

• (decon (κ·v)^{l})^{N} → v^{lN} (decon (κ·v)^{l})^{N}:

= decon (Ψ_{N}((κ·v)^{l}))  (def. of :)
= decon (κ·Ψ_{N}(v^{l}))  (Property 1)
→ Ψ_{N}(v^{l})
= v^{l}:  (def. of :)
= v^{lN}:  (def. of :)

• (case (κ·v)^{l} κ e_{1} e_{2})^{N} → e_{1}^{N}

(case (κ·v)^{l} κ e_{1} e_{2})^{N}:

= case (Ψ_{N}((κ·v)^{l})) κ [[e_{1}]]_{N} [[e_{2}]]_{N}  (def. of :)
= case (κ·Ψ_{N}(v^{l})) κ [[e_{1}]]_{N} [[e_{2}]]_{N}  (Property 1)
→ [[e_{1}]]_{N}
= [[e_{1}^{N}]]_{N}  (def. of [[·]]_{N})
→^{∗} e_{1}^{N}:  (Lemma 3)

• (case (κ·v)^{l} κ′ e_{1} e_{2})^{N} → e_{2}^{N} (κ ≠ κ′)

We can prove similarly to the above case.

• (e_{1}@e_{2})^{N} → (e′_{1}@e_{2})^{N} (e_{1} → e′_{1})

(e_{1}@e_{2})^{N}:

= (e_{1}:)@[[e_{2}]]_{N}  (def. of :)
→^{+} (e′_{1}:)@[[e_{2}]]_{N}  (I.H.)
= (e′_{1}@e_{2})^{N}:  (def. of :)

• (v@e)^{N} → (v@e′)^{N}, (con κ e)^{N} → (con κ e′)^{N}, (decon e)^{N} → (decon e′)^{N}, (case e_{1} κ e_{2} e_{3})^{N} → (case e′_{1} κ e_{2} e_{3})^{N}, We can prove similarly to the above case.

• e^{N} → e^{′N} Then e → e′. e^{N}:

= e:  (def. of :)
→^{+} e′:  (I.H.)
= e^{′N}:  (def. of :)

• e^{C} → e^{′C}

e^{C}:

= e^{C}:c2n(τ_{e})  (def. of :)
→^{+} e^{′C}:c2n(τ_{e})  (I.H. about :K)
= e^{′C}:  (def. of :)

• t^{C} → t^{′C} We can prove similarly to the above e^{C} case.

For :K cases,

• ((λx.e)^{l}@v)^{C} → [v^{C\overline{l}}/x]e^{lC} Prove this case by induction on the length of l.

– ((λx.e)^{C}@v)^{C} → [v^{CC}/x]e^{CC} By the consistency, free variable x in e should be annotated as C. ((λx.e)^{C}@v)^{C}:K

= Ψ_{C}((λx.e)^{C})@Ψ_{C}(v)@K  (def. of :K)
= (λx.[[e]]_{C})@Ψ_{C}(v)@K  (def. of Ψ_{C})
→ ([Ψ_{C}(v)/x][[e]]_{C})@K
= ([Ψ_{C}(v^{CC})/x][[e^{CC}]]_{C})@K

(def. of Ψ_{C} and [[·]]_{C})

= ([[[v^{CC}/x]e^{CC}]]_{C})@K  (Lemma 2)
→^{∗} [v^{CC}/x]e^{CC}:K  (Lemma 3)

– ((λx.e)^{N}@v)^{C} → [v^{CN}/x]e^{NC} By the consistency, free variable x in e should be annotated as N. And λx.e’s type should be τ_{1} → τ_{2}. ((λx.e)^{N}@v)^{C}:K

= Ψ_{C}((λx.e)^{N})@Ψ_{C}(v)@K  (def. of :K)
= (λx.λK.K@(n2c(τ_{2})@(Ψ_{N}((λx.e)^{N})
@(c2n(τ_{1})@x))))@Ψ_{C}(v^{C})@K
(def. of Ψ_{C})
→^{+} K@(n2c(τ_{2})@(Ψ_{N}((λx.e)^{N})
@(c2n(τ_{1})@Ψ_{C}(v^{C}))))
→^{∗} K@(n2c(τ_{2})@(Ψ_{N}((λx.e)^{N})@Ψ_{N}(v^{C})))
(def. of Ψ_{N})
= K@(n2c(τ_{2})@((λx.[[e]]_{N})@Ψ_{N}(v^{C})))
(def. of Ψ_{N})
→ K@(n2c(τ_{2})@([Ψ_{N}(v^{C})/x][[e]]_{N}))
= K@(n2c(τ_{2})@([Ψ_{N}(v^{CN})/x][[e^{N}]]_{N}))
(def. of Ψ_{N} and [[·]]_{N})
= K@(n2c(τ_{2})@([[[v^{CN}/x]e^{N}]]_{N}))(Lemma 2)
→^{∗} K@(n2c(τ_{2})@([v^{CN}/x]e^{N}:)) (Lemma 3)
= [v^{CN}/x]e^{N}:K  (def. of :K)
= [v^{CN}/x]e^{NC}:K  (def. of :K)

– ((λx.e)^{lC}@v)^{C} → [v^{CC\overline{l}}/x]e^{lCC}

((λx.e)^{lC}@v)^{C}:K

= Ψ_{C}((λx.e)^{lC})@Ψ_{C}(v)@K (def. of :K)
= Ψ_{C}((λx.e)^{l})@Ψ_{C}(v^{C})@K (def. of Ψ_{C})
= ((λx.e)^{l}@v^{C})^{C}:K  (def. of :K)
→^{+} [v^{CC\overline{l}}/x]e^{lC}:K

(I.H. about the length of l)

= [v^{CC\overline{l}}/x]e^{lCC}:K  (def. of :K)

– ((λx.e)^{lN}@v)^{C} → [v^{CN\overline{l}}/x]e^{lNC} λx.e’s type should be τ_{1} → τ_{2}. ((λx.e)^{lN}@v)^{C}:K

= Ψ_{C}((λx.e)^{lN})@Ψ_{C}(v)@K (def. of :K)
= (λx.λK.K@(n2c(τ_{2})@(Ψ_{N}((λx.e)^{lN})
@(c2n(τ_{1})@x))))@Ψ_{C}(v)@K

(def. of n2c())

→^{+} K@(n2c(τ_{2})@(Ψ_{N}((λx.e)^{lN})
@(c2n(τ_{1})@Ψ_{C}(v))))
→^{∗} K@(n2c(τ_{2})@(Ψ_{N}((λx.e)^{l})@Ψ_{N}(v^{C})))

(def. of Ψ_{N})

= K@(n2c(τ_{2})@(((λx.e)^{l}@v^{C})^{N}:))(def. of :)
= ((λx.e)^{l}@v^{C})^{N}:K  (def. of :K)
→^{+} [v^{CN\overline{l}}/x]e^{lN}:K(I.H. about the length of l)
= [v^{CN\overline{l}}/x]e^{lNC}:K  (def. of :K)

By induction, ((λx.e)^{l}@v)^{C}:K →^{+} [v^{C\overline{l}}/x]e^{lC}:K

• ((fix f λx.e)^{l}@v)^{C} → [(fix f λx.e)^{a}/f][v^{C\overline{l}}/x]e^{lC} (head of l is a) We can prove similarly to the above case except that f should annotated as the head of l.

• (con κ v)^{C} → (κ·v)^{C} (con κ v)^{C}:K

= K@(con κ Ψ_{C}(v))  (def. of :K)
→ K@(κ·Ψ_{C}(v))
= K@(Ψ_{C}((κ·v)^{C}))  (def. of Ψ_{C})
= (κ·v)^{C}:K  (def. of :K)

• (decon (κ·v)^{l})^{C} → v^{lC}

(decon (κ·v)^{l})^{C}:K

= K@(decon Ψ_{C}((κ·v)^{l}))  (def. of :K)
= K@(decon (κ·Ψ_{C}(v^{l})))  (Property 1)
→ K@Ψ_{C}(v^{l})
= v^{l}:K  (def. of :K)
= v^{lC}:K  (def. of :K)

• (case (κ·v)^{l} κ e_{1} e_{2})^{C} → e_{1}^{C}

(case (κ·v)^{l} κ e_{1} e_{2})^{C}:K

= case (Ψ_{C}((κ·v)^{l})) κ ([[e_{1}]]_{C}@K) ([[e_{2}]]_{C}@K)

(def. of :)

= case (κ·Ψ_{C}(v^{l})) κ ([[e_{1}]]_{C}@K) ([[e_{2}]]_{C}@K)

(Property 1)

→ [[e_{1}]]_{C}@K
= [[e_{1}^{C}]]_{C}@K  (def. of [[·]]_{C})
→^{∗} e_{1}^{C}:K  (Lemma 3)

• (case (κ·v)^{l} κ′ e_{1} e_{2})^{C} → e_{1}^{C} (κ ≠ κ′) We can prove similarly to the above case.

• (e_{1}@e_{2})^{C} → (e′_{1}@e_{2})^{C} (e_{1} → e′_{1})

(e_{1}@e_{2})^{C}:K

= e_{1}:λf.[[e_{2}]]_{C}@(λv.f@v@K)  (def. of :)
→^{+} e′_{1}:λf.[[e_{2}]]_{C}@(λv.f@v@K)  (I.H.)
= (e′_{1}@e_{2})^{C}:K  (def. of :)

• (v@e)^{C} → (v@e′)^{C}, (con κ e)^{C} → (con κ e′)^{C}, (decon e)^{C} → (decon e′)^{C}, (case e_{1} κ e_{2} e_{3})^{C} → (case e′_{1} κ e_{2} e_{3})^{C}, We can prove similarly to the above case.

• e^{C} → e^{′C} Then e → e′. e^{C}:K

= e:K  (def. of :K)
→^{+} e′:K  (I.H.)
= e^{′C}:K  (def. of :K)

• e^{N} → e^{′N}

e^{N}:K

= K@(n2c(τ_{e})@(e^{N}:))  (def. of :K)
→^{+} K@(n2c(τ_{e})@(e^{′N}:))  (I.H.)
= e^{′N}:K  (def. of :K)

• t^{N} → t^{′N}

We can prove similarly to the above e^{N} case.

□