Refocusing (semantics)

The semantics of a programming language defines the meaning of the programs written in this programming language. Plotkin's Structural Operational Semantics is small-step semantics where the meaning of a program is defined step by step, where each step is an elementary operation that is carried out with contraction rules.

For example, consider the following minimalistic language of arithmetic expressions over integers with additions and quotients, in the manner of Hutton's razor.

In OCaml:

type operator = Add | Quo;;

type expression = Lit of int | Opr of expression * operator * expression;;

type value = Int of int;;

let expression_of_value (v : value) : expression = match v with Int n -> Lit n;;

The smallest potentially reducible expressions (potential redexes) are operations over values, and they are carried out with a contraction function that maps an actual redex to an expression and otherwise yields an error message:

type potential_redex = PR of value * operator * value;;

type contractum_or_error = Contractum of expression | Error of string;;

let contract (pr : potential_redex) : contractum_or_error =
  match pr with
    PR (Int n1, Add, Int n2) ->
     Contractum (Lit (n1 + n2))
  | PR (Int n1, Quo, Int n2) ->
     if n2 = 0
     then Error (string_of_int n1 ^ " / 0")
     else Contractum (Lit (n1 / n2));;

The addition of two integers is an actual redex, and so is the quotient of an integer and a nonzero integer. So for example, the expression Opr (Opr (Lit 1, Add, Lit 10), Add, Lit 100), i.e., $(1+10)+100$, reduces to Opr (Lit 11, Add, Lit 100), i.e., $11+100$, and the expression Opr (Opr (Lit 1, Quo, Lit 0), Add, Lit 100), i.e., $(1/0)+100$, reduces to Wrong "1 / 0".

Say that the reduction strategy is leftmost-innermost (i.e., depth first and left to right). The following one-step reduction function implements this strategy:

