# 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:

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.

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.