Divergence, or Non-Termination

The Dv effect

The effect Dv (for divergence) is a primitive effect in F*. Computations in Dv may not terminate, even with infinite resources. In other words, computations in the Dv effect have the observational behavior of non-termination. For example, the following loop function has type unit -> Dv unit and it always diverges when called:

let rec loop (): Dv unit = loop ()

If we remove the Dv effect label annotation, then F* treats the function as total and will try to prove that the recursive call terminates, according to its usual termination checking rules, i.e., F* will attempt to prove () << () which fails, as expected.

Since the Dv effect admits divergence, F* essentially turns-off the termination checker when typechecking Dv computations. So the recursive loop () call does not require a decreasing termination metric.

Partial correctness semantics of Dv

The Tot effect in F* has a total correctness semantics. That is, if a term has type e:Tot t, then e terminates terminates and produces a value of type t.

Terms with type Dv t have a partial correctness semantics. That is, a term e:Dv t, e may either run forever, but if it terminates then the resulting value has type t.

Another perspective is that aside from disabling the termination checking features of F*, all other type-checking constraints are enforced on Dv term. This means that one can still give interesting sound, specifications to Dv programs, e.g., the type below proves that if the Collatz function terminates, then the last element of the sequence is 1.

let rec collatz_ends_in_one (n:pos)
  : Dv (l:list pos { Cons? l /\ last l == 1 })
  = if n = 1 then [n]
    else if n % 2 = 0
    then n::collatz_ends_in_one (n / 2)
    else n::collatz_ends_in_one (3 * n + 1)

If, for example, in the base case we were to return the empty list [] rather than [n], then F* would refuse to accept the program, since the program could terminate while returning a value that is not an element of the annotated return type.

Isolating Dv from the logical core

Since Dv terms need not terminate, a program that always loops forever can be given any return type. For instance, the program below has return type False:

let rec dv_false () : Dv False = dv_false()

Importantly, a term of type Dv False should not be confused as a proof of False, since that would lead immediately to unsoundness of F*’s logical core. In particular, it should be impossible to turn a e:Dv t into a term of type Tot t. This is achieved by F*’s effect system, which treats Tot as a sub-effect of Dv, i.e., Tot < Dv, in the effect order. As explained in earlier, this ensures that no Tot term can depend on a Dv term, maintaining soundness of the total correctness interpretation of Tot.

As an example, the following attempt to “cast” dv_false to Tot fails, as does trying to use dv_false to produce incorrect proofs of other types.

[@@expect_failure]
let tot_false : Tot False = dv_false()
[@@ expect_failure]
let bad_zero : Tot (y:int{y == 0}) = dv_false (); 1

While F* does not allow Tot computations to depend on Dv computations, going the other way is perfectly fine. Intuitively, always terminating computations are potentially non-terminating. We can think of it like a weakening of the specification:

let add_one (x:int) : int = x + 1
let add_one_div (x:int) : Dv int = add_one x

The effect system of F* automatically lifts Tot computations into Dv, meaning that Tot functions can be seamlessly used in Dv functions.

The weakening of Tot terms to other effects is so pervasive in F* that one hardly even thinks about it, e.g., in the collatz program, sub-terms like n / 2 are in Tot but are easily used within a computation in the Dv effect.

No extrinsic proofs for Dv computations

One important consequence of any effectful code, including Dv, being outside the logical core of F* is that it is not possible to do extrinsic proofs about effectful code. One cannot even state properties of Dv computations in specifications, since even specifications must be total. For example, even stating the following lemma is illegal:

[@@expect_failure]
val collatz_property (n:pos)
  : Lemma (Cons? (collatz n) /\ last (collatz n) = 1)

This is nonsensical in F* since writing Cons? (collatz n) supposes that collatz n is defined, whereas it might actually just loop forever.

The only way to state properties about divergent programs is to encode the property intrinsically in the computation type, as we saw above.

let last #a (l:list a { Cons? l }) : a = L.index l (L.length l - 1)
val collatz_ends_in_one (n:pos)
  : Dv (l:list pos { Cons? l /\ last l == 1 })

