Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
I'm studying "A simple proof of a theorem of Statman" 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?
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".
