Lambda body reduction in Lambda calculus

Question

I'm studying lambda calculus with De Bruijn indexes, and have these functions.

$$ zero := (\lambda\lambda.1)\\ succ := (\lambda\lambda\lambda.2 (3 2) 1) $$

Now I want an algorithm to reduce $succ\ zero$

$$ \beta\ succ\ zero \\ \beta\ (\lambda\lambda\lambda.2 (3 2) 1)\ (\lambda\lambda.1)\\ \beta\ \lambda\lambda.2 ((\lambda\lambda.1) 2) 1 $$

where $\beta$ is the beta reduction function.

I tried to come up with an algorithm but it stops here because the head of the expression is not an application it wouldn't go further. I will continue the reduction that I like to implement

$$ \beta\ \lambda\lambda.2 ((\lambda\lambda.1) 2) 1\\ \beta\ \lambda\lambda.2 (\lambda.1) 1\\ \beta\ \lambda\lambda.2 1\\ $$

The problem that I'm facing is that in my program the application is a data type with two parameters App term term and this term $2 (\lambda.1) 1$ corresponds to this in code App (App 2 (Lamb 1 1)) 1). By recursing on this structure I will never match the term $(\lambda.1) 1$ and will never be able to reduce it

I need this to compare numbers, for example

$$ one := (\lambda\lambda.2 1) \\ one' := \beta\ (succ\ zero) $$

If I want $one$ to be syntactically equal to $one'$ I need to be able to normalize the function body, any ideas on how to approach this?

Answer 1

My definition of succ is wrong, the correct is $\lambda\lambda\lambda.2 (3 2 1)$ not $\lambda\lambda\lambda.2 (3 2) 1$

Answer 2

The PL Zoo has a programming language lambda which uses de Bruijn indices (see the type term) and explicit substitutions (described here) to implement reduction, see norm, which actually implements four different strategies, depending on what flags it is given.