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


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.