1
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • $\begingroup$ Going in a different direction on the lambda cube: polymorphic types. Similar question on TCS. $\endgroup$
    – Peter Taylor
    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$
    – user3368561
    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

0

Reset to default

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.