1
$\begingroup$

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?

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Łukasz Lew Jun 14 '18 at 15:51
  • $\begingroup$ Sorry you are right - I was talking of simply typed lambda calculus, I will amend the answer. $\endgroup$ – lambda.xy.x Jun 14 '18 at 16:09
  • $\begingroup$ 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 $\endgroup$ – lambda.xy.x Jun 14 '18 at 16:20
  • 1
    $\begingroup$ 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. $\endgroup$ – cody Jun 14 '18 at 19:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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