let rec collatz_spec (n:pos) (l:list pos)
  : Tot bool (decreases l) 
  = match l with
    | [] -> false
    | hd :: tl -> 
      hd = n && (
        if hd = 1 then tl = []
        else if n%2 = 0 then collatz_spec (n/2) tl
        else collatz_spec (3*n + 1) tl
      )
// collatz' may loop forever on some inputs
// but if it completes it always returns a valid
// Collatz sequence
let rec collatz' (n:pos)
  : Dv (l:list pos { collatz_spec n l } )
  = if n = 1 then [n]
    else if n % 2 = 0
    then n::collatz' (n / 2)
    else n::collatz' (3 * n + 1)

// here's another bogus implementation that always loops
let rec collatz'' (n:pos)
  : Dv (l:list pos { collatz_spec n l } )
  = collatz'' n

General Recursive Types and Impredicativity with Dv

Aside from disabling the decreases metric on recursive functions in Dv, F* also disables two other forms of termination checking on Dv computations.

Recall from a previous chapter that inductive type definitions are subject to the strict positivity condition, since non-positive definitions allow the definition of recursive types and non-terminating computations. However, since computations in the Dv effect are already allowed to loop forever, the strict positivity condition can be relaxed when Dv types are involved. For example, one can define this:

noeq
type nonpos =
  | NonPos : (nonpos -> Dv False) -> nonpos

let loop_nonpos' (f:nonpos) : Dv False =
   let NonPos g = f in g f 
   
let loop_nonpos () : Dv False  = loop_nonpos' (NonPos loop_nonpos')

The type nonpos is not strictly positive, since it appears to the left of an arrow in a field of one of its constructors. Indeed, usingn nonpos it is possible to define (without using let rec) an infinitely looping program loop_nonpos()—however, the type Dv False tells us that this program may loop forever, and the infinite loop is safely isolated from F*’s logical core.

The other place in F*’s type system where termination checking comes into play is in the universe levels. As we learned previously, the logical core of F* is organized into an infinite hierarchy with copies of the F* type system arranged in a tower of universes. This stratification is necessary to prevent inconsistencies within the logical core. However, terms in the Dv effect are outside the logical core and, as such, restrictions on the universe levels no longer apply. As the snippet below shows a total function returning a type in universe u#a resides in universe u#(a + 1). However, a Dv function returning a type in u#a is just in universe 0, since the only way to obtain the type dv_type returns is by incurring a Dv effect and moving outside F*’s logical core.

