3
$\begingroup$

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

Improve this question
$\endgroup$
3
  • 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
    Commented Aug 25, 2019 at 17:50
  • 1
    $\begingroup$ @AntonTrunov you might as well turn your comment into an answer. $\endgroup$
    – cody
    Commented Aug 25, 2019 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
    Commented Sep 7, 2019 at 8:18

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.