Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.

  • 3
    $\begingroup$ You may find this answer by Herman Geuvers to a similar question useful. And the whole thread is very illuminating. $\endgroup$ Aug 25 '19 at 17:50
  • 1
    $\begingroup$ @AntonTrunov you might as well turn your comment into an answer. $\endgroup$
    – cody
    Aug 25 '19 at 21:50
  • $\begingroup$ So if I understand correctly you can not write the Y-combinator but only "looping" combinators. So you can not write (general) recursive functions in type-in-type. $\endgroup$
    – Labbekak
    Sep 7 '19 at 8:18

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.