3
$\begingroup$

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

$\endgroup$
  • 3
    $\begingroup$ You may find this answer by Herman Geuvers to a similar question useful. And the whole thread is very illuminating. $\endgroup$ – Anton Trunov Aug 25 at 17:50
  • 1
    $\begingroup$ @AntonTrunov you might as well turn your comment into an answer. $\endgroup$ – cody Aug 25 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 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.