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?


1 Answer 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".


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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