Divergence, or Non-Termination

Most dependently typed languages are not Turing complete. This is because, as explained earlier, it is crucial to the soundness of a type theory to have all functions terminate. This means that you cannot program, say, an interpreter for a general-purpose programming language in a language like Coq, since such an interpreter would not be able to handle programs that intentionally loop forever. [1]

F*’s logical core of total (and ghost) functions can only express terminating computations. However, F*’s also allows expressing non-terminating or divergent computations, relying on the effect system to isolate divergent computations from the logical core. In particular, the computation type Dv t describes a computation that may loop forever, but if it completes, it returns a value of type t.

Relying on the effect system as a dependency tracking mechanism, F* ensures that Tot computations cannot rely on Dv computations by placing Dv above Tot in the effect hierarchy, while, conversely, a total computation Tot t can be silently promoted to Dv t, the type of computations that may not terminate, i.e., Tot < Dv in the effect partial order.

Recursive functions that return computations in the Dv effect are not checked for termination. As such, using the Dv effect, one can write programs such as the one below, which computes Collatz sequences—whether or not this program terminates for all inputs is an open problem.

(* You can program a function to compute Collatz sequences
   ... though no one knows if it actually terminates for all n *)
let rec collatz (n:pos)
  : Dv (list pos)
  = if n = 1 then [n]
    else if n % 2 = 0
    then n::collatz (n / 2)
    else n::collatz (3 * n + 1)

In this chapter, we’ll look in detail at the Dv effect and how it interacts with other features of the language, including the other effects, recursive type definitions, and the styles of programming and proving it enables.

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 })

Exercise

Define a predicate collatz_spec (n:pos) (l:list pos) : bool that decides if l is a valid Collatz sequence starting at n.

Implement val collatz' (n:pos) : Dv (l:list pos { collatz_spec n l }).

What does this type mean? Are there other ways to implement collatz' with the same type?

Answer

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.

Interpreting Deeply Embedded Lambda Terms

We start by defining the syntax of untyped lambda terms, below. The variables use the de Bruijn convention, where a index of a variable counts the number of lambda-binders to traverse to reach its binding occurrence. The Lam case just has the body of the lambda term, with no type annotation on the binder, and no explicit name for the variable.

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

As usual, we can define what it means to substitute a variable x with a (closed) term v in t—this is just a regular Tot function.

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)

Finally, we can define an interpreter for term, which can (intentionally) loop infinitely, as is clear from the Dv type annotation.

(* 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))))

Exercise

This exercise is designed to show how you can prove non-trivial properties of Dv computations by giving them interesting dependent types.

The substitution function defined here is only sound when the term being substituted is closed, otherwise, any free variables it has can be captured when substituted beneath a lambda.

A term is closed if it satisfies this definition:

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)

Restrict the type of subst so that its argument is v : term { closed v }—you will have to also revise the type of its other argument for the proof to work.

Next, give the following type to the interpreter itself, proving that interpreting closed terms produces closed terms, or loops forever.

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

Answer

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$

Denoting Lambda Terms into an F* Recursive Type

We now look at a variation on the interpreter above to illustrate how (non-positive) recursive types using Dv can also be used to give a semantics to untyped lambda terms.

Consider the type dyn shown below—it has a non-positive constructor DFun. We can use this type to interpret untyped lambda terms into dynamically typed, potentially divergent, F* terms, showing, in a way, that untyped lambda calculus is no more expressive than F* with the Dv effect.

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

The program denote shown below gives a semantics to term using dyn. It is parameterized by a ctx : ctx_t, which interprets the free variables of the term into 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"

We look at the cases in detail:

  • In the Var case, the intepretation just refers to the context.

  • Integers constants in term are directly interpreted to integers in dyn.

  • The case of Lam is the most interesting: An lambda abstraction in term is interpreted as an F* function dyn -> Dv dyn, recursively calling the denotation function on the body when the function is applied. Here’s where we see the non-positivity of DFun at play—it allows us to inject the function into the dyn type.

  • Finally, in the application case, we interpret a syntactic application in term as function application in F* (unless the head is not a function, in which case we have a type error).

Exercise

This exercise is similar in spirit to the previous one and designed to show that you can prove some simple properties of denote by enriching its type.

Can you prove that a closed term can be interpreted in an empty context?

First, let’s refine the type of contexts so that it only provides an interpretation to only some variables:

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

Next, let’s define free t to compute the greatest index of a free variable in a term.

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)

Can you give the same denote function shown earlier the following type?

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

Next, define the empty context as shown below:

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

Given a closed term t : term { closed t }, where closed t = (free t = -1), can you use denote to give an interpretation to closed terms in the empty context?

Answer

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

Shallowly Embedded Dynamically Typed Programming

In the previous example, we saw how the syntax of untyped lambda terms can be interpreted into the F* type dyn. In this example, rather than going via the indirection of the syntax of lambda terms, we show how the type dyn can be used directly to embed within F* a small Turing complete, dynamically typed programming language.

We can start by lifting the F* operations on integers and functions to (possibly failing) operations on dyn.

(* 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"

We also encode provide operations to compare dyn-typed integers and to branch on them, treating 0 as false.

(* 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"

For functions, we can provide combinators to apply functions and, importantly, a combinator fix that provides general recursion.

(* 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

An aside on the arity of recursive functions: You may wonder why fix is defined as shown, rather than fix_alt below, which removes a needless additional abstraction. The reason is that with fix_alt, to instruct F* to disable the termination checker on the recursive definition, we need an additional Dv annotation: indeed, evaluating fixalt f in a call-by-value semantics would result, unconditionally, in an infinite loop, whereas fix f would immediately return the lambda term fun n -> f (fix f) n. In other words, eta reduction (or removing redundant function applications) does not preserve semantics in the presence of divergence.

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

With that, we can program non-trivial dynamically typed, general recursive programs within F* itself, as seen below.

(* 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))))))

All of which is to illustrate that with general recursion and non-positive datatypes using Dv, F* is a general-purpose programming language like ML, Haskell, Lisp, or Scheme, or other functional languages you may be familiar with.