let tot_type : Type u#(a + 1) = unit -> Tot (Type u#a)
let dv_type : Type0 = unit -> Dv (Type u#a)

Top-level Effects

A top-level F* term is not meant to be effectful. If one defines the following term, F* accepts the term but raises a warning saying “Top-level let bindings must be total—this term may have effects”.

let inconsistent : False = loop_nonpos()

Top-level effects can be problematic for a few reasons:

1. The order of evaluation of the effects in top-level terms is undefined for programs with multiple modules—it depends on the order in which modules are loaded at runtime.

2. Top-level effects, particularly when divergence is involved, can render F*’s typechecking context inconsistent. For example, once inconsistent is defined, then any other assertion can be proven.

   let _  = let _ = FStar.Squash.return_squash inconsistent in
            assert false
   

Nevertheless, when used carefully, top-level effects can be useful, e.g., to initialize the state of a module, or to start the main function of a program. So, pay attention to the warning F* raises when you have a top-level effect and make sure you really know what you’re doing.

Example: Untyped Lambda Calculus

In this section, we put together the various things we’ve learned about Dv computations to define several variants of an untyped lambda calculus.

You can refer back to our prior development of the simply typed lambda calculus if you need some basic background on the lambda calculus.

let var = nat
type term = 
  | Var  : var -> term
  | Int  : int -> term
  | Lam  : term -> term
  | App  : term -> term -> term

let rec subst (x:var) (v:term) (t:term)
  : Tot term  (decreases t) = 
  match t with
  | Var y -> if x = y then v else t
  | Int _ -> t
  | Lam t -> Lam (subst (x + 1) v t)
  | App t0 t1 -> App (subst x v t0) (subst x v t1)

(* This interpreter can (intentionally) loop infinitely *)
let rec interpret (t:term)
  : Dv (option term)
  = match t with
    | Var _
    | Int _
    | Lam _ -> Some t
    | App t0 t1 ->
      let head = interpret t0 in
      match head with
      | None -> None
      | Some (Lam body) -> interpret (subst 0 t1 body)
      | _ -> None //type error, expected a function

(* (\x. x x) (\x. x x) *)
let loops () : Dv _ = interpret (App (Lam (App (Var 0) (Var 0)))
                                     (Lam (App (Var 0) (Var 0))))

let rec closed' (t:term) (offset:int) 
  : bool
  = match t with
    | Int _ -> true
    | Var i -> i <= offset
    | Lam t -> closed' t (offset + 1)
    | App t0 t1 -> closed' t0 offset && closed' t1 offset
let closed t = closed' t (-1)

let rec interpret (t:term { closed t })
  : Dv (option (t:term { closed t }))
  = match t with
    | Int _
    | Lam _ -> Some t
    | App t0 t1 ->
      let head = interpret t0 in
      match head with
      | None -> None
      | Some (Lam body) -> interpret (subst 0 t1 body)
      | _ -> None //type error, expected a function

module Part4.UTLCEx1

let var = nat
type term = 
  | Var  : var -> term
  | Int  : int -> term
  | Lam  : term -> term
  | App  : term -> term -> term

//SNIPPET_START: closed$
let rec closed' (t:term) (offset:int) 
  : bool
  = match t with
    | Int _ -> true
    | Var i -> i <= offset
    | Lam t -> closed' t (offset + 1)
    | App t0 t1 -> closed' t0 offset && closed' t1 offset
let closed t = closed' t (-1)
//SNIPPET_END: closed$

let rec closed'_weaken (t:term) (offset offset':int)
  : Lemma 
    (requires closed' t offset /\
              offset <= offset')
    (ensures closed' t offset')
  = match t with
    | Int _ -> ()
    | Var _ -> ()
    | Lam t -> closed'_weaken t (offset + 1) (offset' + 1)
    | App t0 t1 -> 
      closed'_weaken t0 offset offset';
      closed'_weaken t1 offset offset' 

