Refocusing (semantics)

This article is an orphan, as no other articles link to it. Please introduce links to this page from related articles; try the Find link tool for suggestions. (March 2024)

In computer science, refocusing is a program transformation used to implement a reduction semantics—i.e., a small-step operational semantics with an explicit representation of the reduction context—more efficiently. It is a step towards implementing a deterministic semantics as a deterministic abstract machine.

A small-step operational semantics defines the meaning of a given program ${\displaystyle p_{0}}$ as a sequence of one-step reductions that starts with ${\displaystyle p_{0}}$ and continues with a sequence of reducts ${\displaystyle p_{i}}$, where ${\displaystyle i>0}$:

${\displaystyle p_{0}\rightarrow p_{1}\rightarrow p_{2}\rightarrow \cdots }$

A one-step reduction from ${\displaystyle p_{n}}$ to ${\displaystyle p_{n+1}}$ is achieved by

1. locating the smallest potentially reducible term (potential redex) using a given reduction strategy, if this potential redex exists in ${\displaystyle p_{n}}$ (otherwise ${\displaystyle p_{n}}$ is irreducible); and
2. contracting this potential redex using given contraction rules if it is an actual one (otherwise ${\displaystyle p_{n}}$ is stuck).

A reduction semantics is a small-step operational semantics with an explicit representation of the context of each potential redex.

Writing ${\displaystyle C}$ for such context, the sequence of one-step reductions above reads:

${\displaystyle p_{0}=C_{0}[{\mathit {pr}}_{0}]\rightarrow C_{0}[c_{0}]=C_{1}[{\mathit {pr}}_{1}]\rightarrow C_{1}[c_{1}]=C_{2}[{\mathit {pr}}_{2}]\rightarrow C_{2}[c_{2}]\rightarrow \cdots }$

where

1. ${\displaystyle p_{0}}$ is first decomposed into the context ${\displaystyle C_{0}}$ and a potential redex ${\displaystyle {\mathit {pr}}_{0}}$,
2. ${\displaystyle {\mathit {pr}}_{0}}$ is contracted into the contractum ${\displaystyle c_{0}}$,
3. ${\displaystyle C_{0}}$ is then recomposed around ${\displaystyle c_{0}}$ and then decomposed into the context ${\displaystyle C_{1}}$ and a potential redex ${\displaystyle {\mathit {pr}}_{1}}$,
4. etc.

This succession of decompositions, contractions, and recomposition is depicted as follows:

         contract               contract               contract        
       o--------->o           o--------->o           o--------->o      
      /            \         /            \         /            \     
     /    recompose \       /    recompose \       /    recompose \    
    /                \     /                \     /                \   
   / decompose        \   / decompose        \   / decompose        \  
  /                    \ /                    \ /                    \ 
 o--------------------->o--------------------->o--------------------->o
          reduce                 reduce                 reduce        

Refocusing is a deforestation of the successive reducts:^[1][2]

         contract    refocus    contract    refocus    contract        
       o--------->o---------->o--------->o---------->o--------->o------
      /            \         /            \         /            \     
     /    recompose \       /    recompose \       /    recompose \    
    /                \     /                \     /                \   
   / decompose        \   / decompose        \   / decompose        \  
  /                    \ /                    \ /                    \ 
 o                      o                      o                      o

After the initial decomposition, the succession of contractions and refocusings has the structure of a deterministic abstract machine.