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 1 - CBPV Syntax: The term of Call-By-Push-Value is mutually defined as following:
We have two kinds of terms - values and computations:
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.
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.
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.
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.
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:
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.
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.
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.
We will see the relations of different reduction strategies.
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.
Here is a formalized proof in Coq in both CBPV in CBV.