I have heard that Lean uses the locally nameless representation for handling binders, yet if I input an expression that has a bound variable in it, the bound variable is not displayed using its de Bruijn index (example [click at the end of the #check line]). Is there a detailed description of the algorithm that Lean uses for this? How is the input parsed and represented internally and how does the internal representation get translated for display? What happens if the original names can no longer be used for display, for example, if using them would produce an expression no longer alpha equivalent to the internal one? How are new names chosen in that case?
type expr = | Bound of index (** de Bruijn index *) | Atom of atom (** primitive symbol *) | Type (** the type of types *) | Prod of (Name.ident * ty) * ty (** dependent product *) | Lambda of (Name.ident * ty) * expr (** lambda abstraction *) | Apply of expr * expr (** application *)
you will see that
Lambda take a
Name.ident, i.e., they remember what the name of the bound variable was, even though de Bruijn indices are used (that's the
Bound constructor). When expressions are printed out (see
print_expr) an auxiliary function
print_binders figures out what strings it should use to print out de Bruijn indices. It tries to use the string that is stored in
Prod, if possible, otherwise it finds another name (see
Name.refresh which find such a name).
In addition, here are my blog posts on "How to implement type theory" (part 1, part 2, part 3). Note however that the source code for these tutorials is somewhat messed up. The tutorials themselves still explain some basic ideas.
I know you want to implement first-order logic, but that is irrelevant. Many things that are explained in the above material will be useful in your endavors.
I'm not sure what you mean by algorithm, but it sounds like you want to know how an expression is stored internally in Lean. Let's take your example:
∀ (x : ℕ), x ≥ 0
Even if you turn off all the notation, Lean will display it with variables since the input and output of Lean is variable based. But you are correct that internally it also uses de Bruijn indices. To see this, you can do the somewhat complicated looking:
#eval ```(∀ (x : ℕ), x ≥ 0).to_raw_fmt.to_string
The triple-quotes around your code turn it into a lean expression, so it has type
expr instead of type
.to_raw_fmt.to_string just prints the expression to a string representing the underlying constructors for the expression.
(pi x default [macro annotation (const nat )] (app (app [macro annotation (const ge )] (var 0)) [macro prenum]))
Unfortunately, this still shows a lot of macros (which are sort of promises to elaborate that part of the expression later). This can be fixed by putting in a more elaborated formula to begin with:
#eval ```(∀ x : nat, nat.ge x nat.zero).to_raw_fmt.to_string -- (pi x default (local_const nat nat (const 4._.98 )) (app (app (local_const nat.ge nat.ge (const 4._.99 )) (var 0)) (local_const nat.zero nat.zero (const 4._.100 ))))
var 0 is how the variable
x ≥ 0 is represented. It has a de Bruijn index of 0 pointing it to the binder
pi x. (Notice the variable name
x is also there, but is stored with the binder instead of the variable).
This is also documented in the paper A Metaprogramming Framework for Formal Verification which covers the expression datatype in more detail.
The general way one accesses such low level details (including some of the tricks I used like the triple back quotes) is through meta-programming. For Lean 3, see Tutorial: tactic writing in Lean. For Lean 4, see (work in progress) Lean 4 metaprogramming book.