The calculus

The kernel, src/rainbow/kernel.clj, calls itself a “small trusted checker for Rainbow’s initial dependent-function calculus”. The term language is in term.clj.

Terms

mode is :explicit or :implicit. Terms carry no names: variables are indices and constants are content ids, so two terms that mean the same thing are the same vector. Modules write a surface syntax with named binders, and the elaborator, rainbow.elaborate, turns it into these terms for the kernel to check (Terms and binders).

Typing

infer computes a term’s type and check checks a term against an expected type (source).

• [:sort l] has type [:sort [:succ l]].
• [:bound i] has the type the local context gives it.
• [:const id levels] has the declared type of id, with one level from levels for each universe parameter.
• [:nat n] has type data/Nat.
• [:app f a]: the type of f must reduce to a Pi type and a must check against its domain. The result is the Pi’s body with a substituted.
• [:lam domain body mode]: domain must be a type, and the result is a Pi type with the same domain and mode.
• [:pi domain body mode]: domain and body must be types. At levels l1 and l2, the Pi lives at [:imax l1 l2].
• [:let type value body]: value checks against type, and the body’s type has value substituted.

A lambda checked against a Pi type needs the same binder mode and a definitionally equal domain.

Universe levels

A level is [:zero], [:succ l], [:max l1 l2], [:imax l1 l2] or [:param name]. [:sort [:zero]] is Prop, and data/Nat and data/Bool live in [:sort [:succ [:zero]]]. Since imax l 0 is 0, Prop is impredicative, which the corpus uses to define Leibniz equality. A declaration lists its universe parameters as distinct symbols, such as ['u], and a term using any other parameter is rejected. Universes gives the normalisation rules.

Declarations

kernel/add-declaration is the only way into an environment (source). The kernel accepts a declaration only when:

• the kind is :definition, :theorem or :axiom
• the type is closed, well formed, and has a sort as its type
• a definition or theorem has a closed value that checks against the type, and an axiom has no value
• the declared dependencies are exactly the constants in the type and value
• any id supplied with it equals the id computed from its content
• none of its aliases already names a different declaration

Transparency is :reducible, :semireducible or :opaque (the default), and only the first two unfold. Corpus modules typically add definitions as :reducible and theorems as :opaque. kernel/axioms returns the axioms a declaration depends on, transitively.

Reduction and definitional equality

• beta: a lambda applied to an argument substitutes it
• delta: a reducible or semireducible constant unfolds to its value
• zeta: a let substitutes its value into its body
• iota: a recursor applied to a constructor reduces to the matching case
• eta: during normalisation, (fn [x] (f x)) becomes f when x is not free in f
• native: six natural-number operations compute on literals

A definition that would unfold into itself is rejected as cyclic. Two terms are definitionally equal when they are identical or their normal forms are.

Inductive blocks and recursors

kernel/add-inductive-block adds a data type from one descriptor: universe parameters, ordinary parameters (such as the element type A of data/List), a result sort level and constructors with named fields. Blocks have no indices. The kernel generates the type, its constructors and a recursor named <alias>.rec, such as data/Nat.rec for the data/Nat block in rainbow.data.inductive. The recursor takes the parameters, a motive into a sort at a fresh level, one case per constructor and a target. A case receives the constructor’s fields and an induction hypothesis after each recursive field.

The members go in together. Adding one alone with add-declaration is rejected, and so is a block id that does not match the descriptor. A recursive occurrence must be a whole field, [:self]. Anywhere else, even as the result of a function-typed field, it is rejected with :kernel/non-strictly-positive. Fields may refer to parameters and earlier fields of the same constructor. Inductive types shows how to write a block.

The reduction budget

Each reduction step costs one unit of kernel/*reduction-budget*, 1,000,000 by default. When it runs out, the kernel stops with :kernel/resource-limit (kernel/normalize returns :resource-limit), and the question is undecided. lein verify --bundle --reductions N raises the budget. kernel/normalize also caps, with :max-unary-nodes (default 1,000,000), the successor nodes it writes when turning literals back into unary numerals.

Native natural numbers

[:nat n] becomes a constructor form only when a recursor inspects it. algebra/nat-add, nat/multiply, nat/predecessor (0 for 0), nat/distance (absolute difference), nat/decide-equality and nat/decide-at-most compute directly on closed arguments that reduce to numerals. Each is pinned to the content id of the definition it computes (source), and rainbow.kernel-native-test compares each with that definition’s unary reduction. On other arguments the definition unfolds as usual.