I've heard that the functions that are definable in simply-typed $\lambda$-calculus is the class of extended polynomials.

However, it is still not clear to me what exactly is extended polynomials. Could someone explain that to me? Some pointers would be good as well.



1 Answer 1


It turns out the definition is straightforward as seen in [1]. And as an example, exponentiation is not definable in simply-type $\lambda$-calculus.

The class of extended polynomials is the smallest class of func- tions over N which contains:

  1. the constant functions: 0 and 1,
  2. projections,
  3. addition,
  4. multiplication,
  5. the function ifzero(n, m, p) = if n = 0 then m else p

  1. Definable functions in the simply typed lambda-calculus by M. Zakrzewski (2007)

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.