3 ms·
AFAIK languages like Idris, Agda, and Coq are not Turing-complete (specifically, they disallow general recursion) for just this reason.
by BalinKing 5y ago
AFAIK languages like Idris, Agda, and Coq are not Turing-complete (specifically, they disallow general recursion) for just this reason.
- raphlinus 5y agoIf my understanding is correct, Agda and Coq disallow general recursion, so all programs terminate by construction, but Idris relaxes this, in a desire to be more pragmatic at the cost of not as clean mathematically (functions have to be modeled as partial in general, to account for the fact they might not terminate).
- earleybird 5y agoGeneral recursion, yes however often the fixed point operator is added (and its associated judgements) to have interesting programs/proofs. Hmm, that fixed point operator, rings a bell, can't quite put my finger on it . . . :-)