λ-terms can be split in two categories: EAL and non-EAL typeable terms. It is known not only that EAL-typeable terms can be reduced to normal form in polynomial time, but that the reduction can be executed through Lamping's abstract algorithm optimally.
What are the distinct features that make a term EAL-typeable? I've heard words such as "stratifiable", but I'm not sure what that mean. What is the intuitive reasoning behind a term being in EAL?