Terms and binders

The kernel checks core terms: nested vectors without names, where variables are de Bruijn indices and constants are content ids. You write surface data: nested vectors with symbols for variables and aliases for constants. The elaborator turns the second into the first.

Core terms

term? in term.clj accepts eight forms: [:sort level], [:bound i], [:nat n], [:const "sha256:..." [levels]], [:app f a], [:lam type body mode], [:pi type body mode] and [:let type value body], where mode is :explicit or :implicit. rainbow.term has a constructor for each: sort-term, bound, constant, application, lambda-term, pi-term (both default to :explicit) and let-term. The calculus gives each form’s typing rule, and Universes covers levels.

De Bruijn indices

[:bound 0] is the variable of the nearest enclosing :lam, :pi or :let, [:bound 1] the one around it, and so on. The first theorem in the repository, logic/polymorphic-identity (source), says that for every type A in universe u and every x : A there is an A:

;; type: (A : Sort u) -> (x : A) -> A
[:pi [:sort [:param u]]
     [:pi [:bound 0] [:bound 1] :explicit]
     :explicit]

;; proof: fn [A] fn [x] x
[:lam [:sort [:param u]]
      [:lam [:bound 0] [:bound 0] :explicit]
      :explicit]

In the type, the inner domain [:bound 0] is A. Under both binders A has moved one step out and is [:bound 1]. In the proof, the body [:bound 0] is x.

Terms that differ only in variable names are the same vector, with the same hash. You rarely write indices yourself: the elaborator computes them from names, and shift and instantiate in rainbow.term do the arithmetic.

rainbow.term/pretty prints a core term on one line, with #i for indices:

(fn [_:Sort([:param u])] (fn [_:#0] #0))

lein show <alias> prints a statement with names and notation. It is only a view; the kernel never sees it.

Surface helpers

In surface data the identity uses names:

'[:forall [[A [:sort [:param u]]] [x A]] A]

Proof modules build such vectors with rainbow.math.logic.function (source):

(defn forall [bindings body] [:forall (vec bindings) body])
(defn lam [bindings body] [:fn (vec bindings) body])
(defn arrow [& values] (into [:->] values))
(defn app [function & arguments] (into [:app function] arguments))
(defn const* [alias levels] [:const alias (vec levels)])

forall and lam elaborate to one :pi or :lam per binding. (arrow A B C) is A -> (B -> C), a non-dependent :pi. (app f a b) becomes [:app [:app f a] b], and const* takes an alias that the elaborator resolves to a content id.

A binding is [name type] or [name type :implicit]. Names in the body are quoted symbols, 'x. 'Prop stands for [:sort [:zero]], and [:sort level] gives any other universe.

rainbow.math.logic.function also builds equality, involutive, injective, surjective, bijective and injective2. rainbow.math.logic.proposition has truth, falsity, conjunction, disjunction, negation, equivalence, existence, unique-existence, uniqueness, equality and inequality, plus introduce-equivalence, forward-equivalence and backward-equivalence. Each returns a vector that refers to a declared constant.

(defn conjunction [left right]
  (app (const* 'proposition/conjunction []) left right))

(defn existence [level carrier predicate]
  (app (const* 'proposition/existence [level]) carrier predicate))

The connectives themselves are ordinary impredicative definitions in that file, like equality/Eq on Universes.

Binder modes

The kernel keeps :explicit or :implicit in each :lam and :pi. A function checked against a function type must have the same mode, or it fails with :kernel/binder-mode-mismatch. The elaborator inserts no implicit arguments, so you pass every argument whatever its mode. proposition/equivalence-congruence has implicit binders.

Let

The surface form [:let name type value body] becomes [:let type value body], with name as [:bound 0] in body. The kernel checks value against type and reduces a let by substituting the value.

(elaborate/core-expression (environment/empty-environment)
                           '[:fn [[A [:sort [:succ [:zero]]]] [a A]] [:let b A a b]])
;; :term
[:lam [:sort [:succ [:zero]]]
      [:lam [:bound 0] [:let [:bound 1] [:bound 0] [:bound 0]] :explicit]
      :explicit]

Natural-number literals

[:nat 3] has type data/Nat and means data/succ applied three times to data/zero. It becomes a constructor only when a recursor inspects it. Six operations, from algebra/nat-add to nat/decide-at-most, compute directly on literals, each pinned to the content id of its definition (source).

Two terms are definitionally equal when their normal forms match. Reduction runs on kernel/*reduction-budget*, 1,000,000 steps by default, and stops with :kernel/resource-limit when it runs out. The calculus lists the reduction rules and the six native operations.