0
$\begingroup$

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?

$\endgroup$

2 Answers 2

1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Thank you so much!!! $\endgroup$
    – geckos
    Aug 21, 2022 at 23:35
  • $\begingroup$ Excuse me, but what is the Dot constructor denoting? I saw that you used explicit substitutions, what are the pros and cons of having explicit substitutions? $\endgroup$
    – geckos
    Aug 21, 2022 at 23:49
  • $\begingroup$ Ohh ok is in the blog post, thanks!!! $\endgroup$
    – geckos
    Aug 21, 2022 at 23:50

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.