let rec subst (x:var) 
              (v:term { closed v })
              (t:term { closed' t x })
  : Tot (t1:term { closed' t1 (x - 1) }) (decreases t) = 
  match t with
  | Var y -> if x = y then (closed'_weaken v (-1) (x - 1); v) else t
  | Int _ -> t
  | Lam t -> Lam (subst (x + 1) v t)
  | App t0 t1 -> App (subst x v t0) (subst x v t1)

//SNIPPET_START: interpret$
let rec interpret (t:term { closed t })
  : Dv (option (t:term { closed t }))
  = match t with
    | Int _
    | Lam _ -> Some t
    | App t0 t1 ->
      let head = interpret t0 in
      match head with
      | None -> None
      | Some (Lam body) -> interpret (subst 0 t1 body)
      | _ -> None //type error, expected a function
//SNIPPET_END: interpret$

noeq
type dyn = 
  | DErr  : string -> dyn
  | DInt  : int -> dyn
  | DFun  : (dyn -> Dv dyn) -> dyn

let ctx_t = nat -> dyn

let shift (ctx:ctx_t) (v:dyn) 
  : ctx_t
  = fun n -> if n = 0 then v else ctx (n - 1)

let rec denote (t:term) (ctx:ctx_t)
  : Dv dyn 
  = match t with
    | Var v -> ctx v
    | Int i -> DInt i
    | Lam t -> DFun (fun v -> denote t (shift ctx v))
    | App t0 t1 -> 
      match denote t0 ctx with
      | DFun f -> f (denote t1 ctx)
      | DErr msg -> DErr msg
      | DInt _ -> DErr "Cannot apply an integer"

let ctx_t (i:int) = x:nat{x <= i} -> dyn

let max (x y:int) : int = if x < y then y else x
let rec free (t:term)
  : int
  = match t with
    | Var x -> x
    | Int _ -> -1
    | Lam t -> free t - 1
    | App t0 t1 -> max (free t0) (free t1)

val denote (t:term) (ctx:ctx_t (free t))
  : Dv dyn

let empty_context : ctx_t (-1) = fun _ -> false_elim ()

module Part4.UTLCEx2
let var = nat
type term = 
  | Var  : var -> term
  | Int  : int -> term
  | Lam  : term -> term
  | App  : term -> term -> term

//SNIPPET_START: free$
let max (x y:int) : int = if x < y then y else x
let rec free (t:term)
  : int
  = match t with
    | Var x -> x
    | Int _ -> -1
    | Lam t -> free t - 1
    | App t0 t1 -> max (free t0) (free t1)
//SNIPPET_END: free$

noeq
type dyn = 
  | DErr  : string -> dyn
  | DInt  : int -> dyn
  | DFun  : (dyn -> Dv dyn) -> dyn

//SNIPPET_START: ctx_t$
let ctx_t (i:int) = x:nat{x <= i} -> dyn
//SNIPPET_END: ctx_t$

let shift #i (ctx:ctx_t i) (v:dyn) 
  : ctx_t (i + 1)
  = fun n -> if n = 0 then v else ctx (n - 1)

(* This is similar to the interpreter, but
   "interprets" terms into the F* type dyn
    rather than just reducing syntax to syntax *)
let rec denote (t:term)
               (ctx:ctx_t (free t))
  : Dv dyn 
  = match t with
    | Var v -> ctx v
    | Int i -> DInt i
    | Lam t -> DFun (fun v -> denote t (shift ctx v))
    | App t0 t1 -> 
      match denote t0 ctx with
      | DFun f -> f (denote t1 ctx)
      | DErr msg -> DErr msg
      | DInt _ -> DErr "Cannot apply an integer"

//SNIPPET_START: empty_context$
let empty_context : ctx_t (-1) = fun _ -> false_elim ()
//SNIPPET_END: empty_context$

let closed t = free t = -1
let denote_closed (t:term { closed t }) 
  : Dv dyn
  = denote t empty_context

(* Lifting operations on integers to operations on dyn *)
let lift (op: int -> int -> int) (n m:dyn) : dyn
  = match n, m with
    | DInt i, DInt j -> DInt (op i j)
    | _ -> DErr "Expected integers"
let mul = lift op_Multiply
let sub = lift op_Subtraction
let add = lift op_Addition
let div (n m:dyn)
  = match n, m with
    | DInt i, DInt j -> 
      if j = 0 then DErr "Division by zero"
      else DInt (i / j)
    | _ -> DErr "Expected integers"
let mod (n m:dyn)
  = match n, m with
    | DInt i, DInt j -> 
      if j = 0 then DErr "Division by zero"
      else DInt (i % j)
    | _ -> DErr "Expected integers"

(* Branching *)
let if_ (d:dyn) (then_ else_:dyn) =
  match d with
  | DInt b -> 
    if b<>0 then then_ else else_
  | _ -> DErr "Can only branch on integers"

(* comparison *)
let eq_ (d:dyn) (d':dyn)
  : dyn 
  = match d, d' with
    | DInt i, DInt j -> DInt (if i = j then 1 else 0)
    | _ -> DErr "Can only compare integers"

(* Dynamically typed application *)
let app (f:dyn) (x:dyn)
  : Dv dyn
  = match f with
    | DFun f -> f x
    | _ -> DErr "Can only apply a function"
(* general recursion *)
let rec fix (f: (dyn -> Dv dyn) -> dyn -> Dv dyn) (n:dyn)
  : Dv dyn
  = f (fix f) n

let rec fix_alt (f: (dyn -> Dv dyn) -> dyn -> Dv dyn) 
  : Dv (dyn -> Dv dyn)
  = f (fix_alt f)

(* shorthands *)
let i (i:int) : dyn = DInt i
let lam (f:dyn -> Dv dyn) : dyn = DFun f
(* a dynamically typed analog of collatz *)
let collatz_dyn 
  : dyn 
  = lam (fix (fun collatz n ->
                if_ (eq_ n (i 1))
                    (i 1)
                    (if_ (eq_ (mod n (i 2)) (i 0))
                         (collatz (div n (i 2)))
                         (collatz (add (mul n (i 3)) (i 1))))))