2
$\begingroup$

I happened to stumble upon this sequence. It defines the function $BB_{\lambda}(n)$, which is the maximum normal form size of any closed lambda term of size $n$.

However, I noticed this sequence only considered closed lambda terms. There wasn't another sequence that included open lambda terms. For convenience, I will call this other function that does include open terms $BB2_{\lambda}(n)$.

Some intuition tells us that $BB2_{\lambda}(n) \ge BB_{\lambda}(n)$. But, having free variables does not seem like a large advantage.

My question is: Is $BB2_{\lambda}(n) = BB_{\lambda}(n)$ true, and why so? If not, is there a significant difference between the two?

Improve this question
$\endgroup$
3
  • $\begingroup$ How do you define the size of a free variable? The (to me rather unusual) definition of the size function in the OEIS only works for closed terms. $\endgroup$
    – sparusaurata
    Commented Aug 8 at 15:19
  • $\begingroup$ @sparusaurata The function seems to based on Binary Lambda Calculus, which is in turn based on De Bruijn Indexes. In this format, variables are positive integers that are bound by the Nth previous enclosed lambda. If there are less than N lambdas before it, it is not bound, and is therefore free. $\endgroup$
    – undefned
    Commented Aug 8 at 17:06
  • $\begingroup$ I personally dislike De Brujin indexes, though. And I do agree: the size definition is unusual outside of Binary Lambda Calculus. $\endgroup$
    – undefned
    Commented Aug 8 at 17:09

1 Answer 1

Reset to default
0
$\begingroup$

I think the name BB2λ is unnecessarily confusing since there is already a BBλ2 [1], so let's call it BBOλ instead.

The size of a free variable is perfectly well defined in de Bruijn notation. Assuming 1-based indices, the size of index i is 1+i, consistent with A333479.

For an open term M consisting of a single index i we have size(M) = i+1 and since M is in normal form, this proves BBOλ(n) >= n for all n >= 2. This makes BBOλ(n) larger than BBλ(n) for n=2,3,5.

For M = (λ 1 1) i of size 11+i we have normal form i i of size 2i+4, so BBOλ is also larger at n=19..23. I expect free variables are otherwise not helpful in creating faster growth.

[1] https://oeis.org/A361211

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .