Beluga Manual

Beluga contains two languages, one above the other, with a narrow and precisely specified interface between them. Most of what a newcomer finds difficult concerns that interface. This book therefore begins by naming the two languages and fixing the vocabulary, and it keeps the distinction explicit thereafter.

The order of presentation is strictly bottom-up: nothing is used before it has been defined. §0, which may be skipped, reads inference rules, the notation in which formal systems are defined. §1 states the problem Beluga addresses and sets out the shape of the system. §2–§5 introduce both levels on a language in which no variable is bound, the arithmetic expressions of Pierce's Types and Programming Languages, since that is where a reader coming from ML or Haskell has solid ground. §6 and §7 introduce binders. §8–§13 develop contexts, which carry most of the content. §14–§19 complete the upper language. §20 treats totality, §21 the interactive prover, and §22–§29 give complete developments. §30 teaches Beluga's error messages, §31 collects practical advice, and §32 onward is reference.

§0Reading inference rules#

Beluga is a language for reasoning about formal systems, and formal systems are defined by inference rules. This section explains how such rules are read, in paper notation and without any Beluga; a reader who has taken a course on programming languages will have met all of it and can go straight to Part one.

§0.1 · Judgments

A formal system is defined by saying which assertions of certain forms hold. The forms are called judgments. The running example of Part two is a small language of booleans and natural numbers, taken from Pierce's Types and Programming Languages, whose terms M and types T are these.

M  ::=  tt | ff | ite M M M | z | succ M | pred M | iszero M
T  ::=  nat | bool

ite M₁ M₂ M₃ is the conditional, if M₁ then M₂ else M₃; z is zero and succ M the successor of M. The names are the ones the language receives in Beluga in §2.2. Two judgments are defined over it: M : T, read M has type T, and M ⟶ M′, read M steps to M′. This section uses the first.

The terms belong to the object language, the language under study. The rules that follow are written in a second language, ordinary mathematical notation, which talks about the first; it is the metalanguage. §2.2 returns to the distinction when LF takes over as the metalanguage.

§0.2 · Rules

An inference rule has premises above a horizontal line and a single conclusion below it, with the rule's name beside the line. It states that whenever every premise holds, the conclusion holds. A rule with no premises is an axiom: its conclusion holds outright. These seven rules define the typing judgment.

The letters M, M₁ and T in a rule are schematic variables. A rule stands for each of its instances, the rules obtained by replacing every schematic variable with a term or a type, the same one at each of its occurrences. t_succ is in this sense infinitely many rules, among them one whose premise is z : nat and whose conclusion is succ z : nat. The proviso about occurrences carries meaning: in t_ite the T of the second premise, of the third and of the conclusion is one type, which is how the rule says that both branches have the type of the whole. The word metavariable, sometimes used for these, is reserved in this book for something else, defined in §1.4.

A rule can be read in two directions. Read downward, it builds: given derivations of its premises, it yields one of its conclusion. Read upward, it reduces a goal: to establish the conclusion, establish the premises. The meaning of a rule is the downward reading; the upward one is how a derivation is found, and §0.3 uses it.

§0.3 · Derivations

A derivation of a judgment is a tree of rule instances. Its root is the judgment, the premises of each instance are the conclusions of the instances immediately above it, and every leaf is an axiom. A judgment is derivable when it has a derivation. To find one for ite (iszero z) z (succ z) : nat, read the rules upward, starting from the goal.

1. The term is a conditional, and t_ite is the only rule whose conclusion concerns a conditional. Its instance with M₁ = iszero z, M₂ = z, M₃ = succ z and T = nat leaves three goals: iszero z : bool, z : nat and succ z : nat.
2. iszero z : bool can be concluded only by t_isz, which leaves z : nat.
3. z : nat is an instance of the axiom t_z, and needs nothing further.
4. succ z : nat can be concluded only by t_succ, which leaves z : nat once more.

At each step the form of the term chose the rule, because in this system exactly one rule concludes a typing judgment about each form of term. The same fact settles when there is no derivation. Consider succ tt : nat. The only rule that concludes a judgment of the form succ M : nat is t_succ, whose premise would be tt : nat; and the only rule that concludes anything about tt is t_tt, whose conclusion is tt : bool. No tree can be built: succ tt : nat is not derivable, which is what it means for succ tt to be ill-typed. An argument of this shape, from a judgment back to the rules that could have concluded it, is called inversion; in Beluga it is a pattern match on a derivation (§3.3).

§0.4 · Derivable and admissible rules

A new rule can be justified in two ways that look alike and are not.

A rule is derivable when a tree built from the existing rules leads from its premises to its conclusion. From M : nat, two instances of t_succ give succ (succ M) : nat.

A rule is admissible when its conclusion is derivable whenever its premises are, whether or not any tree connects them. From succ M : nat it follows that M : nat: a derivation of succ M : nat must end in t_succ, the only rule that concludes a judgment of that form, and the premise of that instance is a derivation of M : nat. The rule is admissible but not derivable. No tree leads from succ M : nat to M : nat, because every typing rule concludes about a term that contains the terms of its premises, so nothing below a leaf about succ M is about M alone. The argument works by examining the derivation of the premise, which a tree cannot do.

The difference shows when the system grows. Add an eighth rule, an axiom concluding succ tt : nat. The derivable rule survives, since its tree uses only t_succ. The admissible one fails: succ tt : nat is now derivable and tt : nat is not. Admissibility is a fact about the rules as they stand; derivability survives any addition.

The same distinction separates Beluga's two levels. A derivable rule is an open derivation, a tree whose leaves include its premises, unproved, and Beluga writes it as a term at the index level (§1.2, §8.2). An admissible rule needs an argument about every derivation of its premises, that is, a function from derivations to derivations, and Beluga writes it at the computation level as a total recursive program (§5.1).

§0.5 · Induction on derivations

Admissible rules, and theorems about a system in general, are proved by induction on derivations. A derivation is a finite tree, so a property holds of every derivation if it holds of a derivation whenever it holds of the derivations of its premises. A proof has one case for each rule that can end the derivation, and in each case the induction hypothesis applies to the subderivations, which are smaller than the whole.

Proof. By induction on a derivation D of M : T, showing for each rule that can end D that every derivation E of M : T′ has T′ = T.

• D ends in t_tt. Then M is tt, and the only rule concluding a typing judgment about tt is t_tt, so E ends in it as well and T = T′ = bool. The cases t_ff, t_z, t_succ, t_pred and t_isz are alike: the form of M fixes the rule that ends E, and the rule fixes the type.
• D ends in t_ite. Then M is ite M₁ M₂ M₃, and D contains a subderivation D₂ of M₂ : T. By inversion E ends in t_ite too, and so contains a subderivation E₂ of M₂ : T′. D₂ is smaller than D, so the induction hypothesis applies to D₂ and E₂ and gives T = T′. ∎

Here induction on the term M would have served as well, since each form of term has exactly one typing rule. Induction on derivations is the general method, and it is the one Beluga mechanizes: a proof by induction on a derivation is a recursive function over the term that represents the derivation, with one case for each rule (§5.1). §11.4 proves this theorem again, for a language with functions, in exactly that form.

§1.1The problem#

Consider a small programming language, given by a grammar, a set of typing rules, and a set of evaluation rules. The theorem one usually wants first is type safety, which Milner summed up in the slogan that well-typed programs cannot go wrong. On paper the proof occupies a few pages of structural induction. Checking the same proof by machine is far more work, and most of that work lies in material the informal proof never mentions.

The interesting part of the argument transfers to a proof assistant with little friction. The case analyses become case analyses; appeals to the induction hypothesis become recursive calls. What does not transfer is the material underneath. The object language has variables, so a representation must be chosen: concrete names, de Bruijn indices, or a nominal encoding, the three that §6.1 describes. The typing rules mention a context Γ of assumptions, so contexts must be represented and their properties established, among them weakening and exchange (an assumption may be added, or two reordered, without invalidating a derivation) and the uniqueness of a variable's assumption. The evaluation rules substitute, so substitution must be defined, shown to be capture-avoiding, and shown to commute with whatever it needs to commute with.

None of this is part of the theorem, yet all of it must be in place before the theorem can be stated. Berardi, writing about a mechanization of Girard's normalization proof, gave the standard description:

Berardi's image can be made quantitative. In published comparisons of strong-normalization proofs for the simply-typed lambda calculus, the Coq and Agda developments each require on the order of two hundred lines of renaming and substitution boilerplate before the proof proper begins, and the Agda version additionally rests on a generic-syntax library of some sixteen hundred lines. The proofs themselves are of comparable size across the systems; what differs is the material beneath them.

Beluga proceeds from the position that this infrastructure should be neither built nor imported nor reasoned about, but supplied by the language itself. Variables, scope, contexts, simultaneous substitution and its equational theory are primitive notions with their properties already established, and the programmer has no access to their implementation. The approach costs generality: Beluga is not a general-purpose proof assistant. It has no numbers, no strings, no input or output, no mutable state, no exceptions, and no polymorphism. The absence of polymorphism is a consequence of the foundation rather than a gap in the implementation; §14.5 gives the reason.

§1.2The two levels#

Beluga is a two-level system. The lower level is the logical framework LF, in which one writes down the object of study: its syntax, its judgments, its inference rules. The upper level is a dependently-typed functional language, in which one writes proofs about that object as programs. The two are separate languages with separate grammars, separate type systems, and separate notions of function.

Terminology for these two levels is not standardized in the literature, and a reader moving between papers will meet all of the following.

The terms used here are index level and computation level, with LF or contextual LF where precision about the framework itself is required. One further pair of terms must be settled now, since conflating the two is a frequent and costly error.

§1.3Signatures#

A Beluga file is a signature, conventionally carrying the extension .bel, and consists of a sequence of declarations processed in order. There are ten declaration forms, and they exhaust the top-level language. Each is developed in the section named.

Alongside these are the pragmas, each introduced by --, which adjust how a file is processed rather than adding to its content: operator declarations, coverage checking, name preferences, module imports, and logic-programming queries. §19 and §33.2 cover them.

§1.4Lexical conventions#

Three lexical facts carry meaning rather than style, and error messages are hard to read without them.

§1.4.1 · Case

The distribution's files, and this book, follow a convention of case. LF type families, constructors and bound variables, context variables and computation variables begin with a lower-case letter; metavariables, and computation-level types and their constructors, begin with a capital. The convention is not enforced. Beluga does not classify a name by its first letter: what a name denotes depends on where it is declared or bound. Four marks, by contrast, belong to the lexical syntax and do determine what the name after them is.

Since case is not checked, lam \X. X is accepted, and is the same term as lam \x. x. The convention is worth keeping all the same, because Beluga takes a name inside a box to be a metavariable when it is declared nowhere, whatever its spelling. A misspelt constant, such as t_zero for t_z, is therefore read as a metavariable, and the error reports an illegal free metavariable rather than an unknown constant (§30.3). Under the convention a lower-case metavariable is out of place, and the misspelling shows.

§1.4.2 · Terminators

The period and the semicolon are both terminators and they are not interchangeable. A period ends a single declaration written in the older Twelf notation, and ends a pragma. A semicolon ends a grouped declaration, meaning one written with = and a list of alternatives, and ends a rec, let, schema or module. The two listings below declare the same family.

LF tp : type =
| nat  : tp
| bool : tp
;

tp   : type.
nat  : tp.
bool : tp.

The grouped form is preferred because it records that nat and bool are the constructors of tp, information the typechecker uses. The family is the one §2.2 declares: the two types of the small language studied in Part two. A leading | before the first constructor is optional.

§1.4.3 · Comments

% introduces a line comment. %{ … }% delimits a comment that may span lines, and such comments nest. %{{ … }}% is a documentation comment, treated identically by the compiler but rendered as prose by Beluga's HTML mode, which is how the literate examples in the distribution are written.

§1.4.4 · Unicode alternatives

Several tokens have a Unicode spelling, and the two forms are interchangeable. Files in circulation mix them freely.

Greek letters are ordinary identifiers, so a declaration schema ctx = tm; may be followed by a binding (Γ : ctx). Much of the literature writes contexts as Γ, Ψ, Φ and substitutions as σ. In listings this book names contexts and substitutions with ASCII identifiers, as g and $s; in prose it uses the Greek letters.

§2Declaring data at the index level#

Before anything can be proved about a language, its syntax and its judgments must be written down. In Beluga that is the work of the index level. This section writes the arithmetic language there, the one §0.1 sets out on paper: first its syntax, as ordinary data, and then its numerals, values, evaluation and typing as families indexed by terms. The second step, indexing a family by terms, is what makes LF a logical framework rather than a language of datatypes.

§2.1 · Types and kinds

The index level has three strata, named as usual in type theory. Terms are classified by types, and types by kinds. There is a single base kind, written type, which is a keyword.

A declaration tp : type asserts that tp is a type. A declaration nat : tp asserts that nat is a term of type tp. No fourth stratum exists and there is no hierarchy of universes; type is where the tower terminates.

§2.2 · The LF declaration

A single declaration introduces a family together with all of its constructors, as an OCaml variant type is declared with its constructors. The family declared first is the syntax of a small language: the arithmetic expressions of the first chapters of Pierce's Types and Programming Languages, built from booleans, numerals and a conditional.

LF term : type =
| tt     : term
| ff     : term
| ite    : term -> term -> term -> term
| z      : term
| succ   : term -> term
| pred   : term -> term
| iszero : term -> term
;

The terms of type term are z, succ z, ite tt z (succ z), and so on. Application is written by juxtaposition and associates to the left, so that succ succ z is a type error, applying succ to two arguments, and the parentheses in succ (succ z) are required. Equally, succ tt is a term of type term, although it denotes nothing sensible: a syntax contains whatever its constructors build, and ruling out nonsense is the work of a type system, which §2.4 supplies.

A second family, also simple, gives the language its two types.

LF tp : type =
| nat  : tp
| bool : tp
;

nat and bool are types of the arithmetic language. To Beluga they are terms like any other, of type tp. That a type of one language is a term of another is the distinction between an object language, the language under study, and the language in which it is written down. Here the object language is the arithmetic expressions and the language describing them is LF. This book keeps the distinction explicit throughout.

§2.3 · Indexed families

Not every term is a numeral: succ (succ z) is one and succ tt is not, and two of the rules of evaluation in §2.4 apply to numerals alone. Saying which terms are numerals takes a type that depends on a term, and here the index level departs from an ordinary datatype language. A family may be indexed by terms, and the index's type is written to the left of the arrow in the kind. OCaml's generalized algebraic datatypes come closest, but they index types by types; here the index is a term.

LF numval : term -> type =
| nv_z : numval z
| nv_s : numval N -> numval (succ N)
;

Read the kind numval : term -> type as: for every term M of type term, numval M is a type. The constructor nv_z inhabits numval z alone. The constructor nv_s, given an inhabitant of numval N, yields one of numval (succ N). The index belongs to the type, so nv_s nv_z has type numval (succ z) and not numval z, and no term whatever has type numval tt, there being no constructor that could produce it.

An inhabitant of numval M is therefore not data in the ordinary sense. It is evidence that M has a property. The values of the language are defined from it.

LF value : term -> type =
| v_tt  : value tt
| v_ff  : value ff
| v_num : numval N -> value N
;

The capital N in the types of nv_s and v_num occurs free. §4.3 states what Beluga does with such an occurrence: it becomes an additional, hidden argument to the constructor. That mechanism is consequential enough to warrant a section of its own.

LF even : term -> type =
| ev_z  : even z
| ev_ss : even N -> even (succ (succ N))
;

§2.4 · Judgments as types#

The idea that makes LF a logical framework rather than a notation for describing data has already appeared: numval describes a property, and its terms are evidence. Taken in general, an indexed family may describe any relation of the object language, in which case its terms are derivations.

Take the small-step evaluation relation M ⟶ M′, read M steps to M′. It is given by inference rules, read as in §0, of which two suffice to show the pattern.

In LF the relation becomes a family indexed by two terms, with one constructor per rule. The premises of a rule become the arguments of the constructor; the conclusion becomes its result type. The whole relation is ten rules.

LF step : term -> term -> type =
| e_ite_tt : step (ite tt M2 M3) M2
| e_ite_ff : step (ite ff M2 M3) M3
| e_ite    : step M1 M1' ->
             % -------------------------------
             step (ite M1 M2 M3) (ite M1' M2 M3)
| e_succ   : step M M' -> step (succ M) (succ M')
| e_pred_z : step (pred z) z
| e_pred_s : numval N -> step (pred (succ N)) N
| e_pred   : step M M' -> step (pred M) (pred M')
| e_isz_z  : step (iszero z) tt
| e_isz_s  : numval N -> step (iszero (succ N)) ff
| e_isz    : step M M' -> step (iszero M) (iszero M')
;

Two of the rules, e_pred_s and e_isz_s, have a premise of a different judgment: numval N, which restricts them to numerals. A derivation of one judgment may therefore contain derivations of another. The derivation that succ (pred (succ z)) steps to succ z appears below with its term; hovering over either highlights the corresponding part of the other.

Observe what the type records. The term e_succ (e_pred_s nv_z) has type step (succ (pred (succ z))) (succ z) and no other. A term of a step type certifies one specific step.

The language's type system is a second judgment, M : T, declared the same way. Its rules are the familiar ones: the conditional requires a boolean guard and two branches of one type, and the numeric operations require numerals.

LF oft : term -> tp -> type =
| t_tt   : oft tt bool
| t_ff   : oft ff bool
| t_ite  : oft M1 bool -> oft M2 T -> oft M3 T
         -> oft (ite M1 M2 M3) T
| t_z    : oft z nat
| t_succ : oft M nat -> oft (succ M) nat
| t_pred : oft M nat -> oft (pred M) nat
| t_isz  : oft M nat -> oft (iszero M) bool
;

Under these rules succ tt, which §2.2 accepted as syntax, has no type: no constructor concludes oft (succ tt) T for any T, since t_succ would require oft tt nat and nothing concludes that.

On paper, D :: J says that D is a derivation of the judgment J. The double colon keeps the statement legible when the judgment is itself a typing: D :: M : T is a derivation D of M : T. In LF the same statement is the typing D : oft M T, the derivation being a term and the judgment its type. The proofs in this book are written in the paper notation.

§3Boxes and functions#

Nothing at the index level computes, so the operations one wants on the arithmetic language, such as deciding whether a term is a numeral or adding two numerals, must be written at the computation level. To handle index-level data there, the computation level wraps it in a box. This section introduces boxes, and then the functions that take them apart.

§3.1 · Boxed types and boxed objects

The computation level cannot refer to term directly. It can refer to [ |- term], the type of boxed closed terms of type term. Correspondingly, the computation-level value is not z but [ |- z].

§3.2 · rec, fn, case#

A function is declared with rec and is recursive by default. Its type is mandatory. Beluga does not infer function types as ML does; the programmer states the type and Beluga checks the body against it. This is less of an imposition than it may appear: the type is the statement of the theorem the function proves, and a proof should begin from a clear statement of what it proves.

The first function decides whether a term is a numeral. The computation level has no booleans of its own, so the answer is one of the object language's, returned boxed.

rec isnum : [ |- term] -> [ |- term] =
fn m => case m of
| [ |- z]      => [ |- tt]
| [ |- succ M] => isnum [ |- M]
| [ |- M]      => [ |- ff]
;

Five features of this definition are new.

• fn m => e is computation-level lambda abstraction. It introduces the computation variable m, which stands for a value of the computation level, here a boxed term; it is therefore written in lower case, and never occurs inside a box.
• case e of | p => e' | … performs pattern matching, as OCaml's match e with does. The expression analysed is the scrutinee.
• Patterns are written boxed, as [ |- z] rather than z, because the scrutinee has a boxed type. Matching a box against a box unwraps it and exposes the index-level term within. The pattern [ |- succ M] binds the metavariable M to whatever stands under succ.
• Branches are tried in order, and the first whose pattern matches is taken. The last branch here matches anything, and is reached only by a term that neither of the first two matched. Every program over syntax in this part relies on that.
• Branches are separated by |, and the declaration as a whole is terminated by ;.

The recursive call in the second branch returns its result unchanged, as the result of the whole. Nothing further is built from it, and so nothing further need be done with it. §3.3 is about the case where something must.

rec isval : [ |- term] -> [ |- term] =
fn m => case m of
| [ |- tt] => [ |- tt]
| [ |- ff] => [ |- tt]
| [ |- M]  => isnum [ |- M]
;

§3.3 · let and staging#

Addition on numerals requires building a new term around the result of a recursive call.

rec add : [ |- term] -> [ |- term] -> [ |- term] =
fn m => fn n => case m of
| [ |- z]      => n
| [ |- succ M] =>
  let [ |- R] = add [ |- M] n in [ |- succ R]
| [ |- M]      => [ |- M]
;

The second branch contains the one manoeuvre in the language that has no counterpart in ML.

1. The pattern [ |- succ M] matches a boxed term built with succ and binds the metavariable M to the predecessor. M is index-level data.
2. Recursion requires handing M to add, which expects a boxed argument, so one writes [ |- M]. The term has been boxed.
3. The recursive call returns a value of type [ |- term], a boxed term. Building succ of it requires access to the index-level term inside, obtained by unboxing: matching against the pattern [ |- R] in a let.
4. With the metavariable R in hand, [ |- succ R] can be built.

| [ |- succ M] => [ |- succ (add [ |- M] n)]     % rejected

The construct let p = e in e' is not primitive. It is a case with a single branch, exhaustive only when that one pattern covers every value of the scrutinee's type. Here the pattern [ |- R] matches any term, so it does. That property makes let the appropriate tool for inversion, the proof step in which only one rule could have derived a given judgment. §4.6 shows what Beluga does with a let that is not exhaustive, and §15.4 returns to the point.

rec double : [ |- term] -> [ |- term] =
fn m => case m of
| [ |- z]      => [ |- z]
| [ |- succ M] =>
  let [ |- R] = double [ |- M] in [ |- succ (succ R)]
| [ |- M]      => [ |- M]
;

rec fold_isz : [ |- term] -> [ |- term] =
fn m => case m of
| [ |- iszero z] => [ |- tt]
| [ |- ite M1 M2 M3] =>
  let [ |- N1] = fold_isz [ |- M1] in
  let [ |- N2] = fold_isz [ |- M2] in
  let [ |- N3] = fold_isz [ |- M3] in
  [ |- ite N1 N2 N3]
| [ |- succ M] =>
  let [ |- N] = fold_isz [ |- M] in [ |- succ N]
| [ |- pred M] =>
  let [ |- N] = fold_isz [ |- M] in [ |- pred N]
| [ |- iszero M] =>
  let [ |- N] = fold_isz [ |- M] in [ |- iszero N]
| [ |- M] => [ |- M]
;

§3.4 · Several arguments at once

A single fn may bind several computation variables. The following declares the same function as before.

rec add2 : [ |- term] -> [ |- term] -> [ |- term] =
fn m, n => case m of
| [ |- z]      => n
| [ |- succ M] => let [ |- R] = add2 [ |- M] n in [ |- succ R]
| [ |- M]      => [ |- M]
;

Functions of several arguments are curried, as in ML: add2 has the type of add, and fn m, n => e abbreviates fn m => fn n => e. The computation level does have tuples, of type τ1 * τ2, built as (e1, e2) and taken apart by let (x, y) = e in e', but curried arguments are the idiom.

§3.5 · fun

fun abstracts and matches in a single step, after the manner of a clausal definition in Haskell or OCaml's function. §18 shows that it is indispensable for coinductive types; it is available everywhere.

rec add3 : [ |- term] -> [ |- term] -> [ |- term] =
fun [ |- z]      n => n
  | [ |- succ M] n => let [ |- R] = add3 [ |- M] n in [ |- succ R]
  | [ |- M]      n => [ |- M]
;

rec isnum2 : [ |- term] -> [ |- term] =
fun [ |- z]      => [ |- tt]
  | [ |- succ M] => isnum2 [ |- M]
  | [ |- M]      => [ |- ff]
;

§4Index types and type reconstruction#

The functions of §3 compute with index-level data, but their types say nothing about it: a function from [ |- term] to [ |- term] may return any term at all. Because an index-level type can mention terms, a computation type can say more, that a sequence of steps leads from one particular term to another, or that a function accepts only numerals other than zero. This section shows how such types are written, what Beluga supplies when parts of them are left implicit, and how pattern matching uses what they say.

§4.1 · Invariants carried by the type

Because the indices of a family reside in its types, the type of a function can state an invariant that would otherwise require a separate proof. Evaluation in several steps is the reflexive, transitive closure of step, and is declared with two rules.

LF mstep : term -> term -> type =
| ms_refl : mstep M M
| ms_step : step M M' -> mstep M' M'' -> mstep M M''
;

A derivation of mstep M M' is a sequence of steps leading from M to M'. Applying e_succ to each step in turn yields a sequence leading from succ M to succ M'.

rec ms_succ : [ |- mstep M M'] -> [ |- mstep (succ M) (succ M')] =
fn d => case d of
| [ |- ms_refl]     => [ |- ms_refl]
| [ |- ms_step S D] =>
  let [ |- E] = ms_succ [ |- D] in
  [ |- ms_step (e_succ S) E]
;

Set this beside the same program over unindexed lists of steps, which would map e_succ along a list. The code would have the same shape, branch for branch, but here the type carries a theorem: whatever sequence goes in, what comes out leads from succ of its start to succ of its end. The elaborated control shows that the program Beluga checked is not the program written. §4.3 and §4.4 account for the difference.

rec ms_trans : [ |- mstep M M'] -> [ |- mstep M' M'']
               -> [ |- mstep M M''] =
fn d, e => case d of
| [ |- ms_refl]     => e
| [ |- ms_step S D] =>
  let [ |- F] = ms_trans [ |- D] e in [ |- ms_step S F]
;

§4.2 · Π-types

Both levels provide a dependent function space, written with braces.

The type of nv_s, with its index argument written out, is therefore the following.

nv_s : {N : term} numval N -> numval (succ N)

§4.3 · Free variables and implicit arguments#

The following rule is responsible for much of what reconstruction does on the programmer's behalf, and for many of Beluga's least transparent error messages.

So the declaration

nv_s : numval N -> numval (succ N)

is recorded as

nv_s : {N : term} numval N -> numval (succ N)

and nv_s nv_z elaborates to nv_s z nv_z. The z was obtained by matching the type of nv_z, namely numval z, against the expected numval N. It was not written and cannot be written: Beluga rejects nv_s z nv_z as an application of nv_s to one argument too many.

§4.4 · The elaborated form#

Type reconstruction is the pass that performs all of this. It infers the types of free variables, abstracts over them, inserts the corresponding abstractions into the program, and supplies omitted arguments at every call site. Reconstruction is what makes a dependently-typed language writable. It also means that what is checked differs from what was written, and much of the confusion about Beluga arises from that difference.

Two habits keep that confusion in check. The first is a diagnostic rule: an error that mentions a variable not appearing in the source concerns an implicit argument, and therefore concerns reconstruction. The second is a practice: when a type does not behave as expected, write out the elaborated form by hand, or pass +implicit to the compiler, which prints implicit arguments alongside their constructors.

