How to work with De Bruijn indexes?

[joneshf]

I'm writing a program that takes a Dhall expression and compiles it to another language. This language does not support accessing shadowed variables. So, if there is a Dhall expression like:

\(x : Bool) -> \(x : Bool) -> x@1

Something has to be done to make that work. What's the correct way to deal with this? It sounds like renaming all bound variables is what's necessary, but each time I try to implement it it doesn't work quite right. Is there a function I'm missing that might already be doing the right thing?

[Gabriella439]

@joneshf: It's going to be very similar to how α-normalization works, except that instead of renaming each variable to _ you will be renaming each variable to some globally unique name.

See: https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#%CE%B1-normalization

For example, this is the judgment for renaming a variable named x to _ when x is not _:

A₀ ↦ A₁
↑(1, _, 0, b₀) = b₁
b₁[x ≔ _] = b₂
↑(-1, x, 0, b₂) = b₃
b₃ ↦ b₄
───────────────────────────────  x ≠ _
λ(x : A₀) → b₀ ↦ λ(_ : A₁) → b₄

If you were instead renaming the variable x to some globally unique variable named y then you would just replace all occurrences of _ in the above judgment with y:

A₀ ↦ A₁
↑(1, y, 0, b₀) = b₁
b₁[x ≔ y] = b₂
↑(-1, x, 0, b₂) = b₃
b₃ ↦ b₄
───────────────────────────────  x ≠ y
λ(x : A₀) → b₀ ↦ λ(y : A₁) → b₄

Same thing for the other α-normalization rules: just replace _ with the variable you are renaming to and they should work

[joneshf]

Thanks, that make sense!

And it worked too 🎉!

[Gabriella439]

You're welcome! 🙂

[f-f]

Right, the example expression is broken in my implementation as well so I guess the easiest way to go is to make α-normalization "parametric" 🤔

@Gabriel439 actually would it make sense to "unexpose" De Bruijn indices?
Access to the shadowed variable would be lost, but it's easily fixed by renaming the variable (that is, it's not a critical loss for the user IMO).
OTOH implementation(s) would have an easier time in converting the semantics of the languages

[Gabriella439]

@f-f: It wouldn't make it easier to implement the language. A conforming implementation has to support α-normalization to power both equivalence checking and also for semantic integrity checks and α-normalization requires support for De Bruijn indices.