De Bruijn levels is a measure in lambda terms for variables. Suppose an initial natural number k, a lambda term t and a variable x presents in t, the level of x is the number of abstraction encountered between the root of the term and the associated abstraction of x added to k.
(* For instance, in the following term, if we start with k = 0 then the level of x is 0. *)
fun x -> x
(* In the following case, if k = 0 then the level of x is 0 and the level of y is 1. *)
fun x -> fun y -> x + yThe initial natural number can be understood as the number of free variables.
(* In the expression below y is free, then we start with k = 1 and the level of x is 2. *)
fun x -> x + yFirst consequence of that, levels of bound variables depend on the initial natural number k. Second consequence of that, the meaning of a term depends on k.
These levels are used in a formalism to represent variables. It gives an order and a unique name for variables (except in two branches of an application) which avoids variable capture.
(* The first expression is an usual lambda-term, the second one is its level representation. *)
fun x -> (fun y -> x y) x)
fun -> (fun -> 0 1) 0)Although this representation is much less known than the De Bruijn indices representation, there are some useful characteristics. Among them, we can use levels into structures without binders which is not the case with indices.
This library is a collection of interfaces, implementations and functions that can help you in yours use of De Bruijn levels.
Here is the current version of the documentation. This doc is generated by coqdoc with the extension coqdocjs.
To Build and install manually, do:
git clone https://github.com/JordanIschard/DeBrLevel.git
cd DeBrLevel
dune build @install Note
The package is not submitted yet, but we have great hope to create an opam package and add our project to the coq community repository.