# What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?

Let $\Lambda$ be a set of strongly normalizing lambda terms.
Let $\mathtt{NF} : \Lambda \rightarrow \Lambda$ be evaluation to the normal form.
Let $\lvert x\rvert : \Lambda \rightarrow \mathbb{N}$ be size of a term in number of symbols.
The following function seems to be well defined:

$$f_\Lambda:\mathbb{N} \rightarrow \mathbb{N}$$ $$f_\Lambda(n) = \max_{t \in \Lambda, \lvert t \rvert \leq n} \lvert\mathtt{NF}(t)\rvert$$

What is the rate of growth of $f_\Lambda$?

Can we define some lower and upper bound in fast growing hierarchy?

The maximal blowup in termsize of simply typed lambda calculus is non-elementary (2 ↑↑ O(n) see e.g. [1] page 72). This is not exactly what you are asking for, but since typed lambda calculus is a strongly normalizing subset of untyped lambda calculus, it should give you some lower bounds.

I am not sure if the general question can be answered. Untyped lambda calculus is Turing-complete, the strongly normalizing fragment is then equivalent to the set of terminating programs. Since membership in this set is already undecidable, I would not expect that an upper bound on the size of normal forms can be shown.

[1] Morten Heine Sørensen and Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier Science Inc., New York, NY, USA, 2006.

• You are of course right that the function is not well defined, because we can't determine if a term is strongly normalizing. Thanks. But doesn't the blow-up depend on the type-system used? I.e. if we admit System F, shouldn't we be able to proof normalizing much bigger functions than the one you stated? I've found a pdf here. Can you point me to the result? – Łukasz Lew Jun 14 '18 at 15:51
• Sorry you are right - I was talking of simply typed lambda calculus, I will amend the answer. – lambda.xy.x Jun 14 '18 at 16:09
• It also seems the version you found differs significantly from the published book. It is chapter 3.7 Expressibility, page 72 in the version on Google Books – lambda.xy.x Jun 14 '18 at 16:20
• Just as a comment, the function is well-defined in the mathematical sense, for any set of normalizing terms. Certainly it is not computable in general. Compare the busy beaver function. – cody Jun 14 '18 at 19:48