Non-strict monadic evaluation contexts $E^b$

E^b ::= \cdot \mid (\text{if0}\ E^b\ e\ e) \mid (E^b\ e) \mid (v\ E^b) \mid (op\ \vec{v}\ E^b\ \vec{e})

B-reductions

\begin{aligned} E^b[(\text{let}\ (x\ e_1)\ e_2)] \quad\rightarrow\quad &\text{let}\ (x\ e_1)\ E^b[e_2]\quad &B_1 \\ &\text{where}\ E^b \ne \cdot \\ E^b[(\text{if0}\ v\ e_1\ e_2)] \quad\rightarrow\quad &\text{let}\ (y\ (\text{if0}\ v\ e_1\ e_2)) E^b[y]\quad &B_2 \\ &\text{where}\ E^b \ne \cdot, \text{fresh}\ y \\ E^b[(O\ \vec{v})] \quad\rightarrow\quad &\text{let}\ (y\ (O\ \vec{v}))\ E^b[y]\quad &B_3 \\ &\text{where}\ E^b \ne \cdot, \text{fresh}\ y \end{aligned}

如果定義 $B = \{B_1, B_2, B_3\}$ ，那麼這組規則會確保evaluation position上的non-value會被換成value。

Example 避免程式指數爆炸成長 [local-0]

相比起 $A_2$ 規則， $B_2$ 專門用來避免程式指數爆炸的轉換。我們再次回到失敗案例然後推導變換過程

let x := if0 (if0 (if0 0 0 1) 0 1) 0 1
in LARGE

我們改用 $E^b[-]$ 來轉換，由於不抽取let-if，所以我們要直接處理rhs，於是

let x :=
  let y := if0 (if0 0 0 1) 0 1
  in if0 y 0 1
in LARGE

下一步

let x :=
  let z := if0 0 0 1
  in let y := if0 z 0 1
  in if0 y 0 1
in LARGE

所以這確實不會導致大量的程式碼重複

Definition. Non-strict monadic evaluation contexts與B-normalization [PIBK]