λ-Calculus Properties: A Call-By-Push-Value Case

Introduction

In this post, we will show the definitions and theorems of Call-By-Push-Value λ-Calculus (abbreviation: CBPV) by modifying from Takahashi's method. We assume you to be familiar with the reduction and CEK-machine of Call-By-Value λ-Calculus (abbreviation: CBV).

Definition

CBPV Syntax

Definition 1 - CBPV Syntax: The term of Call-By-Push-Value is mutually defined as following:

We have two kinds of terms - values and computations:

x stands for the free variable, so does all the x occuring in later context.
{c} stands for a thunk, a computation contains a computation.
produce v is a produce (known as return in some papers), also a computation containts a computation.
λx.c is the function with argument x and computation c. Unlike CBV where we say function is a value, function is a computation in CBPV.
!v is the term force, we use it to extra the computation inside thunk.
s v is application, we apply a value into a function.
let x ← c in s is like let in CBV at first glance (also known as to in original paper). However, it's not a syntactic sugar for application. It extracts c, a produce, then do substitution as the free variable x in s.

Definition 2 - Normal Form: Normal forms includes all the values, produce, and function.

The CBPV syntax looks like CBV with extra fancy terms, we will see how it distinguishes from CBV in the reduction definitions.

Reduction Strategies

Strong Reduction

Definition 3 - Strong Reduction: ⇒ is defined as strong reduction:

We will prove the strong reduction satisfies Church-Rosser theorem. For some theorems, this reduction is too strong to be induct directly. Therefore, we will further splits it into two cases: Weak Head Reduction and Non Head Reduction.

Weak Head Reduction

Definition 4 - Weak Head Reduction (or weak reduction): ⇝ is defined as weak head reduction, the β-reduction in usual sense:

The Weak Head Reduction reduces terms to normal form.

Now we can see the difference between CBPV and CBV by the weak reduction rules. Assume we add a rule for number addition:

We will have an addition rule (the + is the semantic of plus):

Since both M and N are already values, we don't need to further evaluate them. We can get the result directly. In CBV, however, the M and N might not be in normal form, which requires to evaluate both to a number first. For example, in (1 ⊕ 2) ⊕ 3, the ▫ ⊕ 3 will be push to call stack; and 1 ⊕ 2 is evaluated.

To rewrite the example in CBPV, it should be: let x ← produce (1 ⊕ 2) in produce (x ⊕ 3) or (λ x.produce(x ⊕ 3)) (1 ⊕ 2). Therefore, we can see that CBPV explicitly distinguish continuations in the application and let operators.

Non Head Reduction

Definition 5 - Non Head Reduction: ↠ is defined as non head reduction:

Unlike Weak Head Reduction, which only reduces from the outermost normal form, the Non Head Reduction preserves the outermost normal form; and only strongly reduces inside the normal form. The two reductions act like the complementary of Strong Reduction.

Once we figured out the definitions, the proving is easy.

Reflexive Transitive Closure for Reductions

Definition 6 - Reflexive Transitive Closure: We define R^* to be the reflexive transitive closure for relation R. So we have a R^* a, a R b → a R^* b, and a R^* b → b R^* c → a R^* c. Then we have following notations:

⇒^*: reflexive transitive reduction
⇝^*: reflexive transitive weak-head reduction
↠^*: reflexive transitive non-head reduction

Examples

If you find reading the reduction rules confusing, you can check the example in Levy's thesis and the source code of available CBPV implementations.

Takahashi's method for CBPV

This is adapted from Takahashi's method of Standardization. We show some important lemmas and properties of CBPV. Proof is omitted, but you can find a Coq version proof here.

Parallel Reduction

Lemma 1.1: M ⇒ M′ → N ⇒ N′ → M[N/x] ⇒ M′[N′/x]
Lemma 1.2: M ⇝ M′ → M[N/x] ⇒ M′[N/x]
Lemma 1.3: M ↠ M′ → N ↠ N′ → M[N/x] ↠ M′[N′/x]

It's an essential lemma for substitution. Lemma 1.2 is not like 1.1 and 1.3, because weak head reduction can only reduce on the outermost term. Once the free variables inside a term are replaced, only strong reduction and non-head reduction can reduce it.

Reduction Relations

We will see the relations of different reduction strategies.

Lemma 2.1: M ⇒ M′ → ∃N, M⇝^*N ∧ N ↠ M′. This is one of most important lemma telling us a strong reduction can be decomposed by multiple weak head reduction and a non head reduction.
Lemma 2.2: M ↠ N → N ⇝ P → ∃N, M ⇝ O ∧ O ⇒ P. It's a helper lemma to prove 2.4.
Corollary 2.3: M⇒^*M → ∃N, M⇝^*N ∧ N↠^*M′. Immediate from the previous two lemmas.
Corollary 2.4: M ↠ N → N ⇝ P → ∃N, M⇝^*O ∧ O ⇒ P. This lemma helps us to exchange the head reduction and non-head reduction order.

Church Rosser Theorem

Church-Rosser Theorem, also known as the confluence property of λ-Calculus, states that applying the strong β-reduction rules to λ-Calculus in different ways will not change the results of the reduction. Formally:

M⇒^*N → M⇒^*N′ → ∃O, N⇒^*O ∧ N⇒^*O.

Coq Formalization

Here is a formalized proof in Coq in both CBPV in CBV.