<p>Ok, I think I've got it.</p>

<p>$eq_{k+1}$ calls (indirectly) $eq_k$, so, if I call $subset_{k+1}$ twice, I fall in an exponential blowup because of the two recursive calls of $eq_k$: it is simple to see with a "linear recurrence relation of constant order".</p>

CC BY-SA 3.0
2012-08-01T06:13:07.177Z
2012-08-01T06:13:07.177Z
Mycol
<p>I'm studying "<a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4048" rel="nofollow">A simple proof of a theorem of Statman</a>" by H.G. Mairson.</p>

<p>At page 4, he encodes set/type theory in lambda calculus.
In particular, note che "op" trick in the definition of $eq_{k+1}$.</p>

<p>Mairson stress the fact that this trick is essential, because writing $subset_{k+1}$ twice would cause exponential blowup in term size.
I'm asking why! That would not just double the term size? </p>

<lo.logic><lower-bounds><lambda-calculus>
Exponential blowup in Simple Proof of a theorem of Statman by Mairson
Mycol
# Exponential blowup in Simple Proof of a theorem of Statman by Mairson

(Asked by: username_0 on 2012-07-28)

I'm studying "[A simple proof of a theorem of Statman](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.4048)" by H.G. Mairson.

At page 4, he encodes set/type theory in lambda calculus.
In particular, note che "op" trick in the definition of $eq\_{k+1}$.

Mairson stress the fact that this trick is essential, because writing $subset\_{k+1}$ twice would cause exponential blowup in term size.
I'm asking why! That would not just double the term size?

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


---

## 1 answers

### Answer by username_0 on 2012-08-01. Score: 1

Ok, I think I've got it.

$eq\_{k+1}$ calls (indirectly) $eq\_k$, so, if I call $subset\_{k+1}$ twice, I fall in an exponential blowup because of the two recursive calls of $eq\_k$: it is simple to see with a "linear recurrence relation of constant order".


---