In the case of ms_succ the two forms differ in four respects, all visible in the elaborated listing above: the leading {M : [ |- term]} {M' : [ |- term]}, the mlam M, M' that introduces them (the binder of §4.7), the index arguments now written in every constructor, and the [ |- M1] [ |- M'] supplied to the recursive call. The elaborated listing is a picture of what Beluga checks, not source Beluga would accept, for implicit arguments cannot be written; it has nonetheless been checked, against a signature in which every one of them is declared explicitly.

§4.5 · Refinement by pattern matching

In ML, matching a list against nil yields no new information about the type; the scrutinee was a list before and remains one. With indexed types, a match conveys information about the indices, and that information is propagated into the branch.

In ms_succ the scrutinee has type [ |- mstep M M'].

• In the [ |- ms_refl] branch the pattern has type mstep M M. For the match to be possible, M' must be M. Beluga records the equation M′ = M and uses it while checking the branch, which is why returning [ |- ms_refl] there, of type mstep (succ M) (succ M), satisfies the declared result type [ |- mstep (succ M) (succ M')].
• In the [ |- ms_step S D] branch the pattern has type mstep M M' for a fresh intermediate term M1, with S of type step M M1 and D of type mstep M1 M'. The recursive call on D is therefore at M1, which is the index the elaborated form supplies.

§4.6 · Excluding inapplicable calls

Indexed types also let a function refuse inputs it cannot handle. The predecessor of a numeral can be given a type that accepts only numerals other than zero, with no option type, no error case, and no run-time check.

rec nv_pred : [ |- numval (succ N)] -> [ |- numval N] =
fn v => let [ |- nv_s V] = v in [ |- V]
;

The let here is the inversion of §3.3. The argument has type numval (succ N), which nv_z : numval z cannot match, so nv_s is the only possibility and a single branch is exhaustive. Were the argument of type numval M instead, nv_z would be possible as well, and the same single branch would not be exhaustive. Beluga reports that only when coverage checking is on; without it the omission passes in silence, which is the subject of §20.1.

rec inv_succ : [ |- oft (succ M) nat] -> [ |- oft M nat] =
fn d => let [ |- t_succ D] = d in [ |- D]
;

§4.7 · mlam

The function of §3.2 answered whether a term is a numeral with tt or ff, an answer that carries no evidence. A version that answers with evidence needs a family with an answer for each case.

LF nvq : term -> type =
| yes : numval M -> nvq M
| no  : nvq M
;

The answer's type, nvq M, mentions the term being asked about, so the function's type must name that term: it quantifies over it with braces, {M : [ |- term]}. Where a function's type quantifies over index-level data with braces, the corresponding abstraction in the body is mlam rather than fn. The distinction follows the two classes of variable. fn binds computation variables; mlam binds metavariables, context variables, parameter variables and substitution variables.

rec decide : {M : [ |- term]} [ |- nvq M] =
mlam M => case [ |- M] of
| [ |- z]       => [ |- yes nv_z]
| [ |- succ M'] =>
  (case decide [ |- M'] of
   | [ |- yes V] => [ |- yes (nv_s V)]
   | [ |- no]    => [ |- no])
| [ |- M']      => [ |- no]
;

Only the affirmative answer is certified. no carries nothing, and certifying that a term is not a numeral would need a family for that judgment too; nothing here requires one.

LF valq : term -> type =
| vyes : value M -> valq M
| vno  : valq M
;

rec decide_val : {M : [ |- term]} [ |- valq M] =
mlam M => case [ |- M] of
| [ |- tt] => [ |- vyes v_tt]
| [ |- ff] => [ |- vyes v_ff]
| [ |- M'] =>
  (case decide [ |- M'] of
   | [ |- yes V] => [ |- vyes (v_num V)]
   | [ |- no]    => [ |- vno])
;

§4.8 · Existential quantification by packaging

The need eventually arises to assert that there exists some term M' such that something holds, and Beluga's computation types provide no existential quantifier. The standard workaround appears throughout real developments. Wrap the existential in a constructor. The implicit arguments of a constructor are existentially quantified when viewed from outside.

LF steps : term -> type =
| some_step : step M M' -> steps M
;

A term of steps M is a step from M together with a target that cannot be read off the type. To return a step to some term, return a steps M. Declaring some_step : {M' : term} step M M' -> steps M instead would make the target an explicit argument, written at every construction, but the type steps M would conceal it all the same. §5.4 uses the technique to carry a proof alongside a result.

rec steps_succ : [ |- steps M] -> [ |- steps (succ M)] =
fn s => let [ |- some_step S] = s in [ |- some_step (e_succ S)]
;

§5Proofs as programs#

The previous three sections introduced every construct a first proof needs: families that represent judgments, functions over boxed data, and types that state invariants. This section puts them together, proving a small lemma first on paper and then in Beluga, and ends with the progress half of type safety.

§5.1 · A lemma and its program

The first proof is a small lemma about the arithmetic language. It is proved on paper first, by induction on a derivation (§0.5), and then transcribed.

Transcribed:

rec nv_nat :  [ |- numval N]  -> [ |- oft N nat] =fn v => case v of| [ |- nv_z]   =>  [ |- t_z]| [ |- nv_s V] =>  let [ |- D] = nv_nat [ |- V] in  [ |- t_succ D];

The type is the theorem. [ |- numval N] -> [ |- oft N nat] reads: given evidence that N is a numeral, produce a derivation that it has type nat. The free N is quantified implicitly at the front, as §4.3 described, supplying the universal quantification that the informal statement left tacit.

§5.2 · The correspondence#

The translation is systematic, and the table below gives it in full.

§5.3 · Empty types and impossible#

Informal proofs frequently observe that no rule could have derived some judgment, so that the case does not arise. In Beluga the step has a precise meaning: the type in question is uninhabited, and there are no cases to consider.

No rule concludes step tt M'. Every rule of step concludes a step from a term built by ite, succ, pred or iszero, and tt is none of these. The type is therefore empty, and anything follows from it. To have something to conclude, declare a family that is empty by construction.

LF void : type = ;

rec tt_no_step : [ |- step tt M'] -> [ |- void] =
fn s => impossible s
;

The spelling is impossible e, the counterpart of OCaml's refutation case | p -> ., which asks the compiler to confirm that a pattern can match nothing. A case must carry at least one branch, which is why the language reserves a keyword for the empty one rather than letting the branch list be empty. impossible obliges Beluga to verify that the type is in fact uninhabited; if it is not, Beluga reports that the expression is not impossible, its type being possibly inhabited. It does not say which rule could conclude that type; finding the rule is left to the reader.

rec nv_no_step : [ |- numval M] -> [ |- step M M'] -> [ |- void] =
fn v, s => case v of
| [ |- nv_z]   => impossible s
| [ |- nv_s V] =>
  let [ |- e_succ S] = s in nv_no_step [ |- V] [ |- S]
;

rec val_no_step : [ |- value M] -> [ |- step M M'] -> [ |- void] =
fn w, s => case w of
| [ |- v_tt]    => impossible s
| [ |- v_ff]    => impossible s
| [ |- v_num V] => nv_no_step [ |- V] s
;

§5.4 · Certified programming

Combining §4.8 with §5.1 yields programs that return a result together with a proof about it. Suppose a function is to say of a well-typed term whether it is a value or can take a step. Package each answer with its evidence.

LF progress : term -> type =
| p_val  : value M -> progress M
| p_step : step M M' -> progress M
;

The function that builds the package proves the progress half of type safety.

On paper the proof is an induction on the derivation of M : T. In each compound case it applies the induction hypothesis to the subterm that evaluation examines first. If that subterm steps, the whole term steps, by the rule that evaluates under the constructor, e_succ for instance. If the subterm is a value, the proof must know which value, and its type determines that. Pierce calls the lemma that says so the canonical forms lemma; this book keeps canonical form for a different notion, defined in §6.3.

The second statement ends in a disjunction, and a disjunction is a family with one constructor for each disjunct, as progress itself is.

LF boolval : term -> type =
| bv_tt : boolval tt
| bv_ff : boolval ff
;

One fact is needed first: no numeral has type bool. Both of its cases are empty, since no rule concludes oft z bool and none concludes oft (succ N) bool, and impossible closes each. The result type is [ |- void], the empty type of §5.3, which is how a function states that its arguments cannot exist together.

rec nv_not_bool : [ |- numval M] -> [ |- oft M bool]
                  -> [ |- void] =
fn v, d => case v of
| [ |- nv_z]   => impossible d
| [ |- nv_s V] => impossible d
;

rec cf_nat : [ |- oft M nat] -> [ |- value M]
             -> [ |- numval M] =
fn d, w => case w of
| [ |- v_tt]    => impossible d
| [ |- v_ff]    => impossible d
| [ |- v_num V] => [ |- V]
;

rec cf_bool : [ |- oft M bool] -> [ |- value M]
              -> [ |- boolval M] =
fn d, w => case w of
| [ |- v_tt]    => [ |- bv_tt]
| [ |- v_ff]    => [ |- bv_ff]
| [ |- v_num V] => impossible (nv_not_bool [ |- V] d)
;

In cf_nat the branches for v_tt and v_ff refine M to tt and to ff (§4.5), after which d has type [ |- oft tt nat] or [ |- oft ff nat], and no rule concludes either. The branch for v_num in cf_bool is different. There d has type [ |- oft M bool] for an M known only to be a numeral, and that type, taken alone, could be inhabited: t_tt concludes it if M is tt. So impossible d is refused. The contradiction lies in V and d together, nv_not_bool combines them, and its result, of empty type, is what impossible is given.

With the lemmas in hand, progress is a case on the typing derivation.

rec prog : [ |- oft M T] -> [ |- progress M] =
fn d => case d of
| [ |- t_tt] => [ |- p_val v_tt]
| [ |- t_ff] => [ |- p_val v_ff]
| [ |- t_z]  => [ |- p_val (v_num nv_z)]
| [ |- t_succ D] =>
  (case prog [ |- D] of
   | [ |- p_val W]  =>
     let [ |- V] = cf_nat [ |- D] [ |- W] in
     [ |- p_val (v_num (nv_s V))]
   | [ |- p_step S] => [ |- p_step (e_succ S)])
| [ |- t_pred D] =>
  (case prog [ |- D] of
   | [ |- p_val W]  =>
     (case cf_nat [ |- D] [ |- W] of
      | [ |- nv_z]   => [ |- p_step e_pred_z]
      | [ |- nv_s V] => [ |- p_step (e_pred_s V)])
   | [ |- p_step S] => [ |- p_step (e_pred S)])
| [ |- t_isz D] =>
  (case prog [ |- D] of
   | [ |- p_val W]  =>
     (case cf_nat [ |- D] [ |- W] of
      | [ |- nv_z]   => [ |- p_step e_isz_z]
      | [ |- nv_s V] => [ |- p_step (e_isz_s V)])
   | [ |- p_step S] => [ |- p_step (e_isz S)])
| [ |- t_ite D1 D2 D3] =>
  (case prog [ |- D1] of
   | [ |- p_val W]  =>
     (case cf_bool [ |- D1] [ |- W] of
      | [ |- bv_tt] => [ |- p_step e_ite_tt]
      | [ |- bv_ff] => [ |- p_step e_ite_ff])
   | [ |- p_step S] => [ |- p_step (e_ite S)])
;

The axioms are values. For succ, pred and iszero the subterm is asked for its progress. A step lifts to the whole term by e_succ, e_pred or e_isz. A value is, by cf_nat, a numeral: for succ that makes the whole term a numeral, and for pred and iszero a case on the numeral selects the rule that computes. The conditional is the same, with cf_bool in place of cf_nat. Each piece of evidence is checked where it is built. Answering p_step e_pred_z for pred (succ N) is a type error, since e_pred_z steps only pred z.

That prog has its declared type does not yet make it a proof. A proof must also consider every case, and its induction must be well founded; typechecking establishes neither, and a prog with a branch deleted still typechecks. The first is the business of coverage checking and the second of totality checking, and §20 shows how Beluga is asked for each. Both succeed on prog.

The certificate prog returns can be checked independently of the program that produced it. One need not trust the function, only the typechecker.

rec pres : [ |- oft M T] -> [ |- step M M']
           -> [ |- oft M' T] =
fn d, s => case d of
| [ |- t_tt] => impossible s
| [ |- t_ff] => impossible s
| [ |- t_z]  => impossible s
| [ |- t_ite D1 D2 D3] =>
  (case s of
   | [ |- e_ite_tt] => [ |- D2]
   | [ |- e_ite_ff] => [ |- D3]
   | [ |- e_ite S]  =>
     let [ |- D1'] = pres [ |- D1] [ |- S] in
     [ |- t_ite D1' D2 D3])
| [ |- t_succ D] =>
  let [ |- e_succ S] = s in
  let [ |- D'] = pres [ |- D] [ |- S] in [ |- t_succ D']
| [ |- t_pred D] =>
  (case s of
   | [ |- e_pred_z]   => [ |- t_z]
   | [ |- e_pred_s V] =>
     let [ |- t_succ D'] = [ |- D] in [ |- D']
   | [ |- e_pred S]   =>
     let [ |- D'] = pres [ |- D] [ |- S] in [ |- t_pred D'])
| [ |- t_isz D] =>
  (case s of
   | [ |- e_isz_z]   => [ |- t_tt]
   | [ |- e_isz_s V] => [ |- t_ff]
   | [ |- e_isz S]   =>
     let [ |- D'] = pres [ |- D] [ |- S] in [ |- t_isz D'])
;

LF eq : term -> term -> type =
| refl : eq M M
;

rec ff_no_step : [ |- step ff M'] -> [ |- void] =
fn s => impossible s
;

rec nv_no_step : [ |- numval M] -> [ |- step M M'] -> [ |- void] =
fn v, s => case v of
| [ |- nv_z]   => impossible s
| [ |- nv_s V] =>
  let [ |- e_succ S] = s in nv_no_step [ |- V] [ |- S]
;

rec det : [ |- step M M1] -> [ |- step M M2] -> [ |- eq M1 M2] =
fn s1, s2 => case s1 of
| [ |- e_ite_tt] =>
  (case s2 of
   | [ |- e_ite_tt] => [ |- refl]
   | [ |- e_ite S]  => impossible tt_no_step [ |- S])
| [ |- e_ite_ff] =>
  (case s2 of
   | [ |- e_ite_ff] => [ |- refl]
   | [ |- e_ite S]  => impossible ff_no_step [ |- S])
| [ |- e_ite S1] =>
  (case s2 of
   | [ |- e_ite_tt] => impossible tt_no_step [ |- S1]
   | [ |- e_ite_ff] => impossible ff_no_step [ |- S1]
   | [ |- e_ite S2] =>
     let [ |- refl] = det [ |- S1] [ |- S2] in [ |- refl])
| [ |- e_succ S1] =>
  let [ |- e_succ S2] = s2 in
  let [ |- refl] = det [ |- S1] [ |- S2] in [ |- refl]
| [ |- e_pred_z] =>
  (case s2 of
   | [ |- e_pred_z] => [ |- refl]
   | [ |- e_pred S] => impossible nv_no_step [ |- nv_z] [ |- S])
| [ |- e_pred_s V] =>
  (case s2 of
   | [ |- e_pred_s W] => [ |- refl]
   | [ |- e_pred S]   =>
     impossible nv_no_step [ |- nv_s V] [ |- S])
| [ |- e_pred S1] =>
  (case s2 of
   | [ |- e_pred_z]   => impossible nv_no_step [ |- nv_z] [ |- S1]
   | [ |- e_pred_s V] =>
     impossible nv_no_step [ |- nv_s V] [ |- S1]
   | [ |- e_pred S2]  =>
     let [ |- refl] = det [ |- S1] [ |- S2] in [ |- refl])
| [ |- e_isz_z] =>
  (case s2 of
   | [ |- e_isz_z] => [ |- refl]
   | [ |- e_isz S] => impossible nv_no_step [ |- nv_z] [ |- S])
| [ |- e_isz_s V] =>
  (case s2 of
   | [ |- e_isz_s W] => [ |- refl]
   | [ |- e_isz S]   =>
     impossible nv_no_step [ |- nv_s V] [ |- S])
| [ |- e_isz S1] =>
  (case s2 of
   | [ |- e_isz_z]   => impossible nv_no_step [ |- nv_z] [ |- S1]
   | [ |- e_isz_s V] =>
     impossible nv_no_step [ |- nv_s V] [ |- S1]
   | [ |- e_isz S2]  =>
     let [ |- refl] = det [ |- S1] [ |- S2] in [ |- refl])
;

rec mpres : [ |- oft M T] -> [ |- mstep M M'] -> [ |- oft M' T] =
fn d, ms => case ms of
| [ |- ms_refl]      => d
| [ |- ms_step S MS] =>
  let [ |- D'] = pres d [ |- S] in mpres [ |- D'] [ |- MS]
;

§6The representation problem#

The arithmetic language binds no variables, so writing it down in LF needed nothing beyond declarations of data. A language with functions does bind variables, and bound variables are the source of most of the difficulty in encoding syntax: renaming a bound variable must not change the meaning of a term, substitution must not capture variables, and newly introduced variables must be fresh. This section states the problem on the untyped lambda calculus, sets out the three common answers and what each costs, and then gives LF's.

§6.1 · Three unsatisfactory answers

Take the untyped lambda calculus, whose terms are given by

and ask how to represent it so that a machine can reason about it. Three answers are in common use outside Beluga's tradition.

1. Concrete names. Represent lam x. M as a pair of a string and a term. The approach is simple and immediately wrong: lam x. x and lam y. y become distinct objects although they are the same term. One must then define α-equivalence, sameness up to the renaming of bound variables, and prove that every subsequent operation respects it.
2. De Bruijn indices. Replace names by the count of binders separating a variable from its binding site. α-equivalence becomes syntactic identity, a real gain, but substitution then needs lifting, shifting, and a battery of commutation lemmas. Each must be proved, and none concerns the theorem at hand.
3. Nominal techniques. Names with swapping built in, so that α-equivalence is free. Substitution is not, and must still be defined and reasoned about separately.

All three share a shape. In each, the metalanguage has no notion of binding, so binding has to be defined in it, and those definitions and their lemmas are the infrastructure that §1.1 described.

§6.2 · Higher-order abstract syntax#

LF's answer is different. Being a lambda calculus, LF already has binding, and the encoding reuses it.

Concretely, lam binds a variable in a term, so its argument is a function from terms to terms.

LF tm : type =
| lam : (tm -> tm) -> tm
| app : tm -> tm -> tm
;

Index-level lambda abstraction is written with a backslash, so familiar terms are encoded as follows.

Note that tm has no constructor for variables. None is required. The variables of the object language are the bound variables of LF, introduced by \x., and the apparatus of names, freshness and α-equivalence is inherited along with them. lam \x. x and lam \y. y are the same LF term, LF identifying terms up to renaming of bound variables, so there is nothing to prove.

let two = [ |- lam \f. lam \x. app f (app f x)];

LF tml : type =
| lam' : (tml -> tml) -> tml
| app' : tml -> tml -> tml
| letv : tml -> (tml -> tml) -> tml
;

§6.3 · Adequacy#

A representation is useful only if it represents what was intended, and that is a property to be checked rather than assumed.

Adequacy is a real requirement, and careless encodings fail it. It is established by induction on canonical forms, which is what makes the following subsection matter.

§6.4 · Why the index-level arrow is weak#

Suppose the same declaration were attempted in a general-purpose language: an inductive type D with a single constructor Inj : (D -> D) -> D, where -> is the ordinary function space. Three separate failures follow.

1. Inadequacy. Ordinary functions may be defined by recursion and case analysis, so Inj f, where f inspects its argument and returns different shapes for different inputs, is a perfectly good value of D corresponding to no lambda term at all. These are the exotic terms.
2. Opacity. An ordinary function cannot be inspected. Given Inj f one may apply f but never examine it, and the case analysis that a structural induction over syntax requires is therefore unavailable.
3. Inconsistency. D occurs to the left of an arrow in the type of Inj, a negative occurrence, violating the positivity restriction that keeps a type theory consistent. The classical construction goes through.

inductive D : ctype =
| Inj : (D -> D) -> D
;

rec out : D -> (D -> D) =
fn x => case x of | Inj f => f
;

% let omega  : D = Inj (fn x => (out x) x);
% let omega2 : D = (out omega) omega;         % diverges

LF's arrow escapes all three failures by being weaker. The index level has no recursion and no case analysis, so the only inhabitants of tm -> tm are syntactic lambdas. That keeps the encoding adequate, leaves the function transparent enough to analyse, and sidesteps positivity, the index level having no fixed points to go wrong.

The obvious question follows: if LF definitions are not inductive, how can one reason inductively about them? That question is what Beluga answers, and the answer occupies Part four. Pair the LF term with the context in which it lives, and recurse over the pair.

§7What HOAS supplies#

The language of Part two now gains functions. Types gain an arrow, and terms an abstraction, which carries the type of its bound variable, and an application. That is the language the rest of the book works with until §23, and the only new thing in it is binding. An LF family is declared once, with all of its constructors, so the declarations of Part two are repeated whole, the new lines marked.

LF tp : type =
| nat  : tp
| bool : tp
| arr  : tp -> tp -> tp  % new
;

LF term : type =
| tt     : term
| ff     : term
| ite    : term -> term -> term -> term
| z      : term
| succ   : term -> term
| pred   : term -> term
| iszero : term -> term
| lam    : tp -> (term -> term) -> term  % new
| app    : term -> term -> term  % new
;

§7.1 · Substitution as function application

The β rule of the object language states that

and the right-hand side is the capture-avoiding substitution that would otherwise have to be defined. Under HOAS, M is a function, and substituting N for the bound variable is applying that function. Evaluation gains a value and three rules, those of Pierce's chapter 9: an application evaluates its function, then its argument, and a lam applied to a value is the redex, the term that reduces.

LF numval : term -> type =
| nv_z : numval z
| nv_s : numval N -> numval (succ N)
;

LF value : term -> type =
| v_tt  : value tt
| v_ff  : value ff
| v_num : numval N -> value N
| v_lam : value (lam T M)  % new
;

LF step : term -> term -> type =
| e_ite_tt  : step (ite tt M2 M3) M2
| e_ite_ff  : step (ite ff M2 M3) M3
| e_ite     : step M1 M1' -> step (ite M1 M2 M3) (ite M1' M2 M3)
| e_succ    : step M M' -> step (succ M) (succ M')
| e_pred_z  : step (pred z) z
| e_pred_s  : numval N -> step (pred (succ N)) N
| e_pred    : step M M' -> step (pred M) (pred M')
| e_isz_z   : step (iszero z) tt
| e_isz_s   : numval N -> step (iszero (succ N)) ff
| e_isz     : step M M' -> step (iszero M) (iszero M')
| e_app_1   : step M1 M1' -> step (app M1 M2) (app M1' M2)  % new
| e_app_2   : value M1 -> step M2 M2'  % new
              -> step (app M1 M2) (app M1 M2')
| e_app_abs : value N -> step (app (lam T M) N) (M N)  % new
;

Read the type of e_app_abs carefully. In app (lam T M) N the metavariable M appears as the second argument of lam, so reconstruction infers its type as term -> term. In the second index, M N is therefore a legal application denoting the body of the abstraction with the bound variable replaced by N. Capture-avoidance is LF's concern and is already settled.

let s : [ |- step (app (lam nat \x. succ x) z) (succ z)] =
  [ |- e_app_abs (v_num nv_z)];

let s : [ |- step (app (lam nat \x. x) (pred z))
                   (app (lam nat \x. x) z)] =
  [ |- e_app_2 v_lam e_pred_z];

§7.2 · Hypothetical judgments#

Consider typing, where binding appears in the rules rather than in the syntax. The rule for abstraction is the one every treatment states with a bar and a discharged assumption.

Two things occur in that premise, and HOAS encodes both by the same mechanism. The premise is parametric in x, in that the derivation must work for any fresh variable, and hypothetical in x : A, in that it may use that typing assumption. Parametricity becomes a Π over the variable; hypotheticality becomes an arrow from the assumption's derivation.

LF oft : term -> tp -> type =
| t_tt   : oft tt bool
| t_ff   : oft ff bool
| t_ite  : oft M1 bool -> oft M2 T -> oft M3 T
           -> oft (ite M1 M2 M3) T
| t_z    : oft z nat
| t_succ : oft M nat -> oft (succ M) nat
| t_pred : oft M nat -> oft (pred M) nat
| t_isz  : oft M nat -> oft (iszero M) bool
| t_lam  : ({x : term} oft x A -> oft (M x) B)  % new
           -> oft (lam A M) (arr A B)
| t_app  : oft M (arr A B) -> oft N A -> oft (app M N) B  % new
;

Three details deserve attention.

• The Π must be written. {x : term} is explicit here of necessity: leaving x free would quantify it at the front of the whole type of t_lam, which is the wrong scope. The assumption is local to the premise, so its quantifier must be too.
• The assumption is an argument. The component oft x A -> inside the premise says that the subderivation may use a derivation that x has type A, which is what reasoning under the assumption x : A amounts to.
• Scope is enforced by typing. x is bound by the Π and therefore cannot occur in oft (lam A M) (arr A B). The side condition that x must not escape is not a side condition at all; it is scoping, checked by the typechecker.

A derivation and its term follow. The term lam x:nat. lam y:nat. x has type nat ⇒ nat ⇒ nat.

let d : [ |- oft (lam nat \x. iszero x) (arr nat bool)] =
  [ |- t_lam \x.\u. t_isz u];

§7.3 · The typing context in LF

The informal rule mentions a context: Γ, x:A ⊢ M : B above the line and Γ ⊢ lam x:A. M : A ⇒ B below. The LF encoding contains no Γ. Where has it gone?

It has become the LF context. The term t_lam \x.\u. t_lam \y.\v. u has a subterm u whose LF type is oft x nat, and that type is meaningful only in the LF context

The typing context of the object language has become LF's own context of bound variables. This identification is what keeps the encoding compact, and it is also the source of the problem that Part four exists to solve: reasoning inductively about derivations such as u requires talking about the context in which they live. An LF term on its own does not suffice.

§8Contextual types#

Every computation so far has handled closed index-level data: each box has had an empty context. A proof about a language with binders must also handle open terms and open derivations, those met beneath a binder, together with the variables they may mention. This section introduces the type of such an object, the contextual type, which pairs an LF type with the context in which it is meaningful.

§8.1 · Open terms

Every box so far has had an empty context: [ |- term], [ |- step M M']. Such terms are closed, mentioning no free variables. As soon as a binder is traversed, closed terms no longer suffice.

Consider writing a function that simplifies terms, folding ite tt M N to M wherever it occurs, beneath binders included. Simplifying lam T \x. M requires simplifying the body M, and M is not closed: it may mention x. The recursive call must therefore be made on an open term, and the type system must be able to say which variables it is open in. Without that, the type of the recursive call cannot be stated, and nothing guarantees that x does not escape.

§8.2 · The contextual type#

Three objects in the language of §7:

let c1 = [ |- lam nat \x. succ x];
let c2 = [x : term |- succ x];
let c3 = [x : term, u : oft x nat |- t_succ u];

Their contextual types are [ |- term], [x : term |- term] and

The last is a derivation, complete given the assumption u that x has type nat. In proof-theoretic terms the context holds the hypotheses and the turnstile means what it ordinarily means.

let c4 = [x : term, y : term |- app y x];

let c5 : [ |- oft (lam nat \x. x) (arr nat nat)] =
  [ |- t_lam \x.\u. u];

let c9 : [x : term, u : oft x bool
         |- oft (ite x z (succ z)) nat] =
  [x : term, u : oft x bool |- t_ite u t_z (t_succ t_z)];

§8.3 · The grammar of computation types

With contextual types available, the computation-level type grammar can be given whole. It is short; the pieces still to come are marked with the section that introduces them.

computation types
  tau  ::= [ U ]                 a boxed contextual type
        |  I tau1 … taun         an inductive, stratified or coinductive type, applied  (§16–§18)
        |  tau1 -> tau2          simple (non-dependent) function space
        |  tau1 * tau2           a pair  (§3.4)
        |  { X : U } tau         dependent function space — a PiBox, explicit
        |  ( X : U ) tau         the same, but implicit

contextual types
  U    ::= Psi |- A              an LF term of type A in context Psi
        |  $[ Psi |- Phi ]       a substitution from Phi to Psi  (§12)
        |  $[ Psi |-# Phi ]      a renaming: variables for variables  (§12.3)
        |  #[ Psi |- A ]         a parameter variable's type  (§11.4)
        |  s                     a schema: a context's type  (§11.1)

That is the whole of it. There are no sums, no polymorphism and no universes. Expressive power comes from the index domain rather than from the computation types.

LF opt : type =
| nothing : opt
| just    : term -> opt
;

rec pred_opt : [ |- term] -> [ |- opt] =
fn m => case m of
| [ |- succ N] => [ |- just N]
| [ |- N]      => [ |- nothing]
;

§9Metavariables and delayed substitutions#

Metavariables and their substitutions are the part of Beluga that readers most often find difficult, and almost all of the difficulty comes from one rule: every occurrence of a metavariable carries a substitution, which is usually not written. This section states the rule, lists the forms a substitution can take, and examines the error that an unwritten substitution most often causes.

§9.1 · The rule

An example with nothing elided. Suppose X : [x : tp, y : tp |- tp], perhaps with X the type arr x y. Then

The substitution [nat, nat] replaces x by nat and y by nat, in order, producing a closed object. Substitutions are written positionally: the nth term goes to the nth declaration of the metavariable's context.

rec diag : [x : tp, y : tp |- tp] -> [x : tp |- tp] =
fn a => let [x : tp, y : tp |- X] = a in [x : tp |- X[x, x]]
;

§9.2 · The available forms

Worked readings, in a context g of unknown length:

§9.3 · The characteristic error#

Consider stating type uniqueness for the simply-typed lambda calculus: if a term has type A1 and type A2 in the same context, then A1 and A2 are equal. With the schema ctx and the equality equal that §11 declares, the natural first attempt is

(g : ctx) [g |- oft M A1] -> [g |- oft M A2]
  -> [ |- equal A1 A2]

and the correct version is

(g : ctx) [g |- oft M A1[]] -> [g |- oft M A2[]]
  -> [ |- equal A1 A2]

The reason is as follows. Reconstruction works left to right and adopts the first consistent reading available. Encountering A1 inside g |- oft M A1 with no substitution, it infers the most general type on offer, namely [g |- tp], a type that may depend on the variables in g. That is wrong for the simply-typed lambda calculus, in which types are closed, but nothing so far has said otherwise.

The contradiction surfaces later, at [ |- equal A1 A2]. There the context is empty, so the implicit identity substitution would have to map g to nothing, which it cannot. The reported error concerns an ill-typed substitution at the third occurrence, nowhere near the mistake.

§10Context variables#

A contextual type with a fixed context, such as [x : term |- term], describes terms with exactly one free variable. A function that descends through binders meets terms with any number of free variables, so it must range over contexts too. This section introduces variables standing for contexts, the two ways of quantifying over them, a first function generic in its context, and the matching that takes a context apart.

§10.1 · Abstracting over a context

A function that traverses binders meets contexts of every length and must therefore be generic in the context. Beluga permits quantification over one.

The restriction to the head position follows from how substitutions work. Substitutions are positional, and the declarations following the context variable are the ones whose positions are known. Permitting a context variable in the middle would leave the positions of the declarations after it undetermined, and no substitution into such a context could be written down.

§10.2 · Implicit and explicit quantification#

Context quantification comes in two forms, and the choice between them belongs to the programmer.

§10.3 · A function over open terms

The function promised in §8.1 follows: it folds every conditional whose guard is a boolean literal, wherever the conditional occurs. The declarations come first: a schema describing the shape of the contexts, and then the function. Schemas are the subject of §11.1; for the moment read schema vctx = term; as describing contexts of term variables x : term.

schema vctx = term;

rec simp : (g : vctx) [g |- term] -> [g |- term] =
fn m => case m of
| [g |- #p] => [g |- #p]
| [g |- lam T \x. M] =>
  let [g, x : term |- M'] = simp [g, x : term |- M] in
  [g |- lam T \x. M']
| [g |- app M N] =>
  let [g |- M'] = simp [g |- M] in
  let [g |- N'] = simp [g |- N] in
  [g |- app M' N']
| [g |- ite M1 M2 M3] =>
  (case simp [g |- M1] of
   | [g |- tt] => simp [g |- M2]
   | [g |- ff] => simp [g |- M3]
   | [g |- N1] =>
     let [g |- N2] = simp [g |- M2] in
     let [g |- N3] = simp [g |- M3] in
     [g |- ite N1 N2 N3])
| [g |- succ M]   =>
  let [g |- M'] = simp [g |- M] in [g |- succ M']
| [g |- pred M]   =>
  let [g |- M'] = simp [g |- M] in [g |- pred M']
| [g |- iszero M] =>
  let [g |- M'] = simp [g |- M] in [g |- iszero M']
| [g |- tt]       => [g |- tt]
| [g |- ff]       => [g |- ff]
| [g |- z]        => [g |- z]
;

The unfamiliar elements are taken in turn.

The type. (g : vctx) [g |- term] -> [g |- term] reads: for every context g of schema vctx, given a term in g, return a term in g. The result lives in the context of the argument, so no variable can escape and none can be invented, and that is checked without further work. Nothing in the type says that the result has the type of the argument. In this book's language typing is a separate judgment, so that is a theorem to be proved about simp, as preservation was proved about evaluation in Part two. g is implicitly quantified and therefore never supplied.

A case for each form. A term in context g is one of the nine constructions of term, or a variable from g. Here it becomes visible why the context had to be first class. The variable case exists because the context exists. Under HOAS there is no constructor for variables, so without first-class contexts there would be no case to write, and the coverage checker demands it: delete the first branch and it reports the variable case as not covered.

[g |- #p]. A parameter variable, the pattern matching a variable drawn from the context and nothing else. §11.4 treats it precisely. Operationally, once g is concrete, #p matches any one of its declarations, and a variable simplifies to itself.

[g |- lam T \x. M]. Matching beneath the binder. In this branch M has type [g, x : term |- term], the body, open in one further variable. T, the type the abstraction carries, is matched like any other argument and rebuilt unchanged.

The recursive call simp [g, x : term |- M]. The context has grown, which is permitted: the type of simp quantifies over all contexts of the schema, so g, x : term is as acceptable as g. This is what abstracting over contexts provides. In a system with implicit contexts the same effect must be arranged by hand.

The conditional. The guard is simplified first and the result inspected. A literal tt or ff selects a branch, which is simplified in turn; any other guard leaves the conditional in place, its parts simplified. Matching on the result of a recursive call is an ordinary case, and its patterns are as open as its scrutinee: [g |- tt] is tt, in context g.

rec subst_z : (g : vctx) [g, x : term |- term] -> [g |- term] =
fn m => let [g, x : term |- M] = m in [g |- M[.., z]]
;

rec isvar : (g : vctx) [g |- term] -> [ |- term] =
fn m => case m of
| [g |- #p] => [ |- tt]
| [g |- M]  => [ |- ff]
;

rec swap : (g : vctx) [g, x : term, y : term |- term]
           -> [g, x : term, y : term |- term] =
fn m => let [g, x : term, y : term |- M] = m in
  [g, x : term, y : term |- M[.., y, x]]
;

rec beta : (g : vctx) [g |- term] -> [g |- term] =
fn m => case m of
| [g |- app (lam T \x. M) N] => [g |- M[.., N]]
| [g |- M]                   => [g |- M]
;

§10.4 · Matching on a context

Some functions must tell the empty context from one that has a last declaration. The following function closes a term by abstracting over each of its free variables in turn, the last first, and stops when none is left; it recurses on the context rather than on the term. A context is data and can be matched on. The pattern [ ] matches the empty context and [g', x : term] a context with at least one declaration.

rec close : {g : vctx} {T : [ |- tp]} [g |- term] -> [ |- term] =
mlam g, T => fn m => case [g] of
| [ ]            => m
| [g', x : term] =>
  let [g', x : term |- M] = m in
  close [g'] [ |- T] [g' |- lam T[] \x. M]
;

Read the second branch. M has type [g', x : term |- term]. Writing [g' |- lam T[] \x. M] places M beneath a new LF binder, so the last variable of M is now bound and the result is open in one fewer variable; renaming a bound variable is not an operation one performs, it is what the notation means. T[] is the weakening of §9.2: T is closed and is used inside g'. The call close [g'] … continues with the shorter context, until [ ] is reached and the term is closed.

Note also the mlam g, T. The quantifiers are explicit, so the context and the type are bound in the body and supplied at every call. The recursion is on g itself, and Beluga accepts it as an induction on the context: declared total by / total g (close g t m) /, §20.2, the function passes.

rec closez : {g : vctx} [g |- term] -> [ |- term] =
mlam g => fn m => case [g] of
| [ ]            => m
| [g', x : term] =>
  let [g', x : term |- M] = m in closez [g'] [g' |- M[.., z]]
;

rec len : {g : vctx} [ |- term] =
mlam g => case [g] of
| [ ]            => [ |- z]
| [g', x : term] => let [ |- N] = len [g'] in [ |- succ N]
;

§11Schemas, blocks, and parameter variables#

A context variable stands for some context, but a proof needs to know what the context can contain: that every term variable in it comes with a typing assumption, for instance, and only one. This section introduces schemas, which classify contexts as types classify terms; blocks, which keep a variable and its assumption together; and parameter variables, which name a declaration drawn from a context that is otherwise unknown. With them, §11.4 proves type uniqueness for the language of Part three.

§11.1 · Schemas#

The schema vctx of §10.3, schema vctx = term;, has a single form. Under it, x1 : term, x2 : term is well formed. The context a : tp, x : term is not, a : tp being no instance of term, and Beluga refuses it with the complaint that tp does not check against the schema. Schema checking is part of typechecking, so a well-typed program manipulates only well-formed contexts, and that is one further invariant requiring neither statement nor maintenance.

§11.2 · Blocks

Return to the typing judgment of §7.2. The rule t_lam extends the context with two things at once: a term variable x and a derivation u that x has type A. The two must remain together, since every term variable has exactly one typing assumption and that assumption concerns that variable.

A schema expresses the requirement with a block.

schema ctx = some [t : tp] block x : term, u : oft x t;

Every context of schema ctx is constrained in three ways. It cannot contain a term variable without its typing assumption, cannot contain two assumptions for one variable, and cannot contain an assumption about a variable that is absent. The property that every variable has a unique typing assumption, which an informal proof states as a lemma about contexts and a de Bruijn development proves by induction, is here a consequence of the schema, enforced by the typechecker, with nothing left to prove.

A tuple is what a substitution supplies for a block variable. fill takes a derivation open in one block, a variable together with its typing assumption, and closes it: <z ; t_z> puts z for the variable and t_z for the assumption.

rec fill : [b : block (x : term, u : oft x nat)
            |- oft (succ b.1) nat]
           -> [ |- oft (succ z) nat] =
fn d =>
  let [b : block (x : term, u : oft x nat) |- D] = d in
  [ |- D[<z ; t_z>]]
;

The components are checked in order, and the type of the second is computed from the first, as a Σ-type requires: given z for x, the assumption must have type oft z nat, so <z ; t_tt> is refused. So is <t_z ; z>, a derivation standing where a term is expected. Written with a comma, <z, t_z>, the tuple does not parse.

rec subst_lem : (g : ctx)
  [g, b : block (x : term, u : oft x A[]) |- oft M[.., b.1] B[]]
  -> [g |- oft N A[]] -> [g |- oft M[.., N] B[]] =
fn d, e =>
  let [g, b : block (x : term, u : oft x _) |- D] = d in
  let [g |- E] = e in
  [g |- D[.., <_ ; E>]]
;

rec fill_tt : [b : block (x : term, u : oft x bool)
               |- oft (ite b.1 z z) nat]
              -> [ |- oft (ite tt z z) nat] =
fn d =>
  let [b : block (x : term, u : oft x bool) |- D] = d in
  [ |- D[<tt ; t_tt>]]
;

§11.3 · some

In some [t : tp] block x : term, u : oft x t, the some clause declares the variables that may differ from one entry to the next. Each declaration in the context chooses its own t, so that

has schema ctx with t instantiated differently in each entry. Without some, t would have to be fixed once for the whole context, which is not the intent.

Blocks are distinct objects, so b1.x and b2.x are different variables despite the shared field name. The name labels a position within a block rather than a global identifier.

§11.4 · Parameter variables

Where a context is abstract its declarations cannot be named, being unknown. A parameter variable is the means of referring to one regardless.

Where the schema is a plain type, as in schema vctx = term, the parameter variable #p denotes the variable itself. Where the schema consists of blocks, #p denotes a whole block, #p.1 its term component, and #p.2 the derivation that the term has some type. The variable case of a proof over typing derivations is therefore written [g |- #q.2]: the derivation is an assumption drawn from the context.

Type uniqueness, the standard exercise in this style, follows in full. Read it after the commentary below. It concludes with an equality on types of a particular shape. A structural equality, with a constructor for each way of building a type, as §21.5 declares one, can say that two types are equal only by taking them apart. This theorem has to say that two arbitrary types are the same type, so it needs an equality with a single constructor, reflexivity, whose only inhabitant is evidence that its two indices coincide.

LF equal : tp -> tp -> type =
| e_ref : equal T T
;

rec unique : (g : ctx) [g |- oft M T[]] -> [g |- oft M T2[]]
             -> [ |- equal T T2] =
fn d => fn f => case d of
| [g |- t_tt] => let [g |- t_tt] = f in [ |- e_ref]
| [g |- t_ff] => let [g |- t_ff] = f in [ |- e_ref]
| [g |- t_z]  => let [g |- t_z]  = f in [ |- e_ref]
| [g |- t_succ D] => let [g |- t_succ F] = f in [ |- e_ref]
| [g |- t_pred D] => let [g |- t_pred F] = f in [ |- e_ref]
| [g |- t_isz D]  => let [g |- t_isz F]  = f in [ |- e_ref]
| [g |- t_ite D1 D2 D3] =>
  let [g |- t_ite F1 F2 F3] = f in
  unique [g |- D2] [g |- F2]
| [g |- t_app D1 D2] =>
  let [g |- t_app F1 F2] = f in
  let [ |- e_ref] = unique [g |- D1] [g |- F1] in
  [ |- e_ref]
| [g |- t_lam \x.\u. D] =>
  let [g |- t_lam \x.\u. F] = f in
  let [ |- e_ref] =
      unique [g, b : block x : term, u : oft x _
                |- D[.., b.x, b.u]]
             [g, b |- F[.., b.x, b.u]] in
  [ |- e_ref]
| [g |- #q.2] =>
  let [g |- #r.2] = f in [ |- e_ref]
;

• Constants and operators. A rule such as t_succ fixes the type of its conclusion, here nat. Inverting the second derivation with a let finds the same rule, so both types are that type and e_ref closes the case. The conditional is the one operator whose type comes from its parts: both derivations type the branches, and recursing on D2 and F2 yields the equality required.
• Application. Match the first derivation, invert the second with a let, since only t_app can conclude the typing of an application, and recurse on the function subderivations. The result is a proof of equal (arr T1 T2) (arr S1 S2), and matching it against e_ref, the only constructor, forces the two arrow types to be identical and hence their components also. This is how an equality is used in Beluga: match it against reflexivity, and the typechecker learns that the two sides coincide.
• Abstraction. The subderivations D and F inhabit g, x : term, u : oft x _, two separate declarations. Recursion requires a context of schema ctx, whose entries are blocks, so the context is extended by a block b and D moved across by the substitution .., b.x, b.u: identity on g, then x to b.x and u to b.u. That substitution is the renaming, written down.
• Variable. [g |- #q.2] asserts that the derivation is the typing assumption carried by some block #q. Inverting f likewise yields #r.2, and because the schema guarantees one assumption per variable, #r must be the same block as #q. The two types therefore coincide and e_ref closes the case. This single line is where the schema's guarantee is used.

let d2 : [b1 : block (x : term, u : oft x nat),
          b2 : block (y : term, v : oft y (arr nat nat))
          |- oft (app b2.1 b1.1) nat] =
  [b1 : block (x : term, u : oft x nat),
   b2 : block (y : term, v : oft y (arr nat nat))
   |- t_app b2.2 b1.2];

let e2 = unique d2 d2;

rec er : (g : vctx) [g, x : term |- term]
         -> [g, x : term |- term] =
fn m => let [g, x : term |- M] = m in [g, x |- M]
;

LF void : type = ;

rec nat_not_bool : (g : ctx) [g |- oft M nat] -> [g |- oft M bool]
                   -> [ |- void] =
fn d, f => let [ |- E] = unique d f in impossible [ |- E]
;

rec idd : (g : ctx) [g |- oft M A] -> [g |- oft M A] =
fn d => d;

rec idc : (g : ctx) [g |- oft M A[]] -> [g |- oft M A[]] =
fn d => d;

§11.5 · Alternation

A schema may offer alternatives separated by +, and a context of that schema may mix entries of either shape.

schema altG = block (x : tp, u : equal x x)
            + block (x : term, u : oft x nat);

Alternation has a cost. Pattern matching on a parameter variable of such a context must now consider both shapes, so proofs acquire cases. Use it only where the object language mixes kinds of assumption.

§12Substitution variables#

Every metavariable carries a substitution (§9), but substitutions have so far been written out, never passed around. Some proofs must quantify over them: the main lemma of a proof by logical relations (§23) is a statement about every substitution that closes a term. This section makes substitutions values of the computation level, with types of their own.

§12.1 · Substitutions as values

A simultaneous substitution replaces every variable of a context at once. A proof by logical relations quantifies over such substitutions, in the form for every closing substitution σ, so substitutions must be things a function can quantify over, and in Beluga they are.

rec wk : {g : vctx} $[g, x : term |- g] =
mlam g => $[g, x : term |- ..]
;

§12.2 · Construction

A substitution is built as §9.2 describes, with ^ for the empty one and sigma, M to extend. The definition below describes a closing substitution all of whose entries are values, the substitutions a call-by-value evaluator may apply. Its shape, a predicate on each entry threaded along the context, is the shape every logical-relations proof requires; §23 uses it with reducibility in place of being a value.

inductive ValSub : {g : vctx} {$s : $[ |- g]} ctype =
| Nil : ValSub [ ] $[ |- ^]
| Dot : ValSub [g] $[ |- $s] -> [ |- value M]
        -> ValSub [g, x : term] $[ |- $s, M]
;

Read Dot thus: if $s is such a substitution for g, and M is a closed value, then $s, M is such a substitution for g extended by one further variable.

A substitution variable, once obtained, is applied as any other substitution: if M : [g |- term] and $s : $[ |- g] then M[$s] : [ |- term].

rec vs : ValSub [x : term, y : term] $[ |- tt, z] =
  Dot (Dot Nil [ |- v_tt]) [ |- v_num nv_z];

rec last : (g : vctx) ValSub [g, x : term] $[ |- $s, M]
           -> [ |- value M] =
fn v => case v of
| Dot v' w => w
;

rec vlookup : {g : vctx} {#p : #[g |- term]} ValSub [g] $[ |- $s]
              -> [ |- value #p[$s]] =
/ total g (vlookup g) /
mlam g => mlam #p => fn v => case [g] of
| [ ] => impossible [ |- #p]
| [g', x : term] =>
  (case [g', x : term |- #p] of
   | [g', x : term |- x]      => let Dot v' w = v in w
   | [g', x : term |- #q[..]] =>
     let Dot v' w = v in vlookup [g'] [g' |- #q] v')
;

§12.3 · Renamings

A substitution mapping variables to variables is a renaming, and the distinction sometimes matters, a weakening lemma holding for renamings where it fails for arbitrary substitutions. The hashed turnstile marks the restriction.

rec renamed : {g : vctx} {h : vctx}
              {$R : $[h |-# g]} [g |- term] -> [h |- term] =
mlam g, h, $R => fn t => let [g |- M] = t in [h |- M[$R]]
;

The # on the turnstile is the same marker that appears on the type of a parameter variable, restricting what may stand to its right to variables alone.

rec wkr : {g : vctx} [g |- term] -> [g, x : term |- term] =
mlam g => fn m =>
  renamed [g] [g, x : term] $[g, x : term |-# ..] m
;

§13Structural properties#

Weakening a derivation, using a lemma in a context richer than the one it was proved for, and discarding assumptions that a derivation cannot use are, in most mechanizations, lemmas proved by induction. In Beluga they are part of the language: weakening is built into the typing of substitutions, the second is context subsumption, and the third is strengthening, justified by an analysis of the signature called subordination.

§13.1 · Weakening

Adding an unused declaration to a context does not invalidate a derivation. In Beluga the property is built into the typing of substitutions. The empty substitution ^ maps into any context, and a substitution such as .. whose domain is shorter than its range is itself a weakening. The property is never stated and never proved; one writes the substitution that witnesses it, and the D[.., b.x, b.u] of §11.4 is such a witness.

rec weaken : (g : ctx) [g |- oft M T[]]
  -> [g, b : block (x : term, u : oft x S[]) |- oft M[..] T[]] =
fn d =>
  let [g |- D] = d in
  [g, b : block (x : term, u : oft x _) |- D[..]]
;

rec exch : (g : ctx)
  [g, b : block (x : term, u : oft x A[]),
      c : block (y : term, v : oft y B[])
   |- oft M[.., b.x, c.y] T[]]
  -> [g, c : block (y : term, v : oft y B[]),
         b : block (x : term, u : oft x A[])
      |- oft M[.., b.x, c.y] T[]] =
fn d =>
  let [g, b : block (x : term, u : oft x _),
          c : block (y : term, v : oft y _) |- D] = d in
  [g, c : block (y : term, v : oft y _),
      b : block (x : term, u : oft x _) |- D[.., b, c]]
;

rec contr : (g : ctx)
  [g, b : block (x : term, u : oft x A[]),
      c : block (y : term, v : oft y A[])
   |- oft M[.., b.x, c.y] T[]]
  -> [g, b : block (x : term, u : oft x A[])
      |- oft M[.., b.x, b.x] T[]] =
fn d =>
  let [g, b : block (x : term, u : oft x _),
          c : block (y : term, v : oft y _) |- D] = d in
  [g, b : block (x : term, u : oft x _) |- D[.., b, b]]
;

§13.2 · Context subsumption

Often one proves a lemma about contexts of block (x : term, u : oft x t), the schema ctx, and later one is working in contexts of block (x : term, u : oft x t, v : value x), richer by one assumption per entry, recording perhaps that each variable stands for a value. The lemma may be called regardless. Without subsumption, a transport lemma between the two context shapes would have to be proved, a lemma with no mathematical content.

§13.3 · Subordination and strengthening

The converse direction is more interesting. One sometimes knows that a derivation cannot depend on certain assumptions and wishes to discard them.

Strengthening is requested by writing a substitution that mentions only the assumptions to be retained. Given m : [g, b : block x : term, u : oft x T[] |- term], a term open in a block:

rec strengthen_ex :
     (g : ctx) [g, b : block x : term, u : oft x T[] |- term]
  -> [ |- term] =
fn m =>
  let [g, b : block x : term, u : oft x _ |- M[.., b.x]] = m in
  [ |- z]
;

The synthesized type of M is [g, x : term |- term], the typing assumption u having been dropped. Subordination licenses it: no constructor of term mentions oft, so no term can contain a typing derivation. The construction reads backwards at first. The substitution written is a weakening of M, and the strengthening is the inference Beluga draws about the context of M in order to make that weakening typecheck. Where subordination gives no such licence the pattern fails: the same one written for a typing derivation, which may well use u, does not cover, and coverage checking says so.

Harpoon provides a strengthen tactic for the same purpose, treated in §21.3. It has a secondary use. Contexts containing blocks are not in principle eligible for strengthening, but Beluga flattens blocks automatically when strengthening, so the tactic doubles as a means of flattening a block context.

rec occurs : (g : vctx) [g, x : term |- term] -> [ |- term] =
fn m => case m of
| [g, x : term |- M[..]] => [ |- ff]
| [g, x : term |- M]     => [ |- tt]
;

rec closet : {g : ctx} [g |- term] -> [ |- term] =
mlam g => fn m => case [g] of
| [ ] => m
| [g', b : block (x : term, u : oft x T[])] =>
  let [g', b : block (x : term, u : oft x _) |- M[.., b.x]] = m in
  closet [g'] [g' |- lam T[] \x. M]
;

§14Computation types and kinds#

The computation level has so far been used through boxes, function types and Π-types, as each was needed. Before it gains data types of its own (§16 to §18), its types and kinds are set out in full: how families of computation types are declared, how its two function types relate, the three ways a quantifier may be written, how a boxed value becomes a metavariable, and what the level deliberately lacks.

§14.1 · ctype

Computation-level type families are declared with the keyword ctype in the position where an LF family would say type. The parallel is deliberate. ctype is the base kind of the computation level, and a computation kind is built from it as an LF kind is built from type.

computation kinds
  K ::= ctype
      | tau -> K                 indexed by a computation type
      | { X : U } K              indexed by a contextual type, explicit
      | ( X : U ) K              indexed by a contextual type, implicit

A declaration inductive Ev : [ |- term] -> ctype = … therefore introduces a family of computation types indexed by a boxed term, one type Ev [ |- N] for each term N; §16.2 declares it, for the even numerals. Computation-level types and their constructors are capitalized by convention. The grammar does not enforce it, but every computation type declared in the distribution's examples follows it, and it keeps the two levels visually distinct.

§14.2 · The arrow and the PiBox

At the index level, A -> B abbreviates {x : A} B for an unused x; the two are one function space. At the computation level they are separate.

One cannot write {x : SomeInductiveType} tau. Quantification ranges over the index domain, which is contextual LF, and not over computation types. Dependency at the computation level is always dependency on index-level data.

rec pred_succ : {N : [ |- term]} [ |- numval N]
                -> [ |- step (pred (succ N)) N] =
mlam N => fn v => let [ |- V] = v in [ |- e_pred_s V]
;

§14.3 · Implicit and explicit quantifiers

The same three-way choice appeared in §4.3 and §10.2; the table collects it for computation types.

The final column governs §20.2. A numeric induction order counts explicit parameters only, from left to right.

§14.4 · Unboxing

A computation variable of boxed type is not a metavariable, and there are occasions for wanting it to be one, so that it may appear inside a box, in a type, or as an index.

This is the let of §3.3 viewed from the other side. Staging and unboxing name one mechanism: a let whose pattern is a box.

§14.5 · The absence of polymorphism

Beluga has no type variables and no polymorphic functions: nothing corresponds to ML's 'a list. The omission follows from the foundation rather than from the state of the implementation. The index domain is contextual LF, whose equality must be decidable if the metatheory of the computation level is to go through, and the computation level is an indexed type system in which quantification ranges over that domain and nothing else. Allowing quantification over computation types would introduce impredicativity and, in combination with the rest of the system, inconsistency.

The replacement is indexing by LF data. A generic container becomes a family indexed by an LF type, as the intrinsically typed terms of §23, tm : tp -> type, are. The dependency performs the work that polymorphism would, within the single domain the system is about.

LF tlist : type =
| tnil  : tlist
| tcons : term -> tlist -> tlist
;

rec tappend : [ |- tlist] -> [ |- tlist] -> [ |- tlist] =
fn l, k => case l of
| [ |- tnil]       => k
| [ |- tcons M L'] =>
  let [ |- R] = tappend [ |- L'] k in [ |- tcons M R]
;

§15Pattern matching in depth#

Pattern matching is the only way to take data apart, and on contextual data it does more than in ML: a match can reveal the shape of a context, refine indices beneath binders, and demand a case for the variables of the context. This section collects what a match can do and how Beluga decides which cases a match must have.

§15.1 · What may be matched on

Pattern matching is the sole elimination form for data, and it reaches further than in ML. The following may be matched on.

• Boxed contextual objects, against a constructor applied to patterns, as in [g |- t_app D1 D2].
• Terms beneath binders, as in [g |- lam T \x. M], or with the derivation binder as well, [g |- t_lam \x.\u. D].
• Variables from a context, by a parameter variable pattern [g |- #p] or a projection of one, [g |- #q.2].
• Contexts, by [ ] for the empty context and [g', x : term] for a non-empty one.
• Substitutions, by a substitution variable pattern.
• Computation-level constructors, as Dot rs rN of §12.2, as in any functional language.
• Nested combinations of all of the above.

A pattern may carry a type annotation, written p : tau, and may be preceded by explicit binders for its own metavariables, written {X : U} p => e. The latter is occasionally necessary where reconstruction cannot determine them.

§15.2 · Refinement with contexts

§4.5 introduced refinement for simple indices. With contextual types the same thing occurs and the refinement may involve the context. Matching a derivation of type [g |- oft M T[]] against [g |- t_lam \x.\u. D1] refines M to lam A M1 and T to arr A B, for fresh A, B and M1, and gives D1 the type [g, x : term, u : oft x A[] |- oft M1[.., x] B[]], in a context longer by two declarations. Beluga reports exactly that type for D1 when it lists the cases of such a branch. The branch is checked under the refinement.

§15.3 · Coverage determines the cases

When Beluga generates the cases for a split it does so from the type, including the case for variables from the context whenever the context might contain one. This is why the variable case of §10.3 must be written; the coverage checker reports it missing. Conversely, where the schema of the context makes a variable case impossible, no such case is generated.

rec nvoft : (g : vctx) [g |- numval N] -> [g |- oft N nat] =
fn v => case v of
| [g |- nv_z]   => [g |- t_z]
| [g |- nv_s V] =>
  let [g |- D] = nvoft [g |- V] in [g |- t_succ D]
;

§15.4 · let as inversion

let p = e in e' is a case with a single branch. With coverage checking on, Beluga accepts it only where that one pattern covers the type; without it, a let that misses a case passes in silence (§20.1). A covering let is the informal proof step called inversion: only one rule could have derived this, so read off its premises.

In unique, §11.4, every let is an inversion. The form let [g |- t_app F1 F2] = f says that f derives the typing of an application, must therefore end in t_app, and has premises to be named F1 and F2. Where a second rule could conclude that type, coverage checking rejects the let and a full case is required.

rec inv1 : [ |- step (ite tt M2 M3) M'] -> [ |- term] =
fn s => let [ |- e_ite_tt] = s in [ |- z]
;

rec inv2 : [ |- step (iszero tt) M] -> [ |- term] =
fn s => case s of
| [ |- e_isz S] => impossible [ |- S]
;

§15.5 · The empty case

Where no rule could have concluded the type, there are no branches at all, and the construct is impossible e, as §5.3 described; a case must carry at least one branch, so there is no empty-branch form. Harpoon's tactic is likewise called impossible. Both verify that the type is uninhabited.

rec vac : [ |- oft z bool] -> [ |- term] =
fn d => impossible d
;

rec isz_tt : [ |- oft (iszero tt) bool] -> [ |- term] =
fn d => let [ |- t_isz D] = d in impossible [ |- D]
;

LF void : type = ;

rec nv_nostep : [ |- numval M] -> [ |- step M M'] -> [ |- void] =
/ total v (nv_nostep _ _ v) /
fn v, s => case v of
| [ |- nv_z]   => impossible s
| [ |- nv_s V] =>
  let [ |- e_succ S] = s in nv_nostep [ |- V] [ |- S]
;

rec val_nostep : [ |- value M] -> [ |- step M M'] -> [ |- void] =
fn w, s => case w of
| [ |- v_tt]    => impossible s
| [ |- v_ff]    => impossible s
| [ |- v_num V] => nv_nostep [ |- V] s
| [ |- v_lam]   => impossible s
;

§16inductive#

The data of the index level describes a formal system. A proof sometimes needs data of its own, describing something that is not a judgment of the system: a correspondence between two contexts, entry by entry, for instance. This section gives the computation level data types defined by their constructors, and states the condition, strict positivity, that keeps such definitions sound.

§16.1 · Why the computation level needs its own types

So far, every type family of the index level has described part of a formal system. Some properties one wishes to prove, however, belong not to the system but to the proof: they are invented for the purpose and involve logical structure that LF deliberately lacks, including nested implications, quantification over computations, and relations between contexts.

The example driving the design is a logical relation. The statement that a term of function type is reducible if, for every reducible argument, the application is reducible, nests an implication inside an implication in a negative position. LF cannot express it, LF's arrow being the weak one while this arrow is an implication between propositions. The computation level therefore has recursive type definitions of its own.

§16.2 · Declaring one

A declaration follows the pattern of an LF one, with inductive in place of LF and ctype in place of type.

inductive CNat : ctype =
| CZ : CNat
| CS : CNat -> CNat
;

inductive Ev : [ |- term] -> ctype =
| ZEv : Ev [ |- z]
| SEv : Ev [ |- N] -> Ev [ |- succ (succ N)]
;

Ev [ |- N] is inhabited exactly when N is an even numeral, and its inhabitants are derivations of that fact: the judgments-as-types idea of §2.4, one level higher. The difference from an LF family is that the arrows here are strong, so a constructor argument may be any computation type, functions included.

rec ev_nv : Ev [ |- N] -> [ |- numval N] =
fn e => case e of
| ZEv   => [ |- nv_z]
| SEv E => let [ |- V] = ev_nv E in [ |- nv_s (nv_s V)]
;

LF void : type = ;

rec ev1 : Ev [ |- succ z] -> [ |- void] =
fn e => impossible e
;

§16.3 · Positivity

The D with Inj : (D -> D) -> D of §6.4 is the standard violation, and the non-terminating omega built from it is why the condition exists.

§16.4 · Mutual definitions

Some definitions refer to each other. A numeral is even when it is zero or the successor of an odd numeral, and odd when it is the successor of an even one, so neither family can be declared before the other. and joins mutually recursive declarations, with the flavour keyword repeated.

inductive Even : [ |- term] -> ctype =
| E_z : Even [ |- z]
| E_s : Odd [ |- N] -> Even [ |- succ N]

and inductive Odd : [ |- term] -> ctype =
| O_s : Even [ |- N] -> Odd [ |- succ N]
;

The same and joins mutually recursive functions, in the form rec f : … = … and rec g : … = …;, with rec repeated in the same way; this is how mutual induction is written. A mutual block may also mix flavours, so that an inductive family may be defined jointly with a coinductive one, as §18.3 shows.

rec ev_even : Ev [ |- N] -> Even [ |- N] =
fn e => case e of
| ZEv   => E_z
| SEv E => E_s (O_s (ev_even E))
;

rec even_ev : Even [ |- N] -> Ev [ |- N] =
fn e => case e of
| E_z         => ZEv
| E_s (O_s E) => SEv (even_ev E)
;

rec even_nv : Even [ |- N] -> [ |- numval N] =
/ total e (even_nv _ e) /
fn e => case e of
| E_z   => [ |- nv_z]
| E_s o => let [ |- V] = odd_nv o in [ |- nv_s V]

and rec odd_nv : Odd [ |- N] -> [ |- numval N] =
/ total o (odd_nv _ o) /
fn o => case o of
| O_s e => let [ |- V] = even_nv e in [ |- nv_s V]
;

§16.5 · Context relations

The following idiom recurs more than any other. Two contexts of different schemas must be related, as vctx and ctx are, one carrying terms and the other terms paired with derivations, and the relation between them is a substitution. An inductive type indexed by both contexts and the substitution expresses exactly that.

inductive CtxR : {f : vctx} {p : ctx} {$s : $[p |- f]} ctype =
| Nil_R  : CtxR [] [] $[ |- ^]
| Cons_R : CtxR [f] [p] $[p |- $s]
           -> CtxR [f, x : term]
                   [p, b : block (x : term, u : oft x T[])]
                   $[p, b |- $s[..], b.x]
;

Reach for this construction where context subsumption, §13.2, does not apply because the two schemas stand in no prefix relation. The cost is the labour of threading the relation through every case. It is the one general tool available, and recognizing early that it is needed saves effort.

rec r1 : CtxR [x : term] [b : block (x : term, u : oft x nat)]
             $[b : block (x : term, u : oft x nat) |- b.x] =
  Cons_R Nil_R;

§17stratified#

Some definitions a proof needs are not strictly positive and are sound all the same, because they are defined by recursion on an index rather than by their own construction. Tait's reducibility predicate, the standard example of a logical relation, is the case at hand. This section shows the definition that inductive refuses and the declaration that accepts it.

§17.1 · A definition that is not strictly positive

Tait's reducibility predicate, the core of his method for proving normalization, runs as follows.

Written as an inductive declaration it is rejected. In the second clause the family appears to the left of an arrow, in Reduce [ |- A] [ |- N] -> …, which is a negative occurrence. The definition is not strictly positive and no reformulation will make it so.

It is nonetheless well-founded, though not by the structure of the predicate. It is well-founded by the type: the recursive occurrences stand at A and B, both strictly smaller than arr A B. Beluga provides a second discipline for exactly this situation.

§17.2 · The declaration

LF mstep : term -> term -> type =
| ms_refl : mstep M M
| ms_step : step M M' -> mstep M' M'' -> mstep M M''
;

LF halts : term -> type =
| halt : mstep M V -> value V -> halts M
;

stratified Reduce : {A : [ |- tp]} {M : [ |- term]} ctype =
| R_nat  : [ |- halts M] -> Reduce [ |- nat] [ |- M]
| R_bool : [ |- halts M] -> Reduce [ |- bool] [ |- M]
| R_arr  : [ |- halts M]
           -> ({N : [ |- term]} Reduce [ |- A] [ |- N]
                -> Reduce [ |- B] [ |- app M N])
           -> Reduce [ |- arr A B] [ |- M]
;

Three observations. The arrows are the strong computation-level arrows and are therefore implications in the ordinary sense. {N : [ |- term]} is a universal quantification over closed terms, as for all reducible N requires. And the result types Reduce [ |- nat] …, Reduce [ |- bool] … and Reduce [ |- arr A B] … exhibit the stratification: the conclusion of each constructor stands at a type strictly larger than the types of its recursive premises.

let rz : Reduce [ |- nat] [ |- z] =
  R_nat [ |- halt ms_refl (v_num nv_z)];

let rb : Reduce [ |- bool] [ |- ite tt ff tt] =
  R_bool [ |- halt (ms_step e_ite_tt ms_refl) v_ff];

rec reduce_halts : Reduce [ |- T] [ |- M] -> [ |- halts M] =
fn r => case r of
| R_nat h   => h
| R_bool h  => h
| R_arr h f => h
;

§17.3 · Choosing between the two

Prefer inductive. Reach for stratified only where positivity fails, and expect to pay for it by restructuring the recursion to proceed by the index.

§18coinductive#

Inductive data is finite: built by constructors and taken apart by matching. Some objects are infinite, streams among them, and are described not by how they are built but by what can be observed of them. This section introduces coinductive types, defined by their observations, and copatterns, which define their values.

§18.1 · Definition by observation

An inductive type is defined by how its values are built, by a list of constructors. A coinductive type is defined by how its values are observed, by a list of destructors. The latter is the right notion for infinite data. A stream cannot be built in finitely many steps, but it can be observed: it has a head and a tail.

coinductive Stream : ctype =
| Hd : Stream :: [ |- term]
| Tl : Stream :: Stream
;

Read Hd : Stream :: [ |- term] as: observing a Stream with Hd yields a [ |- term]. These are observations, also called destructors. The :: belongs to coinductive declarations and appears nowhere else.

§18.2 · Copatterns and fun

If a type is defined by its observations, a value of that type is defined by saying what each observation returns. That is a copattern, and fun is the construct taking them.

rec cycle : [ |- term] -> Stream =
fun e .Hd => e
  | [ |- z] .Tl => cycle [ |- succ z]
  | e .Tl       => cycle [ |- z]
;

The left-hand side of a clause mixes ordinary patterns, for the function's arguments, with observations, prefixed by a dot. The clause fun e .Hd => e says that, given argument e, the Hd observation is e. Observations are applied postfix with a dot, so (cycle [ |- z]) .Tl .Hd is the second element.

rec repeat : [ |- term] -> Stream =
fun e .Hd => e
  | e .Tl => repeat e
;

rec nats : [ |- term] -> Stream =
fun e .Hd => e
  | e .Tl => let [ |- N] = e in nats [ |- succ N]
;

rec second : Stream -> [ |- term] =
fn s => s .Tl .Hd
;

rec smap : ([ |- term] -> [ |- term]) -> Stream -> Stream =
fun f s .Hd => f (s .Hd)
  | f s .Tl => smap f (s .Tl)
;

§18.3 · Inductive and coinductive types together

The standard way of expressing a potentially infinite list is a pair of mutually recursive definitions: an inductive one for the shape of a single step, a coinductive one for the unfolding.

inductive MuColist : ctype =
| CNil  : MuColist
| CCons : [ |- term] -> NuColist -> MuColist

and coinductive NuColist : ctype =
| Out : NuColist :: MuColist
;

Coinduction in Beluga supports substantial work. Published developments include bisimilarity for the π-calculus and a mechanization of Howe's method establishing that bisimilarity in a call-by-name calculus with lists is a precongruence, a proof requiring inductive reasoning over syntax and coinductive reasoning over transitions within one development. §27 develops a small case in full, and says what Beluga checks of it.

rec cnil : NuColist =
fun .Out => CNil
;

rec zeros : NuColist =
fun .Out => CCons [ |- z] zeros
;

§19Further features#

Six features complete the language. None adds to what can be expressed; each makes a development easier to write, read or check: abbreviations for types, modules, operators, holes for unfinished code, queries that run a signature as a logic program, and pragmas that adjust checking.

§19.1 · typedef

An abbreviation for a computation type, transparent: it is the type it abbreviates rather than a new one, as an OCaml abbreviation such as type point = int * int is.

typedef Pred : ctype = [ |- term] -> [ |- term];

The idiom justifying the construct is an environment or a map, as in typedef Map : {g : tctx} {h : ctx} ctype = {T : [ |- tp]} TmVar [g] [ |- T] -> Sem [h] [ |- T];, a type whose definition quantifies and which would be unreadable inlined at every use.

rec twice : Pred -> Pred =
fn f => fn m => f (f m)
;

§19.2 · Modules

A development with several object languages needs their names kept apart, so that the z of one does not collide with the z of another. Modules group declarations under a name, as in ML.

module Nats = struct
  nat : type.
  z : nat.
  s : nat -> nat.

  rec suc : [ |- nat] -> [ |- nat] =
  fn n => let [ |- N] = n in [ |- s N];

  let two = [ |- s (s z)];
end;

--abbrev Nats NS.

let nx = [ |- NS.z];

Components are reached as Module.name, and --open Nats. makes them available unqualified. Opening is transitive: if B is opened within A, opening A also opens B.

An abbreviation is a name like any other, and it takes the name over. After --abbrev Nats N., N denotes the module for the rest of the file, and a later metavariable called N, as in [ |- numval N], is refused with the complaint that N is a bound module. Hence the NS above.

rec dbl : [ |- NS.nat] -> [ |- NS.nat] =
fn n => case n of
| [ |- NS.z]   => [ |- NS.z]
| [ |- NS.s N] => let [ |- M] = dbl [ |- N] in [ |- NS.s (NS.s M)]
;

§19.3 · Operators

A two-argument LF constructor can be made infix and a one-argument constructor prefix or postfix. The pragma follows the declaration and names it.

LF nat : type =
| z    : nat
| succ : nat -> nat
;

LF bool : type =
| true  : bool
| false : bool
| conj  : bool -> bool -> bool
;

--infix conj 5 left.
--prefix succ 8.
--assoc right.
--name bool B b.

Precedence is a natural number, with higher numbers binding more tightly; associativity is left, right or none. The order matters. --infix conj 5 left. is correct and --infix conj left 5. is not, the parser reading an optional integer before an optional associativity. There is also --postfix name [precedence]. for a one-argument constructor applied after its argument. --assoc sets the default associativity for operators that declare none; in its absence the default is none. Prefix operators default to precedence −1, which binds very loosely.

--name is unrelated to operators. It sets the preferred name bases for variables Beluga must invent for the family in question: the first identifier for metavariables, the optional second for computation variables. So --name bool B b. causes generated output to read B, B1 and b, b1 rather than something arbitrary. The effect is purely cosmetic and worth setting, as it makes Harpoon's subgoals markedly easier to read.

§19.4 · Holes

Two different constructs are called holes, and they behave differently.

A ? hole synthesizes nothing and can appear only where typechecking is possible. In particular [g |- ?] is often not reconstructible, there being nothing against which to check the hole.

A hole also changes what Beluga does with the rest of the file. The declarations after it are typechecked, but their lets are not evaluated, so a value that would fail when computed, a call that matches no branch for instance, passes without complaint until the hole is filled. Declarations before the hole are evaluated as usual.

rec sketch : [ |- term] -> [ |- term] =
fn n => ?goal
;

§19.5 · Queries

An LF signature is a logic program, and Beluga will run it. A --query pragma asks for inhabitants of a type.

--query 1 * D : oft (succ z) nat.

Beluga searches for terms of the stated type, prints each solution it finds, here D = t_succ t_z, and compares their number with the number declared. A mismatch is reported as a query error, Wrong number of solutions. In the Beluga this book was checked against the error is reported and not fatal, the file still being accepted, so a query used as a test must be read as well as run. The declaration --query 1 * D : oft (lam T (\x. x)) S. asserts that the identity function has exactly one type modulo the metavariables, and reports an error if the signature drifts. The engine is enabled by default and can be disabled with -logic.

--query 1 * D : oft (iszero z) T.

§19.6 · Pragmas affecting checking

Some pragmas change not what a file says but how it is checked.

§20Totality#

Under the Curry–Howard reading, which takes types as propositions and programs as their proofs (§5), a function of type τ is a proof of τ, provided it is total. A function that loops on some input, or that has no branch for some input, inhabits its type so far as the typechecker is concerned and proves nothing. Two further properties must therefore be established: that every input is handled by some case, and that every recursive call terminates.

§20.1 · Coverage

Coverage checking is exhaustiveness checking generalized to higher-order data. It verifies that every closed object of the scrutinee's type is an instance of some pattern, and reports the cases omitted, after the manner of an ML compiler's warning.

For contextual data, coverage performs work that has no analogue in ML. Given a scrutinee of type [g |- term] it must generate one case per constructor of term and one case for each shape of variable the schema of g allows. It consults subordination, §13.3, to exclude cases that cannot arise, so a strengthened pattern is accepted where subordination shows that the discarded assumptions could not have contributed.

§20.2 · Termination

The programmer declares which argument decreases; Beluga checks that every recursive call respects the declaration. It is written between the = and the body.

rec nv_nat : [ |- numval N] -> [ |- oft N nat] =
/ total v (nv_nat _ v) /
fn v => case v of
| [ |- nv_z]   => [ |- t_z]
| [ |- nv_s V] => let [ |- D] = nv_nat [ |- V] in [ |- t_succ D]
;

The function is the lemma of §5.1, its induction now declared. The ordering is the structural subterm ordering: V is a subterm of nv_s V, so the call is accepted. The check is not a heuristic. Beluga generates the set of valid recursive calls when it splits the measured argument, and then verifies that only those calls occur.

For a stratified type the value cannot be measured, so the index is measured instead. In the weak-normalization development of §23 the main lemma is declared / total m (main g a s m) /, an induction on the term M, which is the fourth parameter: the context g is explicit and first, then two implicit arguments inserted by reconstruction, then M.

rec ms_trans : [ |- mstep M M'] -> [ |- mstep M' M'']
               -> [ |- mstep M M''] =
/ total d (ms_trans _ _ _ d) /
fn d, e => case d of
| [ |- ms_refl]     => e
| [ |- ms_step S D] =>
  let [ |- F] = ms_trans [ |- D] e in [ |- ms_step S F]
;

rec nvoft : (g : vctx) [g |- numval N] -> [g |- oft N nat] =
/ total v (nvoft _ _ v) /
fn v => case v of
| [g |- nv_z]   => [g |- t_z]
| [g |- nv_s V] =>
  let [g |- D] = nvoft [g |- V] in [g |- t_succ D]
;

rec ack : CNat -> CNat -> CNat =
/ total {m n} (ack m n) /
fn m, n => case m of
| CZ    => CS n
| CS m' =>
  (case n of
   | CZ    => ack m' (CS CZ)
   | CS n' => ack m' (ack m n'))
;

§20.3 · What a successful check establishes

Precision is called for about what a successful run of the checker establishes, there being three strengths and an easy temptation to conflate them.

The last row is the one most easily forgotten. The commonest way of proving the wrong thing in any proof assistant is to state the wrong type, and no checker can detect it. Reading one's own theorem statement back slowly, with the elaborated form in view, is part of the work.

rec stays : [ |- oft M T] -> [ |- step M M'] -> [ |- oft M T] =
/ total /
fn d, s => d
;

§20.4 · How a false proof can be accepted

rec assumed : [ |- term] -> [ |- term] =
/ trust /
fn n => n
;

rec bogus : {M : [ |- term]} [ |- oft M nat] =
/ trust /
mlam M => bogus [ |- M]
;

§20.5 · Checklist

Before a development is considered finished:

• --coverage appears at the head of the file.
• Every rec stating a theorem carries a / total … / written before the proof, describing the intended induction.
• No / trust / remains, or each remaining occurrence is documented as an assumption.
• No ? holes remain.
• Each theorem's type has been read back and says what was meant, implicit arguments included.

§21Interactive proving#

Every proof so far has been written as a program, in one piece. Harpoon, Beluga's interactive prover, builds the same program one step at a time: it displays the goal, and each of its proof tactics corresponds to a step of an informal proof. This section describes its structure, its prompt and tactics, its automation, the proof scripts it records, and a session from start to finish.

§21.1 · Structure

Harpoon is a separate binary. It loads a Beluga signature and allows proofs to be developed by applying tactics to subgoals. Behind the scenes it builds a proof script, writes it back into the signature file as a proof declaration, and can translate it into an ordinary Beluga program.

Two features of the arrangement matter. The proof object is primary: one is always building a program rather than manipulating an opaque proof state, and the program can be inspected at any point. And a proof developed interactively is covering by construction, since the tactic that splits a variable generates the cases from the coverage algorithm itself.

The structure is hierarchical. A Harpoon run holds sessions, a session holds theorems, and a theorem holds subgoals. A theorem with no subgoals is complete, and a session with no theorems is complete.

§21.2 · The prompt

Starting Harpoon with harpoon --sig file.bel runs a configuration wizard asking for the name of the theorem, its statement, and the induction order, and then presents the subgoal prompt. The prompt has three parts.

Theorem: pres
intros
Meta-context:
  M : ( |- term) (not in scope)
  A : ( |- tp) (not in scope)
  M' : ( |- term) (not in scope)
Computational context:
  x : [ |- oft M A]
  x1 : [ |- step M M']
--------------------------------------------------------------------------------
[ |- oft M' A]
>

1. The label, here intros, under the name of the theorem. It records the position of this subgoal within the proof and grows as work proceeds, becoming for instance intros <- split [ |- X1] (case arr). It is how subgoals are told apart.
2. The two contexts. The meta-context holds metavariables and the computational context holds computation variables, making the distinction of §3.2 visible. The annotation (not in scope) marks implicit parameters, which exist and appear in types but cannot be referred to, as §4.3 explains.
3. The goal, below the line. The task is to construct something of that type.

§21.3 · The tactics

Harpoon's tactics divide into those advancing the proof and those managing the prover. The proof tactics correspond one for one with informal proof steps, which is the design: there are few of them, and each is a move already familiar from paper.

suffices is the tactic that makes large steps readable. It requires that EXP synthesize a type of the form {X1 : U1} … {Xn : Un} tau_1 -> … -> tau_k -> tau, which is the shape of nearly every lemma. A type may be written _ where Harpoon can infer it from the goal and the others, as in suffices by pres toshow [ |- oft M1 T], _ of §21.7. The expression must be a lemma: given the theorem being proved, Harpoon replies that inductive use of suffices by is not currently supported, and the induction hypothesis is applied forward, with by. The tactic is in principle redundant with solve, since the whole term could always be written out, but the arguments would then have to be written as Beluga terms rather than constructed interactively. For a lemma with complicated arguments that is the difference between a pleasant proof and an unbearable one.

§21.4 · Automation

Four automations run whenever a new subgoal is created. Each can be toggled, and anything they do can be undone.

When auto-solve-trivial declines for that reason it says so, naming the solution it would have used: after the invert of Exercise 21.2, Harpoon reports that the subgoal could be solved automatically by solve [ |- X1], and adds, “However, this would complete the theorem.”

The depth bound can be read off an example. Solving Ev [ |- succ (succ (succ (succ z)))] against the Ev of §16.2 requires depth 2: the goal focuses on SEv, yielding Ev [ |- succ (succ z)] at depth 1, which focuses on SEv again, yielding Ev [ |- z] at depth 2, closed by ZEv. Where a goal produces several subgoals, the depth increments by 1 for the group.

§21.5 · Proof scripts

A proof, finished or partial, resides in the signature as a proof declaration. Its body is the script, a structured record of the tactics in which each case states its meta-context and computational context before a ; and then its tactics.

The script below works in a signature of its own, smaller than the language of Part three so that the session of §21.6 stays short: two types and the structural equality on them, with a constructor for each way of building a type.

LF tp : type =
| base : tp
| arr  : tp -> tp -> tp
;

LF eq : tp -> tp -> type =
| eq_base : eq base base
| eq_arr  : eq A1 A2 -> eq B1 B2 -> eq (arr A1 B1) (arr A2 B2)
;

proof tp-refl : {A : [ |- tp]} [ |- eq A A] =
/ total 1 /
intros
{ A : ( |- tp)
| ; split [ |- A] as
  case arr:
  { X : ( |- tp), X1 : ( |- tp)
  | ; by tp-refl [ |- X] as EQ_X unboxed;
      by tp-refl [ |- X1] as EQ_X1 unboxed;
      solve [ |- eq_arr EQ_X EQ_X1]
  }
  case base:
  { | ; solve [ |- eq_base] }
}
;

Harpoon translates a completed script into an ordinary Beluga program, does so automatically, and then typechecks the translation. Proving interactively and reading the generated program afterwards is the most reliable way to learn how the substitutions of Part four are meant to go.

§21.6 · A session, step by step

Reflexivity of structural equality on types. The signature is that of §21.5; the theorem is {A : [ |- tp]} [ |- eq A A], with induction order 1.

Two things are visible in that run. The split produced two cases and Harpoon worked them in its own order, relabelling as it went. And the appeals to the induction hypothesis were written by tp-refl [ |- X] as EQ_X unboxed, the unboxed modifier being required because the result is wanted as a metavariable, usable inside the box that eventually solves the goal.

§21.7 · Practice

The session of §21.6 used three tactics. The three sessions below, in the language of Parts three to six, use the others a proof most often needs: induction with the hypothesis applied by by, a case analysis whose impossible cases must be closed one by one, and backward reasoning with suffices. Each is Harpoon's own output, replayed from the tactics shown at the top of each step. The exercises that follow are proofs to carry out the same way; each answer gives the tactics and the script Harpoon writes.

Induction

The lemma of §20.2, that a numeral has type nat, by induction on the derivation that it is a numeral. The statement is [ |- numval N] -> [ |- oft N nat], with induction order 1.

Cases that cannot arise

The lemma of §22.2 on values of type bool: such a value is tt or ff. Most of its cases are impossible, and Harpoon has to be shown each one. The statement is [ |- oft M bool] -> [ |- value M] -> [ |- boolval M], with no induction.

Reasoning backwards

Preservation over two steps, from preservation over one (§22.1), with no induction: the conclusion of pres matches the goal, so it suffices to provide the premises of pres. The statement is [ |- oft M T] -> [ |- step M M1] -> [ |- step M1 M2] -> [ |- oft M2 T].

invert x
solve [ |- X1]

proof inv-isz : [ |- oft (iszero M) T] -> [ |- oft M nat] =
/ total /
intros
{ M : ( |- term), T : ( |- tp)
| x : [ |- oft (iszero M) T]
; split x as
  case t_isz:
  { M : ( |- term), X1 : ( |- oft M nat)
  | x : [ |- oft (iszero M) bool]
  ; solve [ |- X1]
  }
}
;

split x
by ev-nv x1 as V unboxed
solve [ |- nv_s (nv_s V)]
solve [ |- nv_z]

proof ev-nv : Ev [ |- N] -> [ |- numval N] =
/ total 1 /
intros
{ N : ( |- term)
| x : Ev [ |- N]
; split x as
  case SEv:
  { N1 : ( |- term)
  | x : Ev [ |- succ (succ N1)], x1 : Ev [ |- N1]
  ; by ev-nv x1 as V unboxed;
    solve [ |- nv_s (nv_s V)]
  }
  case ZEv:
  {
  | x : Ev [ |- z]
  ; solve [ |- nv_z]
  }
}
;

split x1
by pres x [ |- X3] as y
solve mpres y [ |- X4]

proof mpres : [ |- oft M T] -> [ |- mstep M M2]
             -> [ |- oft M2 T] =
/ total 2 /
intros
{ M : ( |- term), T : ( |- tp), M1 : ( |- term)
| x : [ |- oft M T], x1 : [ |- mstep M M1]
; split x1 as
  case ms_step:
  { M : ( |- term),
    T : ( |- tp),
    M1 : ( |- term),
    X1 : ( |- term),
    X3 : ( |- step M X1),
    X4 : ( |- mstep X1 M1)
  | x : [ |- oft M T], x1 : [ |- mstep M M1]
  ; by pres x [ |- X3] as y;
    solve mpres y [ |- X4]
  }
  case ms_refl:
  { M1 : ( |- term), T : ( |- tp)
  | x : [ |- oft M1 T], x1 : [ |- mstep M1 M1]
  ; solve x
  }
}
;

split x
by nvoft [_ |- X1] as D unboxed
solve [_ |- t_succ D]
solve [_ |- t_z]

proof nvoft : (g : vctx) [g |- numval N] -> [g |- oft N nat] =
/ total 1 /
intros
{ g : vctx, N : (g |- term)
| x : [g |- numval N]
; split x as
  case nv_s:
  { g : vctx, X : (g |- term), X1 : (g |- numval X)
  | x : [g |- numval (succ X)]
  ; by nvoft [_ |- X1] as D unboxed;
    solve [_ |- t_succ D]
  }
  case nv_z:
  { g : vctx
  | x : [g |- numval z]
  ; solve [_ |- t_z]
  }
}
;

§22Type safety#

This section proves type safety for the language of Part three: a well-typed term either is a value or can take a step, and taking a step preserves its type. Part two proved both for the arithmetic expressions, progress in §5.4 and preservation as Exercise 5.3. The proofs here are those, extended by the cases for abstraction and application, and those cases are the whole of what is new. Both theorems concern closed terms, as the empty contexts in their types say. The signature is the one §7 declared, and the development continues it. Type uniqueness, the standard exercise in contexts, was given in full in §11.4.

§22.1 · Preservation

Induction on the typing derivation, then a case on the step, as in Exercise 5.3. Values do not step, and an abstraction is a value, so the cases t_tt, t_ff, t_z and t_lam are closed by impossible s. The cases for the arithmetic are those of Exercise 5.3. An application has three rules to consider.

rec pres : [ |- oft M T] -> [ |- step M M'] -> [ |- oft M' T] =
/ total d (pres _ _ _ d) /
fn d, s => case d of
| [ |- t_tt] => impossible s
| [ |- t_ff] => impossible s
| [ |- t_z]  => impossible s
| [ |- t_lam \x.\u. D] => impossible s
| [ |- t_ite D1 D2 D3] =>
  (case s of
   | [ |- e_ite_tt] => [ |- D2]
   | [ |- e_ite_ff] => [ |- D3]
   | [ |- e_ite S]  =>
     let [ |- D1'] = pres [ |- D1] [ |- S] in
     [ |- t_ite D1' D2 D3])
| [ |- t_succ D] =>
  let [ |- e_succ S] = s in
  let [ |- D'] = pres [ |- D] [ |- S] in [ |- t_succ D']
| [ |- t_pred D] =>
  (case s of
   | [ |- e_pred_z]   => [ |- t_z]
   | [ |- e_pred_s V] =>
     let [ |- t_succ D'] = [ |- D] in [ |- D']
   | [ |- e_pred S]   =>
     let [ |- D'] = pres [ |- D] [ |- S] in [ |- t_pred D'])
| [ |- t_isz D] =>
  (case s of
   | [ |- e_isz_z]   => [ |- t_tt]
   | [ |- e_isz_s V] => [ |- t_ff]
   | [ |- e_isz S]   =>
     let [ |- D'] = pres [ |- D] [ |- S] in [ |- t_isz D'])
| [ |- t_app D1 D2] =>
  (case s of
   | [ |- e_app_1 S] =>
     let [ |- D1'] = pres [ |- D1] [ |- S] in [ |- t_app D1' D2]
   | [ |- e_app_2 W S] =>
     let [ |- D2'] = pres [ |- D2] [ |- S] in [ |- t_app D1 D2']
   | [ |- e_app_abs W] =>
     let [ |- t_lam \x.\u. D0] = [ |- D1] in
     [ |- D0[_, D2]])
;

The first two rules for application are congruences, and their cases recurse on the subderivation that stepped. The third, e_app_abs, is the substantive case. Step by step:

1. [ |- e_app_abs W] refines M to app (lam T M0) N and M' to M0 N, for some body M0 and argument N, with W deriving value N.
2. d was matched as t_app D1 D2, so D1 types the abstraction, oft (lam T M0) (arr A B), and D2 types the argument, oft N A.
3. Only t_lam concludes the typing of an abstraction, so the let is an inversion. It gives D0, a typing derivation for the body, open in the parameter x and its assumption u : oft x A.
4. D0[_, D2] maps x to the argument and u to D2, the derivation that the argument has type A, producing a closed derivation of oft (M0 N) B, which is what was required. The _ is the argument term, which reconstruction reads off the type of D2. Written the other way round, D0[D2, _], it is refused: a derivation cannot stand where a term is expected.

§22.2 · Progress

As in §5.4, progress must know, of a value whose type is known, which value it is. The lemma on forms of values gains a clause for the arrow: a value of type A ⇒ B is an abstraction. The answer is packaged as in §5.4 and declared again, this being a different development, together with what the lemma returns: boolval as before, and lamval, which says that a term is some abstraction.

LF progress : term -> type =
| p_val  : value M -> progress M
| p_step : step M M' -> progress M
;

LF boolval : term -> type =
| bv_tt : boolval tt
| bv_ff : boolval ff
;

LF lamval : term -> type =
| lv : lamval (lam T M)
;

rec cf_nat : [ |- oft M nat] -> [ |- value M]
             -> [ |- numval M] =
fn d, w => case w of
| [ |- v_tt]    => impossible d
| [ |- v_ff]    => impossible d
| [ |- v_lam]   => impossible d
| [ |- v_num V] => [ |- V]
;

rec cf_bool : [ |- oft M bool] -> [ |- value M]
              -> [ |- boolval M] =
fn d, w => case w of
| [ |- v_tt]    => [ |- bv_tt]
| [ |- v_ff]    => [ |- bv_ff]
| [ |- v_lam]   => impossible d
| [ |- v_num V] =>
  (case [ |- V] of
   | [ |- nv_z]    => impossible d
   | [ |- nv_s V'] => impossible d)
;

rec cf_arr : [ |- oft M (arr A B)] -> [ |- value M]
             -> [ |- lamval M] =
fn d, w => case w of
| [ |- v_tt]    => impossible d
| [ |- v_ff]    => impossible d
| [ |- v_lam]   => [ |- lv]
| [ |- v_num V] =>
  (case [ |- V] of
   | [ |- nv_z]    => impossible d
   | [ |- nv_s V'] => impossible d)
;

The cases closed by impossible are those in which the form of the value contradicts the type, such as tt at type nat or an abstraction at type bool. A numeral needs one step more. In cf_bool and cf_arr, closing the case v_num V at once with impossible d is refused, the type of d being reported "(possibly) inhabited": v_num V says only that M is some numeral, and nothing yet says which. Splitting V says which, and in each of its two cases the type of d is empty. §5.4 did the same work with a lemma returning the empty type; here the split does it in place.

rec prog : [ |- oft M T] -> [ |- progress M] =
/ total d (prog _ _ d) /
fn d => case d of
| [ |- t_tt] => [ |- p_val v_tt]
| [ |- t_ff] => [ |- p_val v_ff]
| [ |- t_z]  => [ |- p_val (v_num nv_z)]
| [ |- t_lam \x.\u. D] => [ |- p_val v_lam]
| [ |- t_succ D] =>
  (case prog [ |- D] of
   | [ |- p_val W]  =>
     let [ |- V] = cf_nat [ |- D] [ |- W] in
     [ |- p_val (v_num (nv_s V))]
   | [ |- p_step S] => [ |- p_step (e_succ S)])
| [ |- t_pred D] =>
  (case prog [ |- D] of
   | [ |- p_val W]  =>
     (case cf_nat [ |- D] [ |- W] of
      | [ |- nv_z]   => [ |- p_step e_pred_z]
      | [ |- nv_s V] => [ |- p_step (e_pred_s V)])
   | [ |- p_step S] => [ |- p_step (e_pred S)])
| [ |- t_isz D] =>
  (case prog [ |- D] of
   | [ |- p_val W]  =>
     (case cf_nat [ |- D] [ |- W] of
      | [ |- nv_z]   => [ |- p_step e_isz_z]
      | [ |- nv_s V] => [ |- p_step (e_isz_s V)])
   | [ |- p_step S] => [ |- p_step (e_isz S)])
| [ |- t_ite D1 D2 D3] =>
  (case prog [ |- D1] of
   | [ |- p_val W]  =>
     (case cf_bool [ |- D1] [ |- W] of
      | [ |- bv_tt] => [ |- p_step e_ite_tt]
      | [ |- bv_ff] => [ |- p_step e_ite_ff])
   | [ |- p_step S] => [ |- p_step (e_ite S)])
| [ |- t_app D1 D2] =>
  (case prog [ |- D1] of
   | [ |- p_step S]  => [ |- p_step (e_app_1 S)]
   | [ |- p_val W1] =>
     (case prog [ |- D2] of
      | [ |- p_step S]  => [ |- p_step (e_app_2 W1 S)]
      | [ |- p_val W2] =>
        let [ |- lv] = cf_arr [ |- D1] [ |- W1] in
        [ |- p_step (e_app_abs W2)]))
;

An abstraction is a value. An application asks for the progress of its function, then of its argument, in the order the evaluation rules impose: a step in either is a step of the whole, by e_app_1 or e_app_2, and when both are values cf_arr says the function is an abstraction, so e_app_abs applies. The let against lv, the only constructor of lamval, is what tells the typechecker so, as matching against e_ref did in §11.4: without it, e_app_abs W2 does not typecheck, since nothing has said that the function is an abstraction. That is the one case in which the form of a value at arrow type is needed, and it is why the lemma has that clause.

Both functions are declared total and both pass with coverage on, which is §20.3's strongest standard: together they are type safety for the language.

rec mpres : [ |- oft M T] -> [ |- mstep M M'] -> [ |- oft M' T] =
/ total s (mpres _ _ _ d s) /
fn d, s => case s of
| [ |- ms_refl]      => d
| [ |- ms_step S S'] => mpres (pres d [ |- S]) [ |- S']
;

rec safe : [ |- oft M T] -> [ |- mstep M M']
           -> [ |- progress M'] =
fn d, s => prog (mpres d s)
;

§23Weak normalization by logical relations#

This development justifies the parts of the language that appeared exotic: stratified types, substitution variables, and the equational theory of simultaneous substitution. Proofs by logical relations are the standard hard case for any system reasoning about binders, and they are what Beluga was built to make tractable.

Direct induction on M fails, β-reduction being capable of enlarging a term. Tait's method replaces the goal with a stronger, type-indexed one.

§23.1 · The system

Two things change from the language of Part three. The second, the encoding of typing, is a choice every Beluga development must make.

The first is size. The language is cut down to its functional core: one base type b with one constant c, abstraction and application. The arithmetic would add cases to every lemma and no ideas to the proof. Evaluation is call-by-name β-reduction, as in the distribution's development, so beta asks nothing of the argument.

The second is the encoding of typing. Until now terms were untyped syntax and typing a separate judgment over them, oft: the extrinsic encoding, in which a term may or may not have a type. That suited type safety and type uniqueness, which are statements about the typing judgment. A logical relation is a predicate on well-typed terms, defined by recursion on their types, and its main lemma is proved by induction on typing. With untyped terms and a separate judgment, the context of that lemma holds a typing assumption beside every variable, as the schema ctx of §11 does, so a substitution closing it must supply a typing derivation for every term it substitutes, beside the term. The intrinsic encoding removes the second component: the term family is indexed by the type, so that a term of tm A is a term of type A and there is no other kind.

In exchange, typing is no longer a judgment one can state things about: type uniqueness has nothing to say about tm, each term having its type by construction. Both encodings are standard, and the choice follows the theorem. §17 wrote reducibility over the extrinsic terms of Part three, to show the declaration; the proof below is the reason to prefer the intrinsic one.

So here terms are intrinsically typed: the type is an index of the term family, ill-typed terms are not representable, and the typing judgment requires no separate definition.

LF tp : type =
| b   : tp
| arr : tp -> tp -> tp
;

LF tm : tp -> type =
| app : tm (arr T S) -> tm T -> tm S
| lam : (tm T -> tm S) -> tm (arr T S)
| c   : tm b
;

LF step : tm A -> tm A -> type =
| beta    : step (app (lam M) N) (M N)
| stepapp : step M M2 -> step (app M N) (app M2 N)
;

LF mstep : tm A -> tm A -> type =
| refl    : mstep M M
| onestep : step M M2 -> mstep M2 M3 -> mstep M M3
;

LF val : tm A -> type =
| val/c   : val c
| val/lam : val (lam M)
;

LF halts : tm A -> type =
| halts/m : mstep M M2 -> val M2 -> halts M
;

let t : [ |- tm b] = [ |- app (lam \x. x) c];

§23.2 · Reducibility

The predicate, on paper:

This cannot be an LF family, requiring an implication in a negative position where LF's arrow is the weak one, §1.2. It cannot be inductive, the negative occurrence violating positivity. It is stratified, by the type index.

stratified Reduce : {A : [ |- tp]} {M : [ |- tm A]} ctype =
| I   : [ |- halts M] -> Reduce [ |- b] [ |- M]
| Arr : [ |- halts M]
        -> ({N : [ |- tm A]} Reduce [ |- A] [ |- N]
             -> Reduce [ |- B] [ |- app M N])
        -> Reduce [ |- arr A B] [ |- M]
;

The recursive occurrences in Arr stand at A and B, both smaller than arr A B. That is the stratification, and it is why A must be an explicit index: functions over Reduce will induct on it.

§23.3 · The small lemmas

Three facts that a paper proof dispatches in a clause must be written down here, though each takes only a few lines.

rec halts_step : {S : [ |- step M M2]} [ |- halts M2]
                 -> [ |- halts M] =
/ total (halts_step) /
mlam S => fn h =>
  let [ |- halts/m MS V] = h in
  [ |- halts/m (onestep S MS) V]
;

rec bwd_closed' : {A : [ |- tp]} {M : [ |- tm A]}
                  {M2 : [ |- tm A]} {S : [ |- step M M2]}
                  Reduce [ |- A] [ |- M2]
                  -> Reduce [ |- A] [ |- M] =
/ total a (bwd_closed' a) /
mlam A, M, M2 => mlam MS => fn r => case [ |- A] of
| [ |- b] => let I ha = r in I (halts_step [ |- MS] ha)
| [ |- arr A1 B] =>
  let Arr ha f = r in
  Arr (halts_step [ |- MS] ha)
    (mlam N => fn rn =>
     bwd_closed' [ |- B] _ _ [ |- stepapp MS] (f [ |- N] rn))
;

rec bwd_closed : {S : [ |- step M M2]} Reduce [ |- A] [ |- M2]
                 -> Reduce [ |- A] [ |- M] =
/ total (bwd_closed) /
mlam S => fn r =>
  let [ |- S] : [ |- step M M2] = [ |- S] in
  let [ |- M] : [ |- tm A] = [ |- M] in
  bwd_closed' [ |- A] [ |- M] [ |- M2] [ |- S] r
;

rec reduce_halts : Reduce [ |- T] [ |- M] -> [ |- halts M] =
/ total (reduce_halts) /
fn r => case r of
| I h     => h
| Arr h f => h
;

bwd_closed' is the one to read. It proceeds by cases on the type A, which is explicit so that it can be measured, / total a (bwd_closed' a) /, and inverts the Reduce value in each case. In the case of an arrow type it must produce a new function, so it builds one with mlam N => fn rn => … and recurses at the range type B, pushing the step into the function position with stepapp. bwd_closed is the same lemma with A, M and M2 left implicit: it names them with the annotated lets and calls bwd_closed', and, not being recursive, needs no measure.

let r : Reduce [ |- b] [ |- app (lam \x. x) c] =
  bwd_closed [ |- beta] (I [ |- halts/m refl val/c]);

rec halts_mstep : [ |- mstep M M2] -> [ |- halts M2]
                  -> [ |- halts M] =
/ total ms (halts_mstep _ _ _ ms) /
fn ms, h => case ms of
| [ |- refl]         => h
| [ |- onestep S MS] =>
  halts_step [ |- S] (halts_mstep [ |- MS] h)
;

§23.4 · Reducible substitutions

The main lemma cannot concern closed terms alone. Getting beneath a lambda means speaking of open terms, and then of substitutions that close them. Both halves of Part four are required.

schema ctx = tm T;

inductive RedSub : {g : ctx} {$s : $[ |- g]} ctype =
| Nil : RedSub [ ] $[ |- ^]
| Dot : RedSub [g] $[ |- $s[^]] -> Reduce [ |- A] [ |- M]
        -> RedSub [g, x : tm A[]] $[ |- $s, M]
;

Dot reads as the informal definition reads: R_Γ,x:A = { σ,N/x | σ ∈ R_Γ and N ∈ R_A }. The A[] weakens the closed type A into g, by §9.2. This definition is strictly positive, hence inductive, and a function may therefore recurse on it. lookup, below, recurses on the context instead, which shrinks in step with it.

rec lookup : {g : ctx} {#p : #[g |- tm A[]]}
             RedSub [g] $[ |- $s[^]]
             -> Reduce [ |- A] [ |- #p[$s]] =
/ total g (lookup g) /
mlam g => mlam #p => fn rs => case [g] of
| [] => impossible [ |- #p]
| [g2, x : tm A] =>
  (case [g2, x : tm A |- #p] of
   | [g2, x : tm A |- x]      => let Dot rs2 rN = rs in rN
   | [g2, x : tm A |- #q[..]] => let Dot rs2 rN = rs in
                                 lookup [g2] [g2 |- #q] rs2)
;

Two cases, and the distinction between them is what parameter variables exist for. Either #p is the last variable of the context, matching [g2, x : tm A |- x], in which case the corresponding entry is the one at the end of the substitution and the second argument of Dot is the required proof. Or #p is one of the earlier variables, matching [g2, x : tm A |- #q[..]], where the [..] establishes that #q lives in g2 and so cannot be x, in which case the recursion proceeds on the shorter context.

§23.5 · The main lemma

rec main : {g : ctx} {M : [g |- tm A[]]} RedSub [g] $[ |- $s[^]]
           -> Reduce [ |- A] [ |- M[$s]] =
/ total m (main g a s m) /
mlam g => mlam M => fn rs => case [g |- M] of
| [g |- #p] => lookup [g] [g |- #p] rs

| [g |- lam (\x. M1)] =>
  Arr [ |- halts/m refl val/lam]
    (mlam N => fn rN =>
     bwd_closed [ |- beta]
       (main [g, x : tm _] [g, x |- M1] (Dot rs rN)))

| [g |- app M1 M2] =>
  let Arr ha f = main [g] [g |- M1] rs in
  f _ (main [g] [g |- M2] rs)

| [g |- c] => I [ |- halts/m refl val/c]
;

Four cases, one for each shape a term in a context can take, with the variable case first because the context exists.

Variable

Apply the lookup lemma. Applying $s to [g |- #p] yields [ |- #p[$s]], which is what lookup returns a proof about.

Application

By the induction hypothesis, M1[$s] is reducible at arr A B. Inverting that with let Arr ha f = … gives the halting proof ha and the function f, whose type is

so applying it to the argument's reducibility proof finishes the case. The underscore in f _ (…) is the explicitly quantified N, recovered by reconstruction.

One step here goes unseen. The goal after the pattern match is Reduce [ |- B] [ |- app M1[$s] M2[$s]] rather than Reduce [ |- B] [ |- (app M1 M2)[$s]]. Beluga pushed the substitution inside the application silently, using the equational theory of simultaneous substitutions. In a hand-rolled development that step is a lemma.

Abstraction

The definition of Reduce at an arrow type requires two things. Halting is immediate, an abstraction already being a value, so halts/m refl val/lam serves. The second obligation is the real work: assume N and a proof rN that it is reducible, and show that app (lam \x. M1[$s,x]) N is reducible.

Appeal to the induction hypothesis on the body, in the extended context, with the substitution extended by N: main [g, x : tm _] [g, x |- M1] (Dot rs rN). That yields Reduce [ |- B] [ |- M1[$s, N]]. The goal differs from it by one β-step, which bwd_closed [ |- beta] bridges.

Concealed in that last sentence is the step most expensive elsewhere. The beta rule produces (\y. M1[$s, y]) N, which is not in normal form, and reaching M1[$s, N] requires composing the single substitution for y with the simultaneous substitution $s, y. That composition is a definitional equality in Beluga, so the two terms are the same term and nothing needs saying. Elsewhere it is a substitution-composition lemma.

§23.6 · The theorem

rec weakNorm : {M : [ |- tm A]} [ |- halts M] =
/ total (weakNorm) /
mlam M => reduce_halts (main [ ] [ |- M] Nil)
;

§23.7 · What the development cost

Count what was written: four LF families for the system, one stratified definition, one inductive definition, one schema, and five functions. No substitution lemma, no renaming lemmas, no weakening or exchange lemmas, no composition lemma, and no well-formedness invariant on contexts.

For the harder relative of this proof, strong normalization with type-directed reductions as posed by the POPLMark Reloaded challenge, published line counts put the Beluga development at roughly the size of the Coq and Agda versions for the proof proper. The difference appears in the supporting material. The Agda version additionally depends on a generic-syntax library of some sixteen hundred lines, and the Coq version carries about two hundred lines of renaming and anti-renaming boilerplate proved with tactic scripts. That supporting material is what Beluga's design removes.

One qualification belongs beside that comparison, and §20.4 says how to find it: search for / trust /. The Beluga development distributed with the system has thirty-seven functions, and one of them, subst_mred, is declared / trust /. It states that a step from N to N' yields reductions from M[.., N] to M[.., N']. Under a binder its recursive call takes M[.., x, y], the body with its two variables exchanged, and the totality checker, which accepts only direct subterms as smaller, does not count it so; the author's comment in the file says as much. Given a measure, Beluga refuses the function ("Recursive call not structurally smaller"); with no annotation it is accepted, because nothing is then checked. The other thirty-six carry measures that Beluga checks.

Where the assumption reaches matters. The development proves two things: that every well-typed term belongs to an inductively defined set of strongly normalizing terms (norm), and that belonging to that set implies strong normalization as originally defined, by accessibility (soundSN). The first is checked in full: with subst_mred and the seven functions that use it removed, the rest of the file still passes, coverage and measures included. The second rests on the asserted lemma.

§24The Church–Rosser theorem#

The untyped calculus of §6 has no types, and its terms need not terminate, so the question of §23, whether evaluation halts, has no general answer there. Another question does: whether the order in which redexes are contracted can change where reduction leads. The Church–Rosser theorem says that it cannot. If a term reduces to two terms, those two reduce to a common one, and as a consequence a term has at most one normal form. This section proves the theorem for β-reduction in that calculus, resuming the development of §6, by the method of Tait and Martin-Löf as Pfenning represented it in LF. The code follows the development in Beluga's distribution, with one lemma restated so that its induction is checked.

The direct route fails. One would like the diamond property for single steps: if M steps to M₁ and to M₂, then M₁ and M₂ step to a common term. It is false, because a step can copy a redex. (λx. x x) ((λy. y) z) steps to ((λy. y) z) ((λy. y) z) by contracting the outer redex and to (λx. x x) z by contracting the inner one, and from the first, two steps are needed to reach z z, which the second reaches in one. Parallel reduction contracts any number of the redexes present in a term in a single step, copies included, and for it the diamond property holds. Since it lies between one step of β-reduction and many, it has the same reflexive and transitive closure, so its confluence is that of β-reduction.

§24.1 · Parallel reduction

M ⇛ M′ holds when M' results from M by contracting some of the redexes present in M, possibly none, all at once. There are three rules besides the case of a variable, which reduces to itself: an application reduces when its parts do (ap); an abstraction when its body does (lm); and a redex (λx. M) N reduces to M'[N'/x] when M ⇛ M′ and N ⇛ N′ (beta). In LF the premises about a body are hypothetical in a variable x and in the assumption that x reduces to itself, which is how the variable case is expressed; the contexts of the development pair each variable with that assumption, in the schema pctx.

LF pred : tm -> tm -> type =
| beta : ({x : tm} pred x x -> pred (M x) (M' x))
         -> pred N N'
         -> pred (app (lam M) N) (M' N')
| ap   : pred M1 M1' -> pred N1 N1'
         -> pred (app M1 N1) (app M1' N1')
| lm   : ({x : tm} pred x x -> pred (M x) (M' x))
         -> pred (lam M) (lam M')
;

schema pctx = block (x : tm, u : pred x x);

Every term reduces to itself in parallel, by contracting nothing. The proof is by induction on the term, and its variable case is the second component of the variable's block.

rec refl : {g : pctx} {M : [g |- tm]} [g |- pred M M] =
/ total m (refl g m) /
mlam g, M => case [g |- M] of
| [g |- #p.1] => [g |- #p.2]
| [g |- lam \x. M1] =>
  let [g, b : block (x : tm, u : pred x x) |- R] =
      refl [g, b : block (x : tm, u : pred x x)]
           [g, b |- M1[.., b.1]]
  in [g |- lm \x.\u. R[.., <x ; u>]]
| [g |- app M1 M2] =>
  let [g |- R1] = refl [g] [g |- M1] in
  let [g |- R2] = refl [g] [g |- M2] in
  [g |- ap R1 R2]
;

let s1 : [ |- pred (app (lam \x. app x (lam \y. y)) (lam \y. y))
                   (app (lam \y. y) (lam \y. y))] =
  [ |- beta (\x.\u. ap u (lm \y.\v. v)) (lm \y.\v. v)];

let s2 : [ |- pred (app (lam \y. y) (lam \y. y)) (lam \y. y)] =
  [ |- beta (\y.\v. v) (lm \y.\v. v)];

§24.2 · The substitution lemma

The lemma the proof turns on: if M ⇛ M′, with x free, and N ⇛ N′, then M[N/x] ⇛ M′[N′/x]. Unlike the substitution lemma of §22.1 it is not an instance of substitution. Substituting for x replaces it by one term throughout, on both sides of the derivation, while here the left side receives N and the right side N'; so the lemma is proved, by induction on the derivation of M ⇛ M′.

rec subst : (g : pctx)
  [g, x : tm, u : pred x x |- pred M[.., x] M'[.., x]]
  -> [g |- pred N N'] -> [g |- pred M[.., N] M'[.., N']] =
/ total d (subst g m m' n n' d) /
fn d, e => case d of
| [g, x : tm, u : pred x x |- u] => e
| [g, x : tm, u : pred x x |- #p.2[..]] => [g |- #p.2]
| [g, x : tm, u : pred x x |- ap R1 R2] =>
  let [g |- S1] = subst [g, x, u |- R1] e in
  let [g |- S2] = subst [g, x, u |- R2] e in
  [g |- ap S1 S2]
| [g, x : tm, u : pred x x |- lm \y.\v. R[.., y, v, x, u]] =>
  let [g |- E] = e in
  let [g, b : block (y : tm, v : pred y y) |- S] =
      subst [g, b : block (y : tm, v : pred y y),
               x : tm, u : pred x x |- R[.., b.1, b.2, x, u]]
            [g, b |- E[..]]
  in [g |- lm \y.\v. S[.., <y ; v>]]
| [g, x : tm, u : pred x x
     |- beta (\y.\v. R[.., y, v, x, u]) R2] =>
  let [g |- S2] = subst [g, x, u |- R2] e in
  let [g |- E] = e in
  let [g, b : block (y : tm, v : pred y y) |- S] =
      subst [g, b : block (y : tm, v : pred y y),
               x : tm, u : pred x x |- R[.., b.1, b.2, x, u]]
            [g, b |- E[..]]
  in [g |- beta (\y.\v. S[.., <y ; v>]) S2]
;

The case for x itself is the assumption u, and its result the given e. Another variable is unchanged, and an application is taken apart componentwise. The cases for lm and beta carry the argument. The body's derivation lives in g, x, u, y, v: the lemma's own variables first, the bound ones after. The recursive call needs a context of schema pctx with the lemma's variables at the end, so the body is moved into g, b, x, u by the renaming [.., b.1, b.2, x, u], the block b standing for y and v. Beluga accepts the measure for that call: the renaming keeps the body's variables in order, the exchange having been done in the pattern, which names R with the bound variables before the lemma's own. §25.2 shows why that matters.

rec subst_same : (g : pctx)
  [g, x : tm, u : pred x x |- pred M[.., x] M'[.., x]]
  -> {N : [g |- tm]} [g |- pred M[.., N] M'[.., N]] =
fn d => mlam N =>
  let [g, x : tm, u : pred x x |- D] = d in
  let [g |- R] = refl [g] [g |- N] in
  [g |- D[.., N, R]]
;

§24.3 · The diamond property

If M ⇛ M₁ and M ⇛ M₂, then M₁ ⇛ N and M₂ ⇛ N for some N. The conclusion is an existential, packaged as an LF family, join, as progress packaged its answer in §22.2. The induction is on the first derivation, and each case inverts the second.

LF join : tm -> tm -> type =
| joins : pred M1 N -> pred M2 N -> join M1 M2
;

rec dia : (g : pctx) [g |- pred M M1] -> [g |- pred M M2]
          -> [g |- join M1 M2] =
/ total d (dia g m m1 m2 d) /
fn d, e => case d of
| [g |- #p.2] => let [g |- #p.2] = e in [g |- joins #p.2 #p.2]
| [g |- lm \y.\v. D] =>
  let [g |- lm \y.\v. E] = e in
  let [g, b : block (y : tm, v : pred y y) |- joins S T] =
      dia [g, b : block (y : tm, v : pred y y) |- D[.., b.1, b.2]]
          [g, b |- E[.., b.1, b.2]] in
  [g |- joins (lm \y.\v. S[.., <y ; v>])
              (lm \y.\v. T[.., <y ; v>])]
| [g |- ap D1 D2] =>
  (case e of
   | [g |- ap E1 E2] =>
     let [g |- joins S1 T1] = dia [g |- D1] [g |- E1] in
     let [g |- joins S2 T2] = dia [g |- D2] [g |- E2] in
     [g |- joins (ap S1 S2) (ap T1 T2)]
   | [g |- beta (\y.\v. E1) E2] =>
     let [g |- lm \y.\v. D1'] = [g |- D1] in
     let [g |- joins S2 T2] = dia [g |- D2] [g |- E2] in
     let [g, b : block (y : tm, v : pred y y) |- joins S1 T1] =
         dia [g, b : block (y : tm, v : pred y y)
                |- D1'[.., b.1, b.2]]
             [g, b |- E1[.., b.1, b.2]] in
     let [g |- T] = subst [g, y, v |- T1[.., <y ; v>]] [g |- T2]
     in [g |- joins (beta (\y.\v. S1[.., <y ; v>]) S2) T])
| [g |- beta (\y.\v. D1) D2] =>
  (case e of
   | [g |- beta (\y.\v. E1) E2] =>
     let [g |- joins S2 T2] = dia [g |- D2] [g |- E2] in
     let [g, b : block (y : tm, v : pred y y) |- joins S1 T1] =
         dia [g, b : block (y : tm, v : pred y y)
                |- D1[.., b.1, b.2]]
             [g, b |- E1[.., b.1, b.2]] in
     let [g |- S] = subst [g, y, v |- S1[.., <y ; v>]] [g |- S2]
     in
     let [g |- T] = subst [g, y, v |- T1[.., <y ; v>]] [g |- T2]
     in [g |- joins S T]
   | [g |- ap (lm \y.\v. E1) E2] =>
     let [g |- joins S2 T2] = dia [g |- D2] [g |- E2] in
     let [g, b : block (y : tm, v : pred y y) |- joins S1 T1] =
         dia [g, b : block (y : tm, v : pred y y)
                |- D1[.., b.1, b.2]]
             [g, b |- E1[.., b.1, b.2]] in
     let [g |- S] = subst [g, y, v |- S1[.., <y ; v>]] [g |- S2]
     in [g |- joins S (beta (\y.\v. T1[.., <y ; v>]) T2)])
;

Six cases. If both derivations are the assumption for one variable, the variable is its own common reduct. If both end in lm, the bodies are joined beneath the binder. If both end in ap, the parts are joined separately. The other three are the overlaps of ap with beta, where one side has contracted the redex and the other has not, or both have, with different reducts. Each joins the parts by the induction hypothesis and then contracts the redex wherever it remains: by beta on a side that still has it, and by the substitution lemma on a side that has already contracted it, whose reduct is a substitution instance.

The development in Beluga's distribution states this lemma on the two derivations packaged as one LF object, so that one pattern can take both apart, and leaves its totality declaration commented out. Packaged that way, every recursive call builds a new package, which is not a subterm of the old one, and Beluga refuses the measure. Taken as two arguments, with the induction on the first, it is checked.

§24.4 · Confluence

From the diamond for one step to confluence for many: if M ⇛* M₁ and M ⇛* M₂, then both reduce to a common N in some number of parallel steps. The proof tiles diamonds. The strip lemma lays one row, a single step against a whole sequence, and confluence stacks the rows.

LF preds : tm -> tm -> type =
| done : preds M M
| more : pred M M1 -> preds M1 M2 -> preds M M2
;

LF strip : tm -> tm -> type =
| strips : preds M1 N -> pred M2 N -> strip M1 M2
;

rec strip_lemma : (g : pctx) [g |- pred M M1] -> [g |- preds M M2]
                  -> [g |- strip M1 M2] =
/ total s (strip_lemma g m m1 m2 d s) /
fn d, s => case s of
| [g |- done] => let [g |- D] = d in [g |- strips done D]
| [g |- more S1 S2] =>
  let [g |- joins T1 T2] = dia d [g |- S1] in
  let [g |- strips U V] = strip_lemma [g |- T2] [g |- S2] in
  [g |- strips (more T1 U) V]
;

LF confl : tm -> tm -> type =
| confls : preds M1 N -> preds M2 N -> confl M1 M2
;

rec conf : (g : pctx) [g |- preds M M1] -> [g |- preds M M2]
           -> [g |- confl M1 M2] =
/ total r (conf g m m1 m2 r) /
fn r, s => case r of
| [g |- done] => let [g |- S] = s in [g |- confls S done]
| [g |- more R1 R2] =>
  let [g |- strips S1 S2] = strip_lemma [g |- R1] s in
  let [g |- confls T U] = conf [g |- R2] [g |- S1] in
  [g |- confls T (more S2 U)]
;

§24.5 · Ordinary reduction

β-reduction contracts one redex, anywhere in a term, and its sequences are reduction in many steps.

LF step : tm -> tm -> type =
| beta1 : step (app (lam M) N) (M N)
| lm1   : ({x : tm} step (M x) (M' x)) -> step (lam M) (lam M')
| apl1  : step M1 M1' -> step (app M1 N) (app M1' N)
| apr1  : step N N' -> step (app M N) (app M N')
;

LF steps : tm -> tm -> type =
| stop : steps M M
| next : step M M1 -> steps M1 M2 -> steps M M2
;

Two facts connect it with parallel reduction. A step is a parallel step, leaving every part but one unreduced, which refl supplies. A parallel step is a sequence of steps: contract the parts, then the redex. The second needs sequences to be closed under the term constructors, under an abstraction and on either side of an application, and closed under concatenation.

rec sappend : (g : pctx) [g |- steps M M1] -> [g |- steps M1 M2]
              -> [g |- steps M M2] =
/ total d (sappend g m m1 m2 d) /
fn d, e => case d of
| [g |- stop] => e
| [g |- next D1 D2] =>
  let [g |- R] = sappend [g |- D2] e in [g |- next D1 R]
;

rec steps_lm : (g : pctx)
  [g, b : block (x : tm, u : pred x x)
     |- steps M[.., b.1] M'[.., b.1]]
  -> [g |- steps (lam \x. M) (lam \x. M')] =
/ total d (steps_lm g m m' d) /
fn d => case d of
| [g, b : block (x : tm, u : pred x x) |- stop] => [g |- stop]
| [g, b : block (x : tm, u : pred x x) |- next S1 S2] =>
  let [g, b : block (x : tm, u : pred x x) |- S1'[.., b.1]] =
      [g, b : block (x : tm, u : pred x x) |- S1] in
  let [g |- R] = steps_lm [g, b |- S2] in
  [g |- next (lm1 \x. S1') R]
;

rec steps_apl : (g : pctx) {N : [g |- tm]} [g |- steps M1 M1']
                -> [g |- steps (app M1 N) (app M1' N)] =
/ total 2 /
mlam N => fn d => case d of
| [g |- stop] => [g |- stop]
| [g |- next S1 S2] =>
  let [g |- R] = steps_apl [g |- N] [g |- S2] in
  [g |- next (apl1 S1) R]
;

rec steps_apr : (g : pctx) {M : [g |- tm]} [g |- steps N N']
                -> [g |- steps (app M N) (app M N')] =
/ total 2 /
mlam M => fn d => case d of
| [g |- stop] => [g |- stop]
| [g |- next S1 S2] =>
  let [g |- R] = steps_apr [g |- M] [g |- S2] in
  [g |- next (apr1 S1) R]
;

Two details. In steps_lm a step beneath the block b can mention only the block's variable, a step being unable to depend on a parallel-reduction assumption, and the let with the pattern S1'[.., b.1] performs that strengthening (§13.3), so that lm1 receives a function of a plain variable. And steps_apl takes the argument N explicitly. It occurs only in the result type, and with N implicit, reconstruction cannot recover it at the recursive call.

rec step_pred : (g : pctx) [g |- step M N] -> [g |- pred M N] =
/ total d (step_pred g m n d) /
fn d => case d of
| [g |- beta1] : [g |- step (app (lam \x. M) N) M[.., N]] =>
  let [g, b : block (x : tm, u : pred x x) |- R] =
      refl [g, b : block (x : tm, u : pred x x)]
           [g, b |- M[.., b.1]] in
  let [g |- R2] = refl [g] [g |- N] in
  [g |- beta (\x.\u. R[.., <x ; u>]) R2]
| [g |- lm1 \x. S] =>
  let [g, b : block (x : tm, u : pred x x) |- R] =
      step_pred [g, b : block (x : tm, u : pred x x)
                   |- S[.., b.1]] in
  [g |- lm \x.\u. R[.., <x ; u>]]
| [g |- apl1 S] : [g |- step (app M1 N) (app M1' N)] =>
  let [g |- R] = step_pred [g |- S] in
  let [g |- R2] = refl [g] [g |- N] in
  [g |- ap R R2]
| [g |- apr1 S] : [g |- step (app M N) (app M N')] =>
  let [g |- R] = step_pred [g |- S] in
  let [g |- R1] = refl [g] [g |- M] in
  [g |- ap R1 R]
;

rec pred_steps : (g : pctx) [g |- pred M N] -> [g |- steps M N] =
/ total d (pred_steps g m n d) /
fn d => case d of
| [g |- #p.2] => [g |- stop]
| [g |- ap D1 D2] : [g |- pred (app M1 N1) (app M1' N1')] =>
  sappend (steps_apl [g |- N1] (pred_steps [g |- D1]))
          (steps_apr [g |- M1'] (pred_steps [g |- D2]))
| [g |- lm \x.\u. D] =>
  steps_lm (pred_steps [g, b : block (x : tm, u : pred x x)
                          |- D[.., b.1, b.2]])
| [g |- beta (\x.\u. D1) D2] =>
  let [g |- S1] : [g |- steps (lam \x. M) (lam \x. M')] =
      steps_lm (pred_steps [g, b : block (x : tm, u : pred x x)
                              |- D1[.., b.1, b.2]]) in
  let [g |- S2] : [g |- steps N N'] = pred_steps [g |- D2] in
  let [g |- S] =
      sappend (steps_apl [g |- N] [g |- S1])
              (steps_apr [g |- lam \x. M'] [g |- S2]) in
  sappend [g |- S] [g |- next beta1 stop]
;

rec steps_preds : (g : pctx) [g |- steps M N]
                  -> [g |- preds M N] =
/ total d (steps_preds g m n d) /
fn d => case d of
| [g |- stop] => [g |- done]
| [g |- next S1 S2] =>
  let [g |- R] = step_pred [g |- S1] in
  let [g |- Rs] = steps_preds [g |- S2] in
  [g |- more R Rs]
;

rec preds_steps : (g : pctx) [g |- preds M N]
                  -> [g |- steps M N] =
/ total d (preds_steps g m n d) /
fn d => case d of
| [g |- done] => [g |- stop]
| [g |- more R1 R2] =>
  sappend (pred_steps [g |- R1]) (preds_steps [g |- R2])
;

§24.6 · The theorem

LF common : tm -> tm -> type =
| commons : steps M1 N -> steps M2 N -> common M1 M2
;

rec church_rosser : (g : pctx) [g |- steps M M1]
                    -> [g |- steps M M2] -> [g |- common M1 M2] =
/ total /
fn s1, s2 =>
  let [g |- confls T U] =
      conf (steps_preds s1) (steps_preds s2) in
  let [g |- S1] = preds_steps [g |- T] in
  let [g |- S2] = preds_steps [g |- U] in
  [g |- commons S1 S2]
;

The theorem is a composition with no induction of its own. Counting what was written: four LF families beyond the syntax, parallel and ordinary reduction and their sequences, and four that package an answer; one schema; and fourteen functions, every one with a measure that Beluga checks. As in §22 and §23, variables, substitution and the laws of substitution went unwritten. The single lemma about substitution the proof needs, that of §24.2, is a fact about parallel reduction rather than about substitution.

LF conv : tm -> tm -> type =
| cstep  : step M N -> conv M N
| crefl  : conv M M
| csym   : conv M N -> conv N M
| ctrans : conv M N -> conv N P -> conv M P
;

rec conv_common : (g : pctx) [g |- conv M N]
                  -> [g |- common M N] =
/ total c (conv_common g m n c) /
fn c => case c of
| [g |- cstep S] => [g |- commons (next S stop) stop]
| [g |- crefl] => [g |- commons stop stop]
| [g |- csym C] =>
  let [g |- commons A B] = conv_common [g |- C] in
  [g |- commons B A]
| [g |- ctrans C1 C2] =>
  let [g |- commons A1 B1] = conv_common [g |- C1] in
  let [g |- commons A2 B2] = conv_common [g |- C2] in
  let [g |- commons U V] = church_rosser [g |- B1] [g |- A2] in
  let [g |- L] = sappend [g |- A1] [g |- U] in
  let [g |- R] = sappend [g |- B2] [g |- V] in
  [g |- commons L R]
;

§25Cut elimination#

The developments so far reason about programming languages. The object of study can as well be a logic, and the theorem one first proves about a sequent calculus is cut elimination: the rule of cut, which lets a proof use a lemma proved separately, adds nothing that cannot be proved without it. Its proof is a nested induction, on the formula cut and then on the two derivations, which Beluga checks as a lexicographic order. This section follows Pfenning's structural proof, in the form the distribution's examples take, for the conjunction and implication of intuitionistic logic. Quantifiers are left out: an instance A[t/x] of a quantified formula ∀x. A is not one of its subformulas, so the cut formula would no longer shrink by structure alone, and the induction here would not apply as it stands.

§25.1 · The sequent calculus

Formulas are built from atoms p and q by conjunction and implication. A sequent Γ ⊢ C says that C follows from the hypotheses Γ. Its rules introduce a connective either in the conclusion, a right rule, or in a hypothesis, a left rule, and the rule init closes a branch with a hypothesis that is the conclusion. In LF the hypotheses are assumptions in the context, of type hyp A, and hyp has no constructors: its only inhabitants are the assumptions themselves, and its contexts are those of the schema hctx. A left rule names the hypothesis it decomposes, and adds the hypotheses it produces to the context of its premise.

LF form : type =
| p    : form
| q    : form
| conj : form -> form -> form
| imp  : form -> form -> form
;

LF hyp : form -> type = ;

LF conc : form -> type =
| init  : hyp A -> conc A
| conjr : conc A -> conc B -> conc (conj A B)
| conjl : (hyp A -> hyp B -> conc C) -> hyp (conj A B) -> conc C
| impr  : (hyp A -> conc B) -> conc (imp A B)
| impl  : conc A -> (hyp B -> conc C) -> hyp (imp A B) -> conc C
;

schema hctx = some [a : form] hyp a;

let swap : [ |- conc (imp (conj p q) (conj q p))] =
  [ |- impr \h. conjl (\x.\y. conjr (init y) (init x)) h];

§25.2 · Cut is admissible

The rule of cut reads: from Γ ⊢ A and Γ, A ⊢ C, conclude Γ ⊢ C. It is admissible in the calculus above, and the function ca proves it, turning the two derivations into a derivation of Γ ⊢ C that uses no cut. The formula A is closed, given explicitly, and the right-hand derivation is open in the hypothesis h : hyp A, which it may use any number of times.

rec ca : (g : hctx) {A : [ |- form]} [g |- conc A[]]
         -> [g, h : hyp A[] |- conc C[]] -> [g |- conc C[]] =
/ total {a d e} (ca g c a d e) /
mlam A => fn d, e => case e of
| [g, h : hyp _ |- init h] => d
| [g, h : hyp _ |- init #x[..]] => [g |- init #x]
| [g, h : hyp _ |- conjr E1 E2] =>
  let [g |- F1] = ca [ |- A] d [g, h |- E1] in
  let [g |- F2] = ca [ |- A] d [g, h |- E2] in
  [g |- conjr F1 F2]
| [g, h : hyp _ |- impr \x. E[.., x, h]] =>
  let [g |- D] = d in
  let [g, x : hyp _ |- F] =
      ca [ |- A] [g, x : hyp _ |- D[..]] [g, x, h |- E] in
  [g |- impr \x. F]
| [g, h : hyp _ |- conjl (\x.\y. E[.., x, y, h]) #z[..]] =>
  let [g |- D] = d in
  let [g, x : hyp _, y : hyp _ |- F] =
      ca [ |- A] [g, x : hyp _, y : hyp _ |- D[..]]
         [g, x, y, h |- E] in
  [g |- conjl (\x.\y. F) #z]
| [g, h : hyp _ |- impl E1 (\y. E2[.., y, h]) #z[..]] =>
  let [g |- D] = d in
  let [g |- F1] = ca [ |- A] d [g, h |- E1] in
  let [g, y : hyp _ |- F2] =
      ca [ |- A] [g, y : hyp _ |- D[..]] [g, y, h |- E2] in
  [g |- impl F1 (\y. F2) #z]
| [g, h : hyp (conj A1[] A2[])
     |- conjl (\x.\y. E[.., x, y, h]) h] =>
  (case d of
   | [g |- conjr D1 D2] =>
     let [g, x : hyp A1[], y : hyp A2[] |- F] =
         ca [ |- conj A1 A2]
            [g, x : hyp A1[], y : hyp A2[] |- conjr D1[..] D2[..]]
            [g, x, y, h |- E] in
     let [g, y : hyp A2[] |- F1] =
         ca [ |- A1] [g, y : hyp A2[] |- D1[..]]
            [g, y, x |- F[.., x, y]] in
     ca [ |- A2] [g |- D2] [g, y |- F1]
   | [g |- init #w] =>
     let [g, h : hyp _ |- E0] = e in [g |- E0[.., #w]]
   | [g |- conjl (\x.\y. D1) #w] =>
     let [g, h : hyp _ |- E0] = e in
     let [g, x : hyp _, y : hyp _ |- F] =
         ca [ |- conj A1 A2] [g, x : hyp _, y : hyp _ |- D1]
            [g, x, y, h |- E0[.., h]] in
     [g |- conjl (\x.\y. F) #w]
   | [g |- impl D1 (\y. D2) #w] =>
     let [g, h : hyp _ |- E0] = e in
     let [g, y : hyp _ |- F] =
         ca [ |- conj A1 A2] [g, y : hyp _ |- D2]
            [g, y, h |- E0[.., h]] in
     [g |- impl D1 (\y. F) #w])
| [g, h : hyp (imp A1[] A2[]) |- impl E1 (\y. E2[.., y, h]) h] =>
  (case d of
   | [g |- impr \x. D2] =>
     let [g |- F1] = ca [ |- imp A1 A2] d [g, h |- E1] in
     let [g, y : hyp A2[] |- F2] =
         ca [ |- imp A1 A2]
            [g, y : hyp A2[] |- impr \x. D2[.., x]]
            [g, y, h |- E2] in
     let [g |- G] = ca [ |- A1] [g |- F1] [g, x |- D2] in
     ca [ |- A2] [g |- G] [g, y |- F2]
   | [g |- init #w] =>
     let [g, h : hyp _ |- E0] = e in [g |- E0[.., #w]]
   | [g |- conjl (\x.\y. D1) #w] =>
     let [g, h : hyp _ |- E0] = e in
     let [g, x : hyp _, y : hyp _ |- F] =
         ca [ |- imp A1 A2] [g, x : hyp _, y : hyp _ |- D1]
            [g, x, y, h |- E0[.., h]] in
     [g |- conjl (\x.\y. F) #w]
   | [g |- impl D1 (\y. D2) #w] =>
     let [g, h : hyp _ |- E0] = e in
     let [g, y : hyp _ |- F] =
         ca [ |- imp A1 A2] [g, y : hyp _ |- D2]
            [g, y, h |- E0[.., h]] in
     [g |- impl D1 (\y. F) #w])
;

The measure / total {a d e} (ca g c a d e) / is lexicographic (§20.2). Every recursive call either cuts a smaller formula, whatever its derivations; or cuts the same formula and has a smaller left derivation, the right one being anything; or keeps both and has a smaller right derivation. The cases follow the last rule of the right derivation e. If it is init on h, the result is d itself; init on another hypothesis survives unchanged. A right rule, or a left rule on another hypothesis, does not touch h, so the cut is pushed into its premises, which are smaller right derivations. What remains is a left rule on h itself, and there the left derivation d decides. If d ends in the matching right rule, the cut is principal: it is replaced by cuts on the immediate subformulas, after one more cut of the same formula removes the uses of h that the premises of e still contain. If d is a hypothesis, that hypothesis replaces h in e. If d ends in a left rule, the cut is pushed into the premise of d, a smaller left derivation.

One detail decides whether Beluga accepts the measure. In each case that goes beneath a binder, the pattern names the premise with the cut hypothesis last: impr \x. E[.., x, h] names E in the context g, x, h, so the recursive call passes E itself. Written the other way, with E named in g, h, x and the call passing E[.., h, x], the argument is a subderivation with two of its hypotheses exchanged, and Beluga refuses the measure. An exchange, like any reordering, belongs in the pattern.

§25.3 · Cut elimination

With cut admissible, eliminating cuts is a plain induction. The calculus with cut has the same rules and one more; a derivation in it is translated rule by rule into the cut-free calculus, and at each cut both premises are translated first and ca then combines them.

LF concx : form -> type =
| initx  : hyp A -> concx A
| conjrx : concx A -> concx B -> concx (conj A B)
| conjlx : (hyp A -> hyp B -> concx C) -> hyp (conj A B)
           -> concx C
| imprx  : (hyp A -> concx B) -> concx (imp A B)
| implx  : concx A -> (hyp B -> concx C) -> hyp (imp A B)
           -> concx C
| cut    : concx A -> (hyp A -> concx C) -> concx C
;

rec elim : (g : hctx) [g |- concx C[]] -> [g |- conc C[]] =
/ total d (elim g c d) /
fn d => case d of
| [g |- initx #x] => [g |- init #x]
| [g |- conjrx D1 D2] =>
  let [g |- F1] = elim [g |- D1] in
  let [g |- F2] = elim [g |- D2] in
  [g |- conjr F1 F2]
| [g |- conjlx (\x.\y. D) #z] =>
  let [g, x : hyp _, y : hyp _ |- F] =
      elim [g, x : hyp _, y : hyp _ |- D] in
  [g |- conjl (\x.\y. F) #z]
| [g |- imprx \x. D] =>
  let [g, x : hyp _ |- F] = elim [g, x : hyp _ |- D] in
  [g |- impr \x. F]
| [g |- implx D1 (\y. D2) #z] =>
  let [g |- F1] = elim [g |- D1] in
  let [g, y : hyp _ |- F2] = elim [g, y : hyp _ |- D2] in
  [g |- impl F1 (\y. F2) #z]
| [g |- cut D1 (\x. D2)] : [g |- concx C[]] =>
  let [g |- F1] : [g |- conc A[]] = elim [g |- D1] in
  let [g, x : hyp A[] |- F2] = elim [g, x : hyp A[] |- D2] in
  ca [ |- A] [g |- F1] [g, x |- F2]
;

The cut case names the formula cut with an annotated let, since the rule leaves it implicit, and passes it to ca explicitly.

rec embed : (g : hctx) [g |- conc C[]] -> [g |- concx C[]] =
/ total d (embed g c d) /
fn d => case d of
| [g |- init #x] => [g |- initx #x]
| [g |- conjr D1 D2] =>
  let [g |- F1] = embed [g |- D1] in
  let [g |- F2] = embed [g |- D2] in
  [g |- conjrx F1 F2]
| [g |- conjl (\x.\y. D) #z] =>
  let [g, x : hyp _, y : hyp _ |- F] =
      embed [g, x : hyp _, y : hyp _ |- D] in
  [g |- conjlx (\x.\y. F) #z]
| [g |- impr \x. D] =>
  let [g, x : hyp _ |- F] = embed [g, x : hyp _ |- D] in
  [g |- imprx \x. F]
| [g |- impl D1 (\y. D2) #z] =>
  let [g |- F1] = embed [g |- D1] in
  let [g, y : hyp _ |- F2] = embed [g, y : hyp _ |- D2] in
  [g |- implx F1 (\y. F2) #z]
;

§25.4 · Consistency

Cut elimination yields consistency. A cut-free derivation has the subformula property: every formula in it occurs in its final sequent. In the empty context nothing then concludes an atom: init needs a hypothesis, each left rule a hypothesis to decompose, and no right rule concludes an atom. So ⊢ p has no cut-free derivation, and by elimination none with cut either.

LF void : type = ;

rec consistent : [ |- concx p] -> [ |- void] =
/ total /
fn d => case elim d of
| [ |- init H]             => impossible [ |- H]
| [ |- conjl (\x.\y. D) H] => impossible [ |- H]
| [ |- impl D1 (\y. D2) H] => impossible [ |- H]
;

The case analysis is written out. impossible d alone is refused for a cut-free derivation of conc p: the rule init concludes it, and impossible accepts only a type no rule concludes (§15.4). Each case is closed instead by the hypothesis it needs, of which the empty context has none. Counted: four LF families, one schema, and three functions, each with a measure that Beluga checks.

§26Translations#

A compiler is a series of translations, each from one language into another. One property asked of each is that it preserves types, and it is the one that can be stated before either language has a semantics. When both languages are encoded intrinsically, in the sense of §23.1, the type of a translation states that property: a function from source terms of type A to target terms of type A cannot produce an ill-typed term, since the target has none, and typechecking the function proves the theorem. This section gives two translations of one source language. The first, into continuation-passing style, has a typed target whose variables correspond one to one with those of the source, and a block schema keeps each pair together. The second, into de Bruijn form, has a target without variable names, and the source context serves as the environment in which each variable's position is found. Both are adapted from the distribution's examples.

§26.1 · Two languages

The source is a call-by-value λ-calculus over one base type o, intrinsically typed, with values and expressions in separate families. A value is an abstraction or a variable, and an expression is an application or a value returned by ret. Variables range over values, as call by value requires: a function receives its argument only once the argument has been evaluated. Each family mentions the other, so the two are declared together.

The target is the language of continuation-passing style, in three families. A contra is a computation that does not return: capp applies a function to an argument and a continuation, and cthrow passes a value to a continuation. A cvalue of type A ⇒ B is a function that takes an argument of type A and a continuation for B. A ccont of type A, a continuation, is a computation waiting for a value of type A. contra has no type index, since a computation that never returns has no result whose type could be recorded. Read as propositions, contra is falsehood and a continuation for A is a refutation of A, and under that reading the translation below is a double-negation translation.

LF tp : type =
| o   : tp
| arr : tp -> tp -> tp
;

LF exp : tp -> type =
| app : exp (arr A B) -> exp A -> exp B
| ret : value A -> exp A

and value : tp -> type =
| lam : (value A -> exp B) -> value (arr A B)
;

LF contra : type =
| capp   : cvalue (arr A B) -> cvalue A -> ccont B -> contra
| cthrow : ccont A -> cvalue A -> contra

and cvalue : tp -> type =
| clam : (cvalue A -> ccont B -> contra) -> cvalue (arr A B)

and ccont : tp -> type =
| cconti : (cvalue A -> contra) -> ccont A
;

§26.2 · Continuation-passing style

The translation sends a value of type A to a target value of type A, and an expression of type A to a computation that passes the expression's value to a continuation k : ccont A. That continuation is a variable of the result's context, [g, k : ccont A[] |- contra]. The two types are the theorem that the translation preserves types, and nothing beyond them remains to be proved.

A source variable must become a target variable, and the image of a term open in source variables is open in the corresponding target variables. §16.5 related two contexts of different schemas by an inductive type. A simpler arrangement is available here, the correspondence being one to one: the two variables are declared together. Each element of a context of the schema cctx is a block (§11.2) holding a source variable x : value a and its counterpart y : cvalue a in the target.

schema cctx = some [a : tp] block (x : value a, y : cvalue a);

rec cpsv : (g : cctx) [g |- value A[]] -> [g |- cvalue A[]] =
/ total v (cpsv g a v) /
fn v => case v of
| [g |- #p.1] => [g |- #p.2]
| [g |- lam \x. E] : [g |- value (arr A[] B[])] =>
  let [g, b : block (x : value A[], y : cvalue A[]), k : ccont B[]
         |- F[.., b.2, k]] =
      cpse [g, b : block (x : value A[], y : cvalue A[])
              |- E[.., b.1]]
  in [g |- clam \y.\k. F]

and rec cpse : (g : cctx) [g |- exp A[]]
               -> [g, k : ccont A[] |- contra] =
/ total e (cpse g a e) /
fn e => case e of
| [g |- ret V] =>
  let [g |- W] = cpsv [g |- V] in [g, k |- cthrow k W[..]]
| [g |- app E1 E2] =>
  let [g, k : ccont _ |- F1] = cpse [g |- E1] in
  let [g, k : ccont _ |- F2] = cpse [g |- E2] in
  [g, k |- F1[.., cconti \f. F2[.., cconti \x. capp f x k]]]
;

The variable case is a projection: the source variable #p.1 becomes its counterpart #p.2. For an abstraction lam \x. E, the body is translated in the context extended by one block, whose source half stands for x. The result is a computation open in the block and in the continuation, and the pattern F[.., b.2, k] says that it uses only the target half of the block. That pattern is a strengthening, accepted because no target term can mention a source value, which is the subordination of §13.3: with a target constructor that took a source value, the same let is refused as not covering. clam then binds the target variable and the continuation. The annotation on the pattern names the types A and B, and the let uses them; with the block's types left as _, Beluga refuses the call, reporting that the type of its result is not closed.

A returned value ret V becomes cthrow k W, with W the image of V: the value is passed straight to the continuation. An application is the substantive case. Both subexpressions are translated, each against a continuation of its own, giving F1 and F2, both open in k. The result replaces the k of F1 by a continuation that receives the function's value f and continues as F2, and the k of F2 by a continuation that receives the argument's value x and makes the call capp f x k, with the continuation of the whole application. Read from the outside in, the function is evaluated, then the argument, then the call. The order of evaluation, which in the source is a matter of its evaluation rules, is now in the structure of the term. Each measure is on the source term, and every recursive call receives a subterm.

This is Plotkin's call-by-value translation. It is direct, and it is not economical: its image contains administrative redexes, continuations applied directly to values, which the translation introduced and the source did not contain. Danvy and Filinski's one-pass translation does not create them, at the cost of a less direct definition. Exercise 26.1 computes an image and finds them.

let image : [k : ccont (arr o o) |- contra] =
  [k : ccont (arr o o) |-
     cthrow (cconti \f. cthrow (cconti \x. capp f x k)
                                (clam \y.\c. cthrow c y))
            (clam \y.\c. cthrow c y)];

LF uterm : type =
| uapp : uterm -> uterm -> uterm
| ulam : (uterm -> uterm) -> uterm
;

schema ectx = some [a : tp] block (x : value a, u : uterm);

rec erv : (g : ectx) [g |- value A[]] -> [g |- uterm] =
/ total v (erv g a v) /
fn v => case v of
| [g |- #p.1] => [g |- #p.2]
| [g |- lam \x. E] : [g |- value (arr A[] B[])] =>
  let [g, b : block (x : value A[], u : uterm) |- F[.., b.2]] =
      ere [g, b : block (x : value A[], u : uterm) |- E[.., b.1]]
  in [g |- ulam \u. F]

and rec ere : (g : ectx) [g |- exp A[]] -> [g |- uterm] =
/ total e (ere g a e) /
fn e => case e of
| [g |- ret V] => erv [g |- V]
| [g |- app E1 E2] =>
  let [g |- F1] = ere [g |- E1] in
  let [g |- F2] = ere [g |- E2] in
  [g |- uapp F1 F2]
;

§26.3 · De Bruijn form

In de Bruijn's notation a variable is a number, the count of binders from its occurrence out to the binder it refers to, that binder included: a de Bruijn index. Bound variables have no names, so terms that differ only in the names of their bound variables are identical. In dexp, one is the variable bound by the nearest enclosing dlam, and shift moves a variable one binder further out, so that shift one is the variable bound by the second nearest. A dexp is a closed LF term. Its variables are numerals, not LF variables, and its type index records the type of the term.

The translation turns a term open in g into a closed dexp, so the source context must supply what the image cannot contain, the position of each variable. The context is the environment. Its schema, vctx, holds source variables alone: the target has no variables for them to be paired with.

LF dexp : tp -> type =
| one   : dexp A
| shift : dexp A -> dexp A
| dlam  : dexp B -> dexp (arr A B)
| dapp  : dexp (arr A B) -> dexp A -> dexp B
;

schema vctx = some [a : tp] value a;

lookup finds a variable's position by recursion on the context, matching on it as in §10.4. The empty context has no variables, so a parameter variable over it has no instances, and impossible closes the case (§15.5); coverage requires the case to be written. In a context h, x : value T[] the parameter is either x, the last variable, at position one, or a variable #q of h, weakened past x, whose position is one more than its position in h.

rec lookup : {g : vctx} {#p : #[g |- value S[]]} [ |- dexp S[]] =
/ total g (lookup g) /
mlam g, #p => case [g] of
| [] => impossible [ |- #p]
| [h, x : value T[]] =>
  (case [h, x : value T[] |- #p[.., x]] of
   | [h, x : value T[] |- x] => [ |- one]
   | [h, x : value T[] |- #q[..]] =>
     let [ |- D] = lookup [h] [h |- #q] in [ |- shift D])
;

The recursion is on the context, and it has to be written that way. The direct formulation, in dbv, would match [h, x : value T[] |- #q[..]] and call dbv [h |- #q]. Beluga refuses that call as not structurally smaller, and by its own standard rightly: [h |- #q] is not a subterm of [h, x : value T[] |- #q[..]] but the same variable in a shorter context. What decreases is the context, and the measure / total g (lookup g) / says so, on a function that takes the context explicitly and matches on it.

rec dbv : (g : vctx) [g |- value S[]] -> [ |- dexp S[]] =
/ total v (dbv g s v) /
fn v => case v of
| [g |- #p] => lookup [g] [g |- #p]
| [g |- lam \x. E] : [g |- value (arr A[] B[])] =>
  let [ |- D] = dbe [g, x : value A[] |- E] in [ |- dlam D]

and rec dbe : (g : vctx) [g |- exp S[]] -> [ |- dexp S[]] =
/ total e (dbe g s e) /
fn e => case e of
| [g |- ret V] => dbv [g |- V]
| [g |- app E1 E2] =>
  let [ |- D1] = dbe [g |- E1] in
  let [ |- D2] = dbe [g |- E2] in
  [ |- dapp D1 D2]
;

dbv and dbe are then a structural recursion of the ordinary kind. A variable is looked up. The body of an abstraction is translated in the context extended by its variable, and dlam wraps the result. An application translates both parts. Applied to lam \x. ret (lam \y. ret x), at type o ⇒ o ⇒ o, dbv gives dlam (dlam (shift one)): the body refers to x across the inner binder.

The type of dbe states less than the type of cpse. It says that the image has the type of the source, and nothing about its variables: dexp has no index for a context, and [ |- one] is a dexp of type o, though as a closed term it names a variable bound by nothing. Exercise 26.5 indexes the target by the types of the variables in scope, and relates the two contexts as §16.5 does. Counted: seven LF families, two schemas, and five functions, each with a measure that Beluga checks.

dlam (dlam (dapp (shift one) one))

LF tps : type =
| nil  : tps
| cons : tp -> tps -> tps
;

LF dvar : tps -> tp -> type =
| top : dvar (cons A G) A
| pop : dvar G A -> dvar (cons B G) A
;

LF wexp : tps -> tp -> type =
| wvar : dvar G A -> wexp G A
| wlam : wexp (cons A G) B -> wexp G (arr A B)
| wapp : wexp G (arr A B) -> wexp G A -> wexp G B
;

inductive Env : {g : vctx} [ |- tps] -> ctype =
| Nil  : Env [] [ |- nil]
| Snoc : Env [g] [ |- G] -> Env [g, x : value A[]] [ |- cons A G]
;

rec wlookup : {g : vctx} Env [g] [ |- G]
              -> {#p : #[g |- value S[]]} [ |- dvar G S[]] =
/ total g (wlookup g _ _ _) /
mlam g => fn r => mlam #p => case [g] of
| [] => impossible [ |- #p]
| [h, x : value T[]] =>
  let Snoc r' = r in
  (case [h, x : value T[] |- #p[.., x]] of
   | [h, x : value T[] |- x] => [ |- top]
   | [h, x : value T[] |- #q[..]] =>
     let [ |- I] = wlookup [h] r' [h |- #q] in [ |- pop I])
;

rec wv : Env [g] [ |- G] -> [g |- value S[]] -> [ |- wexp G S[]] =
/ total v (wv _ _ _ r v) /
fn r, v => case v of
| [g |- #p] =>
  let [ |- I] = wlookup [g] r [g |- #p] in [ |- wvar I]
| [g |- lam \x. E] : [g |- value (arr A[] B[])] =>
  let [ |- D] = we (Snoc r) [g, x : value A[] |- E] in
  [ |- wlam D]

and rec we : Env [g] [ |- G] -> [g |- exp S[]]
             -> [ |- wexp G S[]] =
/ total e (we _ _ _ r e) /
fn r, e => case e of
| [g |- ret V] => wv r [g |- V]
| [g |- app E1 E2] =>
  let [ |- D1] = we r [g |- E1] in
  let [ |- D2] = we r [g |- E2] in
  [ |- wapp D1 D2]
;

§27Bisimulation#

Two processes are equivalent, in the sense that matters for concurrency, when each can match every action of the other and the processes they then become are again equivalent. That relation is bisimilarity, and since processes may run forever it is defined coinductively, as the largest relation with that property rather than the least. §18 introduced coinductive types for infinite data. Here a coinductive type is a relation, its inhabitants are proofs by coinduction, and an inhabitant is built as §18 built streams, by saying what each observation returns. The development follows the distribution's bisimulation for the π-calculus, itself after Abella's, on a smaller calculus. Its last subsection says what Beluga checks of such a proof, which is less than it checks of the proofs before it.

§27.1 · Processes and transitions

A process performs actions, here a, b and c. nil does nothing; pre A P performs A and becomes P; sum P Q behaves as P or as Q, the choice being made by the first action; and fix F is a recursive process, F binding the recursion variable, so that fix \x. pre a x performs a forever. The judgment step P A P' says that P can perform A and become P'. Its rule for recursion unfolds the process once: F (fix F) is the body with fix F substituted for its variable, an LF application being a substitution.

LF act : type =
| a : act
| b : act
| c : act
;

LF proc : type =
| nil : proc
| pre : act -> proc -> proc
| sum : proc -> proc -> proc
| fix : (proc -> proc) -> proc
;

LF step : proc -> act -> proc -> type =
| s_pre  : step (pre A P) A P
| s_suml : step P A P' -> step (sum P Q) A P'
| s_sumr : step Q A Q' -> step (sum P Q) A Q'
| s_fix  : step (F (fix F)) A P' -> step (fix F) A P'
;

§27.2 · Bisimilarity

A relation between processes is a bisimulation when, for every related pair P and Q, each step of P is matched by a step of Q with the same action, the two results being related again, and each step of Q is matched in the same way by P. Two processes are bisimilar when some bisimulation relates them. As a coinductive type, bisimilarity is defined by what can be asked of it: given a bisimilarity of P and Q and a step of P, the observation Fwd answers with a step of Q and a bisimilarity of the two results, and Bwd does the same for a step of Q. The answer is packaged in the inductive type Reply, declared with Bisim since each mentions the other (§18.3).

Rep holds the step of the process that answers and the bisimilarity of the results, with the result of the step asked about first. Fwd and Bwd share Reply, so the backward answer relates Q' to the result of P's step, in that order: the roles of the two processes are exchanged. Exercise 27.1 asks what follows from that arrangement.

coinductive Bisim : [ |- proc] -> [ |- proc] -> ctype =
| Fwd : Bisim [ |- P] [ |- Q] :: [ |- step P A P']
        -> Reply [ |- Q] [ |- A] [ |- P']
| Bwd : Bisim [ |- P] [ |- Q] :: [ |- step Q A Q']
        -> Reply [ |- P] [ |- A] [ |- Q']

and inductive Reply : [ |- proc] -> [ |- act] -> [ |- proc]
                      -> ctype =
| Rep : [ |- step Q A Q'] -> Bisim [ |- P'] [ |- Q']
        -> Reply [ |- Q] [ |- A] [ |- P']
;

Reflexivity, symmetry and transitivity follow, each a definition by copatterns. refl answers a step of P with the same step and continues with the reflexivity of the result. sym answers each observation with the opposite observation of its argument, which the exchanged roles make possible without a recursive call. trans answers a step of P by asking the first bisimilarity for a step of Q, then the second for a step of R, and continues with the transitivity of the two bisimilarities that come back; the backward case asks in the opposite order. None of the three carries a totality declaration, for the reason §27.4 gives.

rec refl : {P : [ |- proc]} Bisim [ |- P] [ |- P] =
fun [ |- P] .Fwd (t : [ |- step P A P']) => Rep t (refl [ |- P'])
  | [ |- P] .Bwd (t : [ |- step P A P']) => Rep t (refl [ |- P'])
;

rec sym : Bisim [ |- P] [ |- Q] -> Bisim [ |- Q] [ |- P] =
fun s .Fwd t => s .Bwd t
  | s .Bwd t => s .Fwd t
;

rec trans : Bisim [ |- P] [ |- Q] -> Bisim [ |- Q] [ |- R]
            -> Bisim [ |- P] [ |- R] =
fun s1 s2 .Fwd t =>
    let Rep t1 s3 = s1 .Fwd t in
    let Rep t2 s4 = s2 .Fwd t1 in
    Rep t2 (trans s3 s4)
  | s1 s2 .Bwd t =>
    let Rep t1 s3 = s2 .Bwd t in
    let Rep t2 s4 = s1 .Bwd t1 in
    Rep t2 (trans s3 s4)
;

§27.3 · A proof by coinduction

To prove two processes bisimilar is to exhibit a bisimulation containing them, and in Beluga it is to define a bisimilarity of the two by saying how each observation is answered. Take fix \x. pre a x, which performs a forever, and fix \x. pre a (pre a x), which performs a twice and repeats. Each step of either is matched by a step of the other, the second passing through pre a (fix \x. pre a (pre a x)) on the way. The relation containing the pair of the two processes and the pair of the first with that intermediate process, together with the two pairs reversed, is a bisimulation. The definitions w1 and w2 are its first two pairs, each answering with the other, and sym supplies the reversed pairs that the backward answers require.

rec sp : [ |- step (fix \x. pre a x) a (fix \x. pre a x)] =
  [ |- s_fix s_pre]
;

rec sq : [ |- step (fix \x. pre a (pre a x)) a
                   (pre a (fix \x. pre a (pre a x)))] =
  [ |- s_fix s_pre]
;

rec w1 : Bisim [ |- fix \x. pre a x]
               [ |- fix \x. pre a (pre a x)] =
fun .Fwd t =>
    (case t of
     | [ |- s_fix S] =>
       (case [ |- S] of
        | [ |- s_pre] => Rep sq w2))
  | .Bwd t =>
    (case t of
     | [ |- s_fix S] =>
       (case [ |- S] of
        | [ |- s_pre] => Rep sp (sym w2)))

and rec w2 : Bisim [ |- fix \x. pre a x]
                   [ |- pre a (fix \x. pre a (pre a x))] =
fun .Fwd t =>
    (case t of
     | [ |- s_fix S] =>
       (case [ |- S] of
        | [ |- s_pre] => Rep [ |- s_pre] w1))
  | .Bwd t =>
    (case t of
     | [ |- s_pre] => Rep sp (sym w1))
;

Two details concern the rule s_fix. Its premise is a step of F (fix F), which is a pattern only once F is known. Matched in one pattern, [ |- s_fix s_pre], it is refused as falling outside the decidable pattern fragment; matched in two stages, first s_fix S and then S, it is accepted, the first match having fixed F. For the same reason a step through s_fix is built where its full type is known. Written inline as the argument of Rep, where the target of the step is still to be inferred, it is refused in the same terms; named at its type, as sp and sq are, it is accepted.

rec comm : {P : [ |- proc]} {Q : [ |- proc]}
           Bisim [ |- sum P Q] [ |- sum Q P] =
fun [ |- P] [ |- Q] .Fwd (t : [ |- step (sum P Q) A R]) =>
    (case t of
     | [ |- s_suml T] => Rep [ |- s_sumr T] (refl [ |- R])
     | [ |- s_sumr T] => Rep [ |- s_suml T] (refl [ |- R]))
  | [ |- P] [ |- Q] .Bwd (t : [ |- step (sum Q P) A R]) =>
    (case t of
     | [ |- s_suml T] => Rep [ |- s_sumr T] (refl [ |- R])
     | [ |- s_sumr T] => Rep [ |- s_suml T] (refl [ |- R]))
;

rec sfix : {F : [x : proc |- proc]} [ |- step F[fix \x. F] A Q']
           -> [ |- step (fix \x. F) A Q'] =
mlam F => fn t => let [ |- T] = t in [ |- s_fix T]
;

rec unfold : {F : [x : proc |- proc]}
             Bisim [ |- fix \x. F] [ |- F[fix \x. F]] =
fun [x : proc |- F] .Fwd (t : [ |- step (fix \x. F) A P']) =>
    let [ |- s_fix T] = t in Rep [ |- T] (refl [ |- P'])
  | [x : proc |- F] .Bwd (t : [ |- step F[fix \x. F] A Q']) =>
    Rep (sfix [x : proc |- F] t) (refl [ |- Q'])
;

§27.4 · What is checked

The definitions of §27.2 and §27.3 typecheck, and they cover: every step an observation can be asked about is answered. That is all Beluga checks of them. A corecursive definition describes an infinite object only when it is productive, every observation returning after finitely many steps of computation, and Beluga does not check productivity. The following definition claims that pre a nil and pre b nil are bisimilar, which is false, since the first performs a and the second b. It typechecks and covers, and it is accepted.

rec fake : Bisim [ |- pre a nil] [ |- pre b nil] =
fun .Fwd t => fake .Fwd t
  | .Bwd t => fake .Bwd t
;

Its observations answer by asking themselves the same question, and they never return. A totality declaration does not help. A bare / total / declares a function that does not call itself, and it refuses fake for doing so; it refuses refl, trans, w1 and w2 for the same reason, while sym, which makes no recursive call, accepts it. A measure is refused as well: refl measured on its process is refused, the process after a step being no smaller than the process before it. The distribution's own total development of Howe's method declares its corecursive definitions / trust /. A proof by coinduction in Beluga therefore stands at the second row of §20.3's table. It typechecks and covers, and its productivity, on which its meaning rests, is checked by hand. Here every answer is returned at once: each corecursive call stands beneath Rep, as an argument of the answer, and sym, through which two of them pass, answers an observation with one observation of its argument.

Non-bisimilarity, by contrast, is inductive. To show that two processes are not bisimilar is to refute a bisimilarity of them, by a finite sequence of observations ending at a step that has no answer. pre a (sum (pre b nil) (pre c nil)) and sum (pre a (pre b nil)) (pre a (pre c nil)) perform the same sequences of actions, a then b or a then c, and they are not bisimilar: after a the first can still do either, while the second has committed to one. distinct asks a bisimilarity of the two for the answer to the first process's a. That answer may come from either side of the choice, so impossible cannot close it at once, and the two cases are taken in turn. In each, the bisimilarity that comes back is asked for the step the committed process cannot match, and the answer contains a step that does not exist. The function makes no recursive call, is declared / total /, and under --coverage is a proof in the strongest sense of §20.3.

LF void : type = ;

rec distinct :
    Bisim [ |- pre a (sum (pre b nil) (pre c nil))]
          [ |- sum (pre a (pre b nil)) (pre a (pre c nil))]
    -> [ |- void] =
/ total /
fn s =>
  let Rep t s1 = s .Fwd [ |- s_pre] in
  (case t of
   | [ |- s_suml s_pre] =>
     let Rep u s2 = s1 .Fwd [ |- s_sumr s_pre] in impossible u
   | [ |- s_sumr s_pre] =>
     let Rep u s2 = s1 .Fwd [ |- s_suml s_pre] in impossible u)
;

Counted: four LF families, a coinductive type and an inductive one declared together, and eight definitions. distinct carries a totality declaration that Beluga checks. The four that call themselves, refl, trans, w1 and w2, are refused a bare / total /, and refl is refused a measure too.

rec once : Bisim [ |- fix \x. pre a x] [ |- pre a nil]
           -> [ |- void] =
/ total /
fn s =>
  let Rep t s1 = s .Fwd sp in
  let [ |- s_pre] = t in
  let Rep u s2 = s1 .Fwd sp in
  impossible u
;

§28Big-step evaluation#

§24 studied β-reduction, which may contract any redex anywhere and in any order. A programming language fixes an order, and its semantics is often given in big-step form: one judgment relates a term to its value directly, with one rule for each construct and no intermediate terms. This section gives call-by-value evaluation for the untyped calculus of §6 in that form, proves it deterministic, relates it to the reduction of §24, and shows what it cannot do: a term may reduce to a value without having one. It resumes the development of §24, whose lemmas about reduction it uses.

§28.1 · Evaluation

A value is an abstraction. Evaluating an abstraction gives the abstraction itself. Evaluating an application evaluates the function to an abstraction lam M, then the argument to a value V, then the body with V substituted for its variable, M V; the result of the last is the result of the whole. The argument is evaluated before it is substituted, which is what call by value means. Evaluation concerns closed terms, and every derivation in this section is in the empty context.

LF value : tm -> type =
| v_lam : value (lam M)
;

LF eval : tm -> tm -> type =
| ev_lam : eval (lam M) (lam M)
| ev_app : eval M1 (lam M) -> eval N V -> eval (M V) W
           -> eval (app M1 N) W
;

By induction on the derivation, the result of an evaluation is a value: an abstraction evaluates to itself, and an application has the result of its third premise.

rec ev_value : [ |- eval M V] -> [ |- value V] =
/ total d (ev_value m v d) /
fn d => case d of
| [ |- ev_lam] => [ |- v_lam]
| [ |- ev_app D1 D2 D3] => ev_value [ |- D3]
;

let ex1 : [ |- eval (app (lam \x. x) (lam \y. y)) (lam \y. y)] =
  [ |- ev_app ev_lam ev_lam ev_lam];

rec val_ev : [ |- value V] -> [ |- eval V V] =
/ total /
fn w => let [ |- v_lam] = w in [ |- ev_lam]
;

§28.2 · Determinism

Evaluation is deterministic: a term has at most one value. Equality of terms is stated by an LF family with one constructor, eq_refl : eq M M, so that matching a derivation of eq V1 V2 against eq_refl makes V1 and V2 one metavariable, as matching against e_ref did in §11.4.

LF eq : tm -> tm -> type =
| eq_refl : eq M M
;

The proof is by induction on the first derivation, inverting the second. For an application, the two function results are equal by the induction hypothesis, so the two bodies are one M; the two argument values are equal likewise; and the two third premises then evaluate the same term, M V, so the induction hypothesis applies once more. Each let against eq_refl is what makes the next call well typed. Before it, D3 and E3 evaluate terms that the typechecker does not know to be equal.

rec det : [ |- eval M V1] -> [ |- eval M V2] -> [ |- eq V1 V2] =
/ total d (det m v1 v2 d) /
fn d, e => case d of
| [ |- ev_lam] => let [ |- ev_lam] = e in [ |- eq_refl]
| [ |- ev_app D1 D2 D3] =>
  let [ |- ev_app E1 E2 E3] = e in
  let [ |- eq_refl] = det [ |- D1] [ |- E1] in
  let [ |- eq_refl] = det [ |- D2] [ |- E2] in
  det [ |- D3] [ |- E3]
;

§28.3 · Evaluation and reduction

An evaluation determines a reduction sequence. §24.5 defined steps, sequences of β-reductions, and proved that they are closed under the contexts of application: steps_apl reduces the function of an application, steps_apr its argument, and sappend joins two sequences. In the case for application, ev_steps reduces the function to its abstraction, then the argument to its value, then contracts the redex at the root by beta1 and continues with the sequence for the body.

rec ev_steps : [ |- eval M V] -> [ |- steps M V] =
/ total d (ev_steps m v d) /
fn d => case d of
| [ |- ev_lam] => [ |- stop]
| [ |- ev_app D1 D2 D3] : [ |- eval (app M1 N) W] =>
  let [ |- S1] : [ |- steps M1 L] = ev_steps [ |- D1] in
  let [ |- S2] = ev_steps [ |- D2] in
  let [ |- S3] = ev_steps [ |- D3] in
  let [ |- R1] = steps_apl [ |- N] [ |- S1] in
  let [ |- R2] = steps_apr [ |- L] [ |- S2] in
  sappend [ |- R1] (sappend [ |- R2] [ |- next beta1 S3])
;

The annotation on the first let names the abstraction, L, which steps_apr needs explicitly. With the abstraction left to reconstruction, as steps_apr [ |- _], Beluga refuses the call, its type not being closed.

§28.4 · Divergence

Some terms have no value. Ω, the application of lam \x. app x x to itself, contracts to itself, and an evaluation of it would contain an evaluation of Ω again as its third premise. That observation is a proof by induction that no evaluation exists. omega inverts the first two premises, which can only be ev_lam, and calls itself on the third, a subderivation, so the measure is accepted. impossible d alone is refused, since ev_app concludes the type. That Ω has no evaluation is not a matter of which rules apply, but of their applying without end.

LF void : type = ;

rec omega : [ |- eval (app (lam \x. app x x) (lam \x. app x x)) V]
            -> [ |- void] =
/ total d (omega v d) /
fn d => case d of
| [ |- ev_app D1 D2 D3] =>
  let [ |- ev_lam] = [ |- D1] in
  let [ |- ev_lam] = [ |- D2] in
  omega [ |- D3]
;

The converse of ev_steps fails. The application of lam \x. lam \y. y to Ω reduces to lam \y. y in one step, the argument being discarded. Its evaluation would first evaluate the argument, Ω, and stuck turns any such evaluation into an evaluation of Ω, which omega refutes. So a term may reduce to a value and have none: call by value evaluates arguments that β-reduction is free to discard.

let reduces :
    [ |- steps (app (lam \x. lam \y. y)
                    (app (lam \x. app x x) (lam \x. app x x)))
               (lam \y. y)] =
  [ |- next beta1 stop];

rec stuck :
    [ |- eval (app (lam \x. lam \y. y)
                   (app (lam \x. app x x) (lam \x. app x x))) V]
    -> [ |- void] =
/ total /
fn d => let [ |- ev_app D1 D2 D3] = d in omega [ |- D2]
;

Counted: this section adds four LF families, one value and five functions, each function with a totality declaration that Beluga checks.

LF evaln : tm -> tm -> type =
| evn_lam : evaln (lam M) (lam M)
| evn_app : evaln M1 (lam M) -> evaln (M N) W
            -> evaln (app M1 N) W
;

let lazy :
    [ |- evaln (app (lam \x. lam \y. y)
                    (app (lam \x. app x x) (lam \x. app x x)))
               (lam \y. y)] =
  [ |- evn_app evn_lam evn_lam];

§29Normalization by evaluation#

§23 proved that every well-typed term of the simply typed calculus halts, by a logical relation. Normalization by evaluation computes a normal form instead, and it is a program rather than a proof about one. It evaluates a term into a semantic domain, in which a function is a computation-level function and β-reduction is ordinary application, and then reads the semantic value back as a normal form. Beluga accepts the program as total, every function carrying a totality declaration that it checks, so the program computes, for every well-typed term, an η-long normal form of the same type. That this normal form is βη-equal to the term, which is what makes it the term's normal form, is a further theorem and is not proved here. The section follows the distribution's literate development, after Berger and Schwichtenberg, with one change of representation that §29.2 explains.

§29.1 · Terms and normal forms

Terms are intrinsically typed, as in §23, over one base type b with no constants. The normal forms are β-normal and η-long, and come in two families declared together. A neutral term is a variable applied to normal arguments: rapp applies a neutral of arrow type to a normal argument, and the variables of the context are neutrals. A normal term is an abstraction, nlam, or, at base type only, an embedded neutral. Allowing embed at base type alone is what makes the normal forms η-long: a neutral of arrow type is not normal until it has been expanded into an abstraction. Terms are open in variables of type tm, in contexts of the schema tctx, and normal forms in neutral variables, in contexts of the schema ctx.

LF tp : type =
| b   : tp
| arr : tp -> tp -> tp
;

LF tm : tp -> type =
| app : tm (arr T S) -> tm T -> tm S
| lam : (tm T -> tm S) -> tm (arr T S)
;

schema tctx = some [t : tp] tm t;

LF neut : tp -> type =
| rapp  : neut (arr T S) -> norm T -> neut S

and norm : tp -> type =
| nlam  : (neut T -> norm S) -> norm (arr T S)
| embed : neut b -> norm b
;

schema ctx = some [t : tp] neut t;

§29.2 · The semantic domain

A semantic value at base type is a neutral term: having no constants, the base type has no other normal forms. At an arrow type it is a function from semantic values to semantic values, and it must accept arguments in contexts larger than its own. Reading a function back applies it to a fresh variable, and that variable lives in an extension of the context in which the function was made. A semantic function therefore takes, besides its argument, a context h and evidence that h extends its own context g, and it works in h. This is the Kripke function space, its extensions given as data.

The evidence is the inductive type Ext, which says that h is g with zero or more neutral variables added at the end. wk carries a neutral term along such an extension by recursion on the evidence, weakening by one variable at each Wk, and ext_trans composes two extensions.

inductive Ext : {g : ctx} {h : ctx} ctype =
| Id : Ext [g] [g]
| Wk : Ext [g] [h] -> Ext [g] [h, x : neut T[]]
;

rec wk : {h : ctx} Ext [g] [h] -> [g |- neut A[]]
         -> [h |- neut A[]] =
/ total w (wk h g a w) /
mlam h => fn w, r => case w of
| Id => r
| Wk w' : Ext [g] [h', x : neut T[]] =>
  let [h' |- R] = wk [h'] w' r in [h', x : neut T[] |- R[..]]
;

rec ext_trans : {k : ctx} Ext [g] [h] -> Ext [h] [k]
                -> Ext [g] [k] =
/ total w2 (ext_trans k g h w1 w2) /
mlam k => fn w1, w2 => case w2 of
| Id => w1
| Wk w2' : Ext [h] [k', x : neut T[]] =>
  Wk (ext_trans [k'] w1 w2')
;

Sem is defined by recursion on its type index, which is why it is declared stratified (§17): at an arrow type the semantic value takes semantic values as arguments, an occurrence to the left of an arrow, which an inductive definition does not permit: declared inductive, Sem fails Beluga's positivity check (§16.3). sem_wk weakens a semantic value, a neutral by wk and a function by composing the extension it will later be given with the one it is weakened along.

stratified Sem : {g : ctx} [ |- tp] -> ctype =
| Base : [g |- neut b] -> Sem [g] [ |- b]
| Arr  : {g : ctx}
         ({h : ctx} Ext [g] [h] -> Sem [h] [ |- A]
                    -> Sem [h] [ |- B])
         -> Sem [g] [ |- arr A B]
;

rec sem_wk : {h : ctx} Ext [g] [h] -> Sem [g] [ |- A]
             -> Sem [h] [ |- A] =
/ total /
mlam h => fn w, e => case e of
| Base r => Base (wk [h] w r)
| Arr [g] f =>
  Arr [h] (mlam k => fn w2 => f [k] (ext_trans [k] w w2))
;

The distribution's development states the extension as a substitution variable, $W : $[h |- g], and weakens by applying it, R[$W]. That version typechecks, and the Beluga this book was checked against cannot run it: evaluating an application of a function to a substitution stops with an internal error in opsem.ml, and every semantic function there receives one. With the extension given as data, every value the program passes is an ordinary one, and the normalizer runs.

§29.3 · Evaluation

An environment gives a semantic value to each variable of the term's context. Env is declared by typedef (§19.1) as a computation-level function, from a type T and a parameter variable of type tm T to a semantic value of type T; a let with the type annotation unfolds the abbreviation where a function needs to apply it. env_ext extends an environment by a value for a new last variable, and env_wk weakens every value in it along an extension.

typedef Env : {g : tctx} {h : ctx} ctype =
  {T : [ |- tp]} {#p : #[g |- tm T[]]} Sem [h] [ |- T];

rec env_ext : Env [g] [h] -> Sem [h] [ |- S]
              -> Env [g, x : tm S[]] [h] =
/ total /
fn s => let s : Env [g] [h] = s in
fn e => mlam T, #p => case [g, x : tm _ |- #p] of
| [g, x : tm S |- x] => e
| [g, x : tm S |- #q[..]] => s [ |- T] [g |- #q]
;

rec env_wk : {k : ctx} Ext [h] [k] -> Env [g] [h] -> Env [g] [k] =
/ total /
mlam k => fn w, s => let s : Env [g] [h] = s in
mlam T, #p => sem_wk [k] w (s [ |- T] [g |- #p])
;

eval is by recursion on the term. A variable is looked up in the environment. An abstraction becomes a semantic function: given an extension w of h and an argument e, it evaluates the body in the environment weakened along w and extended by e. An application evaluates the function, which can only be Arr, and applies it at the identity extension to the value of the argument. That application is β-reduction, performed by the computation level; the redex never exists as syntax. The measure is on the term, and the recursive call in the case for abstraction, which stands inside the semantic function and is made only when that function is applied, still receives a subterm, the body E.

rec eval : {h : ctx} [g |- tm S[]] -> Env [g] [h]
           -> Sem [h] [ |- S] =
/ total t (eval h g s t) /
mlam h => fn t, s => let s : Env [g] [h] = s in
case t of
| [g |- #p] => s _ [g |- #p]
| [g |- lam \x. E] =>
  Arr [h] (mlam k => fn w, e =>
    eval [k] [g, x : tm _ |- E] (env_ext (env_wk [k] w s) e))
| [g |- app E1 E2] =>
  let Arr [h] f = eval [h] [g |- E1] s in
  f [h] Id (eval [h] [g |- E2] s)
;

§29.4 · Reading back

reflect turns a neutral term into a semantic value, and reify turns a semantic value into a normal term, by recursion on the type, together. At base type a semantic value is a neutral, and reify embeds it. At an arrow type reify extends the context by a fresh neutral variable, reflects it, applies the semantic function to it at the one-step extension Wk Id, reifies the result and abstracts over the variable, which is η-expansion. reflect at an arrow type produces the semantic function that weakens the neutral along the extension it is given and applies it to the reified argument; app' builds that application.

rec app' : (h : ctx) [h |- neut (arr T[] S[])] -> [h |- norm T[]]
           -> [h |- neut S[]] =
/ total /
fn r, n => let [h |- R] = r in let [h |- N] = n in [h |- rapp R N]
;

rec reflect : {A : [ |- tp]} [g |- neut A[]] -> Sem [g] [ |- A] =
/ total a (reflect g a) /
mlam A => fn r => case [ |- A] of
| [ |- b] => Base r
| [ |- arr T S] =>
  let [g |- R] = r in
  Arr [g] (mlam h => fn w, e =>
    reflect [ |- S] (app' (wk [h] w [g |- R]) (reify [ |- T] e)))

and rec reify : {A : [ |- tp]} Sem [g] [ |- A]
                -> [g |- norm A[]] =
/ total a (reify g a) /
mlam A => fn e => case [ |- A] of
| [ |- b] => let Base [g |- R] = e in [g |- embed R]
| [ |- arr T S] =>
  let Arr [g] f = e in
  let [g, x : neut T[] |- N] =
      reify [ |- S] (f [g, x : neut T[]] (Wk Id)
                       (reflect [ |- T] [g, x : neut T[] |- x]))
  in [g |- nlam \x. N]
;

The type is explicit in both functions, and both are measured on it. Left implicit, recovered from the type of the argument, the same measure is refused at the call that reflects at the result type, although that type is smaller; explicit and matched on, it is accepted, as for bwd_closed' in §23.3. The normalizer evaluates a closed term in the empty environment, which no variable can consult, and reads the result back.

rec emp_env : Env [] [] =
/ total /
mlam T, #p => impossible [ |- #p]
;

rec nbe : [ |- tm A] -> [ |- norm A] =
/ total /
fn t => reify [ |- _] (eval [] t emp_env)
;

Applied to lam \f. f, at type (b ⇒ b) ⇒ b ⇒ b, nbe returns nlam \f. nlam \x. embed (rapp f (embed x)), the η-expansion of the identity. Applied to lam \f. lam \x. app f (app (lam \y. app f y) x) it returns nlam \f. nlam \x. embed (rapp f (embed (rapp f (embed x)))), the inner redex contracted beneath two binders. Counted: four LF families, two schemas, an inductive and a stratified type, a type abbreviation, and eleven functions, every one declared total and checked so under --coverage.

nlam \f. nlam \x. embed (rapp f (embed x))

inductive Rel : {g : tctx} {h : ctx} ctype =
| RNil  : Rel [] []
| RCons : Rel [g] [h] -> Rel [g, x : tm T[]] [h, y : neut T[]]
;

rec idenv : {h : ctx} Rel [g] [h] -> Env [g] [h] =
/ total r (idenv h g r) /
mlam h => fn r => case r of
| RNil => emp_env
| RCons r' : Rel [g, x : tm T[]] [h', y : neut T[]] =>
  env_ext (env_wk [h', y : neut T[]] (Wk Id) (idenv [h'] r'))
          (reflect [ |- T] [h', y : neut T[] |- y])
;

rec nbe_open : {h : ctx} {A : [ |- tp]} Rel [g] [h]
               -> [g |- tm A[]] -> [h |- norm A[]] =
/ total /
mlam h, A => fn r, t => reify [ |- A] (eval [h] t (idenv [h] r))
;

§30Error messages#

Beluga's error messages are terse, and they often name a consequence rather than its cause. This section shows how to read them: what a message contains and where its cause usually lies, and then the messages themselves, each produced by a short program, quoted as Beluga prints it, explained and repaired.

§30.1 · Reading a message

Beluga stops at the first error it finds and reports it in one form: a position, then the word Error and a description. A position names a line and a column. In this section each is counted from the first line of the listing above it. Beluga counts from the top of the file, and every listing here was checked appended to a development of the book, named beside it, so the numbers have been rebased; a position that falls inside the development is shown as such. Everything else in a message is reproduced exactly as Beluga printed it. Each was produced by running the listing, and the build checks, every time it runs, that Beluga still prints exactly that.

A file passes through four checks in order, and a message comes from the first that fails. Parsing reads the text into declarations. Reconstruction and typechecking infer what was omitted and check every term against its type. Coverage checks that every case analysis is exhaustive (§20.1), and totality checks every declared induction (§20.2). Knowing which check produced a message narrows the search: a parse error concerns the text alone and never a type, and a coverage failure is never a misspelt name.

The position in a message is where Beluga noticed the problem, which is not always where the problem lies. The parser reports the first token it could not accept, so a missing semicolon is reported at the declaration after it. Reconstruction works from left to right and commits to the first reading consistent with what it has seen, so a mistake at an early occurrence of a metavariable is reported at a later one, where that reading finally fails (§9.3). Two habits follow. When a message names a line that looks correct, look before it. And when a message cannot be understood, make the program smaller: delete, or replace with a hole (§19.4), everything the error does not need, until what remains is small enough to see.

The subsections after this one take the messages in the order of the four checks, each with a short program that produces it, the message, what it means and a repaired program. §30.8 collects mistakes that Beluga accepts without a word, and §30.9 the internal errors of the version this book was checked against.

§30.2 · Parsing

A parse error concerns the text alone. Its form does not vary: Failed to parse, the kind of declaration being read, and the token expected beside the token found. The token found is where the parser stopped, at the mistake or after it.

Expected the token `;', but got the token `rec'

A recursive function, like every grouped declaration, ends with a semicolon (§1.4.2). Here the first of two lacks one.

rec f1 : [ |- term] -> [ |- term] =
fn m => m

rec f2 : [ |- term] -> [ |- term] =
fn m => f1 m
;

line 4, column 1
Error: Failed to parse (mutual) recursive function declaration(s).
       Expected the token `;', but got the token `rec'.

The parser reads the body of f1, finds no semicolon, and arrives at the next declaration while still inside the first, so the position is line 4, the line of the second rec, two lines after the omission. With another keyword in place of rec, LF or inductive for instance, the message has the same cause.

rec f1 : [ |- term] -> [ |- term] =
fn m => m
;

rec f2 : [ |- term] -> [ |- term] =
fn m => f1 m
;

Expected the token `;', but got the token `.'

A grouped LF declaration is closed by a semicolon. The period belongs to the older notation, one declaration at a time (§1.4.2).

LF colour : type =
| red  : colour
| blue : colour
.

line 4, column 1
Error: Failed to parse LF type declaration block.
       Expected the token `;', but got the token `.'.

The two notations cannot be mixed within one declaration. The grouped form ends with a semicolon.

LF colour : type =
| red  : colour
| blue : colour
;

Expected the token `=>', but got the token `|'

Each branch of a case is a pattern, the arrow =>, and a body.

rec f3 : [ |- term] -> [ |- term] =
fn m => case m of
| [ |- z] [ |- tt]
| [ |- M] => m
;

line 4, column 1
Error: Failed to parse (mutual) recursive function declaration(s).
       Expected the token `=>', but got the token `|'.

Without the arrow, the parser reads the box meant as the body as more of the pattern, and goes on reading until the bar of the next branch, on line 4, where it reports the arrow missing.

rec f3 : [ |- term] -> [ |- term] =
fn m => case m of
| [ |- z] => [ |- tt]
| [ |- M] => m
;

Expected the token `)', but got the token `]'

Parentheses and brackets must nest.

let t2 = [ |- succ (succ z];

line 1, column 27
Error: Failed to parse value declaration.
       Expected the token `)', but got the token `]'.

The parser reports the bracket that arrived while a parenthesis was still open. In a long term the parenthesis left open may stand well to the left of the column named.

let t2 = [ |- succ (succ z)];

Expected the token `>', but got the token `,'

A tuple, the value of a block (§11.2), separates its components with semicolons.

rec fill2 : [b : block (x : term, u : oft x nat)
             |- oft (succ b.1) nat]
            -> [ |- oft (succ z) nat] =
fn d =>
  let [b : block (x : term, u : oft x nat) |- D] = d in
  [ |- D[<z, t_z>]]
;

line 6, column 12
Error: Failed to parse (mutual) recursive function declaration(s).
       Expected the token `>', but got the token `,'.

Inside a tuple a comma means nothing, so the parser, expecting the closing angle bracket after the first component, stops at the comma.

rec fill2 : [b : block (x : term, u : oft x nat)
             |- oft (succ b.1) nat]
            -> [ |- oft (succ z) nat] =
fn d =>
  let [b : block (x : term, u : oft x nat) |- D] = d in
  [ |- D[<z ; t_z>]]
;

Expected the token `rec', but got the token `od2'

Mutually recursive functions are joined by and, and each after the first repeats the keyword rec (§16.4).

rec ev2 : [ |- term] -> [ |- term] = fn m => od2 m
and od2 : [ |- term] -> [ |- term] = fn m => ev2 m
;

line 2, column 5
Error: Failed to parse (mutual) recursive function declaration(s).
       Exhausted alternatives in parsing:
         - Expected the token `rec', but got the token `od2'.
         - Expected the token `proof', but got the token `od2'.

The message lists two alternatives because and may also join Harpoon proofs, which begin with proof. The parser reports every token it would have accepted.

rec ev2 : [ |- term] -> [ |- term] = fn m => od2 m
and rec od2 : [ |- term] -> [ |- term] = fn m => ev2 m
;

Expected the token `/', but got the token `('

A totality declaration gives either a position or the function applied to its parameters, never both (§20.2).

rec nvn : [ |- numval N] -> [ |- oft N nat] =
/ total 1 (nvn _ v) /
fn v => case v of
| [ |- nv_z]   => [ |- t_z]
| [ |- nv_s V] => let [ |- D] = nvn [ |- V] in [ |- t_succ D]
;

line 2, column 11
Error: Failed to parse (mutual) recursive function declaration(s).
       Expected the token `/', but got the token `('.

After a position the parser expects the closing slash.

rec nvn : [ |- numval N] -> [ |- oft N nat] =
/ total 1 /
fn v => case v of
| [ |- nv_z]   => [ |- t_z]
| [ |- nv_s V] => let [ |- D] = nvn [ |- V] in [ |- t_succ D]
;

This operator is missing its left argument

Once a constructor is declared infix (§19.3), it stands between its arguments.

LF bool : type =
| true  : bool
| false : bool
| conj  : bool -> bool -> bool
;
--infix conj 5 left.
let q = [ |- conj true false];

line 7, column 14
Error: Failed to parse application.
       This operator is missing its left argument.

Written before its arguments, as an ordinary constructor is, conj has nothing on its left.

LF bool : type =
| true  : bool
| false : bool
| conj  : bool -> bool -> bool
;
--infix conj 5 left.
let q = [ |- true conj false];

Failed to parse old-style LF type or term constant declaration

// is not a comment (§1.4.3).

// the identity on terms
rec idt : [ |- term] -> [ |- term] = fn m => m;

line 1, column 4
Error: Failed to parse old-style LF type or term constant declaration.
       Expected the token `:', but got the token `the'.

Beluga reads // as a name and the line as a declaration of it in the older notation, name : type., so after the name it expects a colon and finds the word the. A comment begins with %.

% the identity on terms
rec idt : [ |- term] -> [ |- term] = fn m => m;

§30.3 · Names and reconstruction

Once parsed, each declaration is reconstructed and typechecked: every name is looked up, omitted arguments are inferred, and every term is checked against its type. The messages of this stage name a term and its type, or a name.

This free meta-variable is illegal

A constant misspelt inside a box.

let d1 : [ |- oft z nat] = [ |- t_zero];

line 1, column 33
Error: This free meta-variable is illegal.

Beluga takes a name that is declared nowhere, met inside a box, for a metavariable (§1.4.1). In a type such a name would be quantified implicitly; in a term nothing binds it, and it is illegal. So a misspelt constant is reported not as unknown but as an illegal metavariable. A variable used outside its context, as in [x : term |- succ y], gives the same message.

let d1 : [ |- oft z nat] = [ |- t_z];

Identifier simpp is unbound

A function name misspelt outside any box.

rec f4 : [ |- term] -> [ |- term] = fn m => simpp m;

line 1, column 45
Error: Identifier simpp is unbound.

At the computation level an unknown name is reported as unbound, and by name. The difference from the previous entry is the level: inside a box an undeclared name is taken for a metavariable, outside one it is an identifier that does not exist.

rec f4 : [ |- term] -> [ |- term] = fn m => simp m;

m is a bound computation variable

A computation variable inside a box (§3.3).