Refactoring 2

So what is this mysterious $I{\beta }^{\prime }$? well, if $p$ was a program in $[[u\parallel u]]$, then $[[I{\beta }^{\prime }(u)\parallel I{\beta }^{\prime }(u)]]$ suggests programs $p^{\prime }$ for which $p^{\prime }⟶p$ is a semantically equivalent re-write.

$\ast proof\ast :$

• The first case is that $p^{\prime }=(\lambda b^{\prime })v^{\prime }$ where $v^{\prime }\in v$ and $b^{\prime }\in b$ such that $v\mapsto b\in S_o(u)$. By the definition of $\beta$ reduction, $p^{\prime }={\uparrow }_0^{-1}[0\mapsto {\uparrow }_0^1{v}^{\prime }]b^{\prime }\in [[u\parallel u]]$ by consistency of $S_0$. hence selecting $p={\uparrow }_0^{-1}[0\mapsto {\uparrow }_0^1{v}^{\prime }]b^{\prime }$, we have $p^{\prime }⟶p$.
• The next case is $u=\lambda b$. By induction whenever $q^{\prime }\in [[I{\beta }^{\prime }(b)\parallel I{\beta }^{\prime }(b)]]$, we have $q\in [[b\parallel b]]$ such that $q^{\prime }⟶q$. Hence $\lambda q^{\prime }⟶\lambda q$. But $\lambda q\in [[\lambda b\parallel \lambda b]]=[[u\parallel u]]$. By definition any $p\in \lambda I{\beta }^{\prime }(b)$ is equal to $\lambda q^{\prime }$ for some $q^{\prime }\in [[I{\beta }^{\prime }(b)\parallel I{\beta }^{\prime }(b)]]$, completing this part.
• There will be two cases if $u=(fx)$.
  • one where $p^{\prime }\in [[(I{\beta }^{\prime }(f)x)\parallel (I{\beta }^{\prime }(f)x)]]$. In this case, $p^{\prime }=(p_1^{\prime }{p}_2^{\prime })$ where $p_1^{\prime }\in [[I{\beta }^{\prime }(f)\parallel I{\beta }^{\prime }(f)]],p_2^{\prime }\in [[x\parallel x]]$. By induction, there exists $p\in [[f\parallel f]]$ such that $p_1^{\prime }⟶p$. which means that $(p{p}_2^{\prime })\in [[(fx)\parallel (fx)]]$ and $(p_1^{\prime }{p}_2^{\prime })⟶(p{p}_2^{\prime })$
  • The other case where $p^{\prime }\in [[(fI{\beta }^{\prime }(x))\parallel (fI{\beta }^{\prime }(x))]]$ has a proof symmetric to the above case.
• Now, consider $u=\uplus V$. Take some $p^{\prime }\in [[I{\beta }^{\prime }(u^{\prime })\parallel I{\beta }^{\prime }(u^{\prime })]]$ for any $u^{\prime }\in V$. By induction, there exists $p\in [[u^{\prime }\parallel u^{\prime }]]$ such that $p^{\prime }⟶p$. but of course $p\in [[u\parallel u]]$, by def.
• The cases of primitive, index, and all lambda is vacuous.

$◻$

Theorem 4: Completeness of $I{\beta }^{\prime }$

Statement:
Let $p⟶p^{\prime }$ and $p^{\prime }\in [u]$. Then $p\in [I{\beta }^{\prime }(u)]$.

Proof:
We proceed by structural induction on $u$.

1. Base Case: $u=\uplus V$
   There exists a $v\in V$ such that $p^{\prime }\in [v]$. By induction on $v$, combined with the definition of $I{\beta }^{\prime }$, we have
   $p\in [I{\beta }^{\prime }(v)]\subseteq [I{\beta }^{\prime }(u)]$,
   which is what we needed to show.

2. Inductive Case: Assume $u\ne \uplus V$.

   From the definition of $p⟶p^{\prime }$, at least one of the following cases must hold:

   • Case 1: $p=(\lambda b^{\prime })v^{\prime }$ and $p^{\prime }={\uparrow }^{-1}[\mathrm{\$}0\mapsto {\uparrow }^1{v}^{\prime }]b^{\prime }$
     Since ${\uparrow }^{-1}[\mathrm{\$}0\mapsto {\uparrow }^1{v}^{\prime }]b^{\prime }\in [u]$, we can invoke the completeness of $S_n$ to construct a $(v\mapsto b)\in S_0(u)$ such that $v^{\prime }\in [v]$ and $b^{\prime }\in [b]$. Combining these facts with the definition of $I{\beta }^{\prime }$, we get:
     $p=(\lambda b^{\prime })v^{\prime }\in [(\lambda b)v]\subseteq [I{\beta }^{\prime }(u)]$.

   • Case 2: $p=\lambda b$ and $p^{\prime }=\lambda b^{\prime }$ where $b⟶b^{\prime }$
     Because $p^{\prime }=\lambda b^{\prime }\in [u]$ and by assumption $u\ne \uplus V$, we know that $u=\lambda v$ and $b^{\prime }\in [v]$. By induction, $b\in [I{\beta }^{\prime }(v)]$. Combining with the definition of $I{\beta }^{\prime }$, we get:
     $p=\lambda b\in [\lambda I{\beta }^{\prime }(v)]\subseteq [I{\beta }^{\prime }(u)]$.

   • Case 3: $p=(fx)$ and $p^{\prime }=(f{x}^{\prime })$ where $x⟶x^{\prime }$
     This case is symmetric to the previous case and follows a similar argument.

Theorem 5: Consistency and Completeness of $I{\beta }_n$

Statement:
Let $p$ and $p^{\prime }$ be programs. Then:
$p\underset{\le n\text{ times }}{\underbrace{⟶⟶⟶\cdots ⟶}}{p}^{\prime }$
if and only if $p\in [I{\beta }_n(p^{\prime })]$.

Proof:
We proceed by induction on $n$.

1. Base Case: $n=0$
   In this case, $[I{\beta }_n(p^{\prime })]=\{p^{\prime }\}$ and $p=p^{\prime }$. The theorem holds immediately.

2. Inductive Step: Assume $n>0$.
   If $p\underset{\le n\text{ times }}{⟶⟶⟶}{p}^{\prime }$, then there exists a $q$ such that
   $q\underset{\le n-1\text{ times }}{\underbrace{⟶\cdots ⟶}}{p}^{\prime }$.
   By induction on $n$, we have $q\in [I{\beta }_{n-1}(p^{\prime })]$. Combined with $p⟶q$, we can invoke the completeness of $I{\beta }^{\prime }$ to get:
   $p\in [I{\beta }^{\prime }(I{\beta }_{n-1}(p^{\prime }))]\subseteq [I{\beta }_n(p^{\prime })]$.

   Conversely, if $p\in [I{\beta }_n(p^{\prime })]$, by unrolling the definitions, $p$ reduces to $p^{\prime }$ in at most $n$ steps. This completes the proof.