let rec reduce_d (e : expression) : value_or_expression_or_stuck =
  match e with
    Lit n ->
     Value (Int n)
  | Opr (e1, opr, e2) ->
     match reduce_d e1 with
       Value v1 ->
        (match reduce_d e2 with
           Value v2 ->
            (match contract (PR (v1, opr, v2)) with
               Contractum e ->
                Expression e
             | Error s ->
                Stuck s)
         | Expression e2' ->
            Expression (Opr (expression_of_value v1, opr, e2'))
         | Stuck s ->
            Stuck s)
     | Expression e1' ->
        Expression (Opr (e1', opr, e2))
     | Stuck s ->
        Stuck s;;

In words:

• a literal reduces to a value;
• if the expression e1 is stuck, then so is the expression Opr e1 opr e2, for any expression e2;
• if the expression e1 reduces to an expression e1', then for any expression e2, Opr e1 opr e2 reduces to Opr e1' opr e2;
• if the expression e1 reduces to a value v1, then
  • if the expression e2 is stuck, then so is the expression Opr e1 opr e2;
  • if the expression e2 reduces to an expression e2', then Opr e1 opr e2 reduces to Opr e1 opr e2';
  • if the expression e2 reduces to a value v2, then Opr e1 opr e2 is a potential redex:
    • if this potential redex is an actual one, then contracting it yields an expression; Opr e1 opr e2 reduces to this expression;
    • if this potential redex is not an actual one, then Opr e1 opr e2 is stuck.

Evaluation is achieved by iterated reduction. It yields either a value or an error message:

type result = Normal_form of value | Wrong of string;;

let rec normalize_d (e : expression) : result =
  match reduce_d e with
    Value v ->
     Normal_form v
  | Expression e' ->
     normalize_d e'
  | Stuck s ->
     Wrong s;;

This one-step reduction function implements a Structural Operational Semantics for this language of arithmetic expressions. For example, to carry the reduction step $(1-(5+5))-(2-20)\longrightarrow (1-10)-(2-20)$ the reduction function implicitly constructs the following proof tree:

                    -----------
                    5 + 5 -> 10
              ---------------------
              1 - (5 + 5) -> 1 - 10
 -----------------------------------------------
 (1 - (5 + 5)) - (2 - 20) -> (1 - 10) - (2 - 20)

Reformatting this proof tree to emphasize the implicit decomposition yields:

                  -------------------------------------------------->
                ^                 contraction                         |
                |        -----------------------------                |
                |        5 + 5               ->      10               |
    implicit    |    ----------------------------------               | implicit
  decomposition |    1 - (5 + 5)             ->  1 - 10               | recomposition
                |   -----------------------------------------------   |
                |   (1 - (5 + 5)) - (2 - 20) -> (1 - 10) - (2 - 20)   v

A reduction semantics is a small-step operational semantics where the implicit context of a potential redex is made explicit. So one reduction step gives rise to

1. constructing the context of the redex,
2. contracting this redex, and
3. recomposing the context around the contractum to yield the reduct:

  (1 - (5 + 5)) - (2 - 20)  \
 [(1 - (5 + 5)) - (2 - 20)] | explicit
 [[1 - (5 + 5)] - (2 - 20)] | decomposition
 [[1 - [5 + 5]] - (2 - 20)] /
                              contraction
 [[1 - [ 10  ]] - (2 - 20)] \
 [[1 -   10   ] - (2 - 20)] | explicit
 [(1 -   10   ) - (2 - 20)] | recomposition
  (1 -   10   ) - (2 - 20)  /

And pictorially, an arithmetic expression is evaluated in successive steps:

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

Transforming the one-step reduction function in Continuation-passing style, delimiting the continuation from type value_or_expression_or_stuck -> 'a to type value_or_expression_or_stuck -> value_or_expression_or_stuck, and splitting this delimited continuation into two (one to continue the decomposition and one to recompose) makes it simple to implement the corresponding normalization function:

type value_or_decomposition_cc =
  Val_cc of value
| Dec_cc of potential_redex * (value -> value_or_decomposition_cc) * (expression -> expression);;

let rec decompose_expression_cc (e : expression) (kd : value -> value_or_decomposition_cc) (kr : expression -> expression) : value_or_decomposition_cc =
  match e with
    Lit n ->
     kd (Int n)
  | Opr (e1, opr, e2) ->
     decompose_expression_cc
       e1
       (fun v1 ->
         decompose_expression_cc
           e2
           (fun v2 ->
             Dec_cc (PR (v1, opr, v2), kd, kr))
           (fun e2' ->
             kr (Opr (expression_of_value v1, opr, e2'))))
       (fun e1' ->
         kr (Opr (e1', opr, e2)));;

let decompose_cc (e : expression) : value_or_decomposition_cc =
  decompose_expression_cc e (fun v -> Val_cc v) (fun e' -> e');;

let rec iterate_cc_rb (vod : value_or_decomposition_cc) : result =
  match vod with
    Val_cc v ->
     Normal_form v
  | Dec_cc (pr, kd, kr) ->
     (match contract pr with
        Contractum e ->
         iterate_cc_rb (decompose_cc (kr e))
      | Error s ->     (*^^^^^^^^^^^^^^^^^*)
         Wrong s);;

let normalize_cc_rb (e : expression) : result =
  iterate_cc_rb (decompose_cc e);;

In the underlined code, the contractum is recomposed and the result is decomposed. This normalization function is said to be reduction-based because it enumerates all the reducts in the reduction sequence.

Refocusing

Extensionally, the refocusing thesis is that there is no need to reconstruct the next reduct in order to decompose it in the next reduction step. In other words, these intermediate reducts can be deforested.

Pictorially:

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

Intensionally, the refocusing thesis is that this deforestation is achieved by continuing the decomposition over the contractum in the current context.

let rec iterate_cc_rf (vod : value_or_decomposition_cc) : result =
  match vod with
    Val_cc v ->
     Normal_form v
  | Dec_cc (pr, kd, kr) ->
     (match contract pr with
        Contractum e ->
         iterate_cc_rb (decompose_expression_cc e kd kr)
      | Error s ->     (*^^^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
         Wrong s);;

let normalize_cc_rf (e : expression) : result =
  iterate_cc_rf (decompose_cc e);;

In the underlined code, the decomposition is continued. This normalization function is said to be reduction-free because it enumerates none of the reducts in the reduction sequence.

In practice, the two continuations are defunctionalized into traditional first-order, inside-out contexts, which yields an implementation of Felleisen and Hieb's reduction semantics, a small-step semantics that was designed independently of continuations and defunctionalization.

Applications

The construction sketched above is completely formalized using the Coq Proof Assistant.

Over the years, this construction has been used to inter-derive calculi and abstract machines. Besides the CEK Machine, the Krivine machine, and the SECD machine, examples also include the chemical abstract machine and abstract machines for JavaScript. Bach Poulsen and Mosses have also used refocusing to implement Structural Operational Semantics and Modular Structural Operational Semantics.

More broadly, refocusing has been used to derive type systems and implementations for coroutines, to go from type checking via reduction to type checking via evaluation, to derive a classical call-by-need sequent calculus, to derive interpretations of the gradually-typed lambda calculus, and for full reduction.

Correctness

Danvy and Nielsen stated conditions for refocusing, and proved them informally. Sieczkowski, Biernacka, and Biernacki formalized refocusing using the Coq Proof Assistant. Bach Poulsen proved the correctness of refocusing for XSOS using rule induction. Biernacka, Charatonik, and Zielinska generalized refocusing using the Coq Proof Assistant. Using Agda, Swiestra proved the refocusing step as part of his formalization of the syntactic correspondence between the $\lambda {\widehat {\rho }}$ calculus with a normal-order reduction strategy and the Krivine machine. Also using Agda, Rozowski proved the refocusing step as part of his formalization of the syntactic correspondence between the $\lambda {\widehat {\rho }}$ calculus with an applicative-order reduction strategy and the CEK Machine.