# NOTE: Practical issue in de Bruijn indices

Two years ago, I have a post about de Bruijn indices. I don't think de Bruijn indices order is important, it turns out, that's wrong!

## 1. Introduction

What's the order of indices? It means we have two choices

- converts
`λy.λx.x`

to`λλ1`

- converts
`λy.λx.x`

to`λλ0`

and the second one is better in practice! Because with this encoding, we can work with prepending-list better.

## 2. Expand

Let's see how this works, first, we need a conversion from surface/concrete syntax to our core form.

(: depth : Sexp -> Nonnegative-Integer) (define (depth t) (match t [`(λ (,x) ,body) (add1 (depth body))] [`(,f ,a) (max (depth f) (depth a))] [else 0])) (: convert : (->* (Sexp) ((Immutable-HashTable Symbol Nonnegative-Integer)) term)) (define (convert t [name->index (make-immutable-hash '())]) (match t [`(λ (,x) ,body) (S.lam (convert body (hash-set name->index (cast x Symbol) (depth body))))] [`(,t1 ,t2) (S.app (convert t1 name->index) (convert t2 name->index))] [x (S.var (hash-ref name->index (cast x Symbol)))]))

This is boring, anyway just record how depth we go that far and refer them back for variables.

## 3. evaluation(\(\beta\)-reduction)

- variable case: we use a helper function =proj=(stands for projection in environment). I will go back to this core function later.
application case:

- evaluate function to get the value of function.
- evaluate argument to get the value of argument.

Then we have two cases.

- value of lambda case: apply lift host-lambda to get result
- Not a lambda: prepare a stuck application form.

- lambda case: create a host-lambda, which will evaluate its body(binder) with extended environment!

(: eval : Env Term -> Val) (define (eval env t) (match t [(S.var i) (proj env i)] [(S.app t u) (let ([t- (eval env t)] [u- (eval env u)]) (match t- [(V.lam f) (f u-)] [else (V.app t- u-)]))] [(S.lam binder) (V.lam (λ (u) (eval (cons u env) binder)))]))

Here, since environment is prepended, we can simply count down the counter recorded in the variable. When the counter is zero, the value is what we are looking for, or it's a stuck variable.

(define (proj env i) (match env ; returns a stuck since we don't always have value in environment in lambda calculus [null (V.var i)] [(cons v env) (if (= i 0) v (proj env (sub1 i)))]))

### 3.1. Run it

(eval '() (convert '(((λ (v) (λ (f) (f v))) k) (λ (x) x)) (make-immutable-hash '((k . 100)))))

## 4. Appendix

### 4.1. Environment

(define-type Env (Listof Val))

### 4.2. Term

(define-type term (U S.var S.lam S.app)) (struct S.var ([v : Nonnegative-Integer])) (struct S.lam ([binder : term])) (struct S.app ([fn : term] [arg : term]))

### 4.3. Value

(define-type Val (U V.lam V.stuck)) (struct V.lam ([host-lambda : (Val -> Val)])) (define-type V.stuck (U V.var V.app)) (struct V.var ([v : Nonnegative-Integer])) (struct V.app ([fn : Val] [arg : Val]))