Simply typed lambda calculus has a combinatory logic equivalent with the same expressive power without the need of defining names via lambda abstraction.

Is there a formalism as powerful as System F but based on combinatory logic?

  • $\begingroup$ Going in a different direction on the lambda cube: polymorphic types. Similar question on TCS. $\endgroup$ Jun 7, 2018 at 7:47
  • $\begingroup$ @PeterTaylor I know these questions, but I don't need the extra power of the type system they ask for. I only need sufficient power to type lambda encoded natural numbers. $\endgroup$ Jun 7, 2018 at 9:32
  • $\begingroup$ I thought that combinatory logic is untyped, and is equivalent to the untyped lambda calculus, not to the simply-typed one. I mean, we have things like kkk=k which can not be typed in STLC. Can you elaborate? $\endgroup$
    – chi
    Jun 7, 2018 at 11:00


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.