Note: it is usually not possible to prove $RC$ directly: cannot do induction on typing derivation of the closed term because typing contexts will be non-empty for sub-terms.
$\Gamma \vdash t \leq t' : \tau$ (logical approximation)
$RC$ can be generalised to open terms $\Gamma \vdash t : \tau$ and $\Gamma \vdash t' : \tau$: given two suitable* closing substitutions $\gamma$ and $\gamma'$ we require that $RC\tau(\gamma(t), \gamma(t'))$
* suitable means that if $\gamma(x) = t$ and $\gamma'(x) = t'$, then $RC_\tau(t, t')$ (given $\Gamma(x) = \tau$)
$\Gamma \vdash t \leq_\text{ctx} t' : \tau$ (contextual approximation)
For all one-hole contexts $C$, termination behaviour is preserved, i.e. $C[t] \Downarrow ~ \Rightarrow ~ C[t'] \Downarrow$. Logical approximation implies contextual approximation.
$\approx$ and $\approx_{\text{ctx}} $(Logical/contextual equivalence)
Symmetric closure of $\leq$ and $\leq_{\text{ctx}}$ respectively.
Consequences
Closed terms, base type
$RC_{Bool}(t, t')$ implies that $t \Downarrow v \Rightarrow t' \Downarrow v$
Closed terms, function type
Consider two terms $f, g$ of type $\tau_1 \to ... \to \taun \to Bool$. Then $RC{\tau_1 \to ... \to \tau_n \to Bool}(f, g)$ implies
f ~ t_1 \dots t_n \Downarrow r ~ \Rightarrow ~ g ~ t_1 \dots t_n \Downarrow r
(i.e. an extensional equality). This is a suitable definition for plutus validators.
$[\texttt{let} ~ x = t] \vdash x \triangleright t$
$x$ and $t$ are not contextually equivalent, only in contexts that have let x = t!
A possible solution: use a more general definition than $\leq$. For a substitution to be "suitable", any let-bound variable x can only be replaced by its definition (i.e. agree with the environment of the translation relation).
(disclaimer: simplified definitions (STLC instead of PIR), the concepts should transfer to PIR)
Notions
$RC_\tau(t, t')$ (Related computations)
Relating closed terms. $RC$ = Related Computations $RV$ = Related Values
Note: it is usually not possible to prove $RC$ directly: cannot do induction on typing derivation of the closed term because typing contexts will be non-empty for sub-terms.
$\Gamma \vdash t \leq t' : \tau$ (logical approximation)
$RC$ can be generalised to open terms $\Gamma \vdash t : \tau$ and $\Gamma \vdash t' : \tau$: given two suitable* closing substitutions $\gamma$ and $\gamma'$ we require that $RC\tau(\gamma(t), \gamma(t'))$
* suitable means that if $\gamma(x) = t$ and $\gamma'(x) = t'$, then $RC_\tau(t, t')$ (given $\Gamma(x) = \tau$)
$\Gamma \vdash t \leq_\text{ctx} t' : \tau$ (contextual approximation)
For all one-hole contexts $C$, termination behaviour is preserved, i.e. $C[t] \Downarrow ~ \Rightarrow ~ C[t'] \Downarrow$. Logical approximation implies contextual approximation.
$\approx$ and $\approx_{\text{ctx}} $(Logical/contextual equivalence)
Symmetric closure of $\leq$ and $\leq_{\text{ctx}}$ respectively.
Consequences
Closed terms, base type
$RC_{Bool}(t, t')$ implies that $t \Downarrow v \Rightarrow t' \Downarrow v$
Closed terms, function type
Consider two terms $f, g$ of type $\tau_1 \to ... \to \taun \to Bool$. Then $RC{\tau_1 \to ... \to \tau_n \to Bool}(f, g)$ implies
(i.e. an extensional equality). This is a suitable definition for plutus validators.
What implies what?
$\leq ~ \Rightarrow ~\leq_{ctx}$ $\leq ~ \Rightarrow ~RC$
For dead-code, let-desugaring $\triangleright ~ \Rightarrow ~ \leq ~ \Rightarrow ~ RC ~ \Rightarrow ~ \text{extensional equality}$
For inlining:
$\triangleright ~ \not\Rightarrow ~ \leq$
Why not inlining?
For inlining, $\leq$ cannot be proven:
$[\texttt{let} ~ x = t] \vdash x \triangleright t$
$x$ and $t$ are not contextually equivalent, only in contexts that have
let x = t!A possible solution: use a more general definition than $\leq$. For a substitution to be "suitable", any let-bound variable x can only be replaced by its definition (i.e. agree with the environment of the translation relation).