<p>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.</p>

<p>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.</p>

<p>[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.</p>

CC BY-SA 4.0
2018-06-14T15:51:51.103Z
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](http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf). Can you point me to the result?
Łukasz Lew
CC BY-SA 4.0
2018-06-14T16:09:09.093Z
Sorry you are right - I was talking of simply typed lambda calculus, I will amend the answer.
lambda.xy.x
CC BY-SA 4.0
2018-06-14T16:20:07.520Z
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](https://books.google.at/books?id=_mtnm-9KtbEC&pg=PA55&hl=de&source=gbs_toc_r&cad=3#v=onepage&q&f=false)
lambda.xy.x
CC BY-SA 4.0
2018-06-14T19:48:52.613Z
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](https://en.wikipedia.org/wiki/Busy_beaver#The_busy_beaver_function_%CE%A3).
cody
CC BY-SA 4.0
2018-06-14T11:50:38.330Z
2018-06-14T16:09:19.710Z
2018-06-14T16:09:19.710Z
lambda.xy.x
<p>Let $\Lambda$ be a set of strongly normalizing lambda terms.<br>
Let $\mathtt{NF} : \Lambda \rightarrow \Lambda$ be evaluation to the normal form.<br>
Let $ \lvert x\rvert : \Lambda \rightarrow \mathbb{N}$ be 
size of a term in number of symbols.<br>
The following function seems to be well defined:</p>

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

<p>What is the rate of growth of $f_\Lambda$?</p>

<p>Can we define some lower and upper bound in <a href="http://googology.wikia.com/wiki/Fast-growing_hierarchy" rel="nofollow noreferrer">fast growing hierarchy</a>?</p>

<lo.logic><lambda-calculus>
What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?
Łukasz Lew
# What's the expressive/compressive power of strongly normalizing subset of untyped lambda calculus?

(Asked by: username_0 on 2018-06-14)

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](http://googology.wikia.com/wiki/Fast-growing_hierarchy)?

**Tags:** lo.logic, lambda-calculus


---

## 1 answers

### Answer by username_1 on 2018-06-14. Score: 4 | Accepted answer

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.

> **Comments:**
> **username_0**: 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](http://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf). Can you point me to the result?  
> **username_1**: Sorry you are right - I was talking of simply typed lambda calculus, I will amend the answer.  
> **username_1**: 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](https://books.google.at/books?id=_mtnm-9KtbEC&pg=PA55&hl=de&source=gbs_toc_r&cad=3#v=onepage&q&f=false)  
> **username_2**: 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](https://en.wikipedia.org/wiki/Busy_beaver#The_busy_beaver_function_%CE%A3).  

---

