2
$\begingroup$

λ-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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.