The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed function and, with the addition of the Y combinator, you gain Turing completeness (and adding other recursion combinations yields different recursive classes).

I highly suspect that the same can be done for System $F_{\omega}$ but I'm not sure how quite to do this. Is there a set of combinators that form a complete basis typed under system F-omega?

Additionally, in system $F$ type checking is only decidable with type hints (Church style). Would a combinator basis for system $F$ still have decidable type checking? If true would this still also be true of a complete basis for system $F_\omega$?

What about complete basis and decidability of type checking for Per Martin-Löf typing systems?

  • $\begingroup$ I can't find seem to find a complete basis typed under system F. I'd very much so like to first find a complete basis under system F first before system F-omega $\endgroup$ – Jake Apr 17 '14 at 18:23

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.