5
$\begingroup$

I've been trying to get into Agda and I noticed that it doesn't have recursion, which implies that it isn't Turing-Complete.

From what I could understand, if Agda had recursion, it would make itself an inconsistency from a type theory perspective.

Something stuck to my mind: Is it possible to exist a language that it isn't strongly normalizing but, yet, consistent? Or does the existence of recursion mandatorily implies inconsistency?

$\endgroup$
  • 2
    $\begingroup$ Forcibly add a reduction rule $t \to t$, and normalization is lost, but all the logical properties are preserved :) $\endgroup$ – chi Sep 27 '18 at 16:50
  • $\begingroup$ Thank you for the answer, chi. However, I'm having a hard time wrapping my head around it, would it be possible for you to expand your answer a little? $\endgroup$ – Tiago Loriato Simões Sep 27 '18 at 17:31
  • 2
    $\begingroup$ Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases. $\endgroup$ – chi Sep 27 '18 at 17:41
4
$\begingroup$

Some trivial type systems

Let the set of types be $\bot,\top$ and the sets of terms be $a,b$, with typing rules

$$ \vdash a:\top \qquad \vdash b:\top $$ and computational rules $$ a \to b \qquad b \to a $$

Then, the resulting system has no (weakly/strongly) normalizing terms, yet it is consistent since no term inhabits $\bot$.

We can also allow recursion on $\top$, if we want.

$$ \dfrac{ \Gamma, x:\top \vdash e:\top }{ \Gamma \vdash {\sf rec}\ x. e\ :\top } $$ with the obvious computational rule $$ {\sf rec}\ x. e \to e\{{\sf rec}\ x. e/x\} $$

On adding full recursion

Of course, we can't allow unrestricted recursion on $\bot$, otherwise ${\sf rec}\ x.x:\bot$ leads to an inconsistency.

Adapting more serious type systems

If we take any strongly normalizing typed lambda calculus, we can modify the computational rules to add a silly reduction step $$ t\to t $$ for any term $t$.

The new calculus has as inhabited types the same inhabited types, so it preserves consistency. The calculus is not even weakly normalizing, though.

$\endgroup$
  • $\begingroup$ That was extremely useful! Since there are so many simple ways of adding non-normalized terms without leading to an inconsistency, why is it such a big deal for Agda? Is there an explanation for the cause of this problem? $\endgroup$ – Tiago Loriato Simões Sep 27 '18 at 18:06
  • 2
    $\begingroup$ @TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $t\to t$ rule above is simple to handle, but adding a constrained form of non-always-terminating recursion can be vastly more complex. Also, it is nice to know that when you prove in Agda that there is some natural satisfying some property, you get for free a terminating program which produces said natural. That's one of the main features of constructivism, and people don't want to break that. $\endgroup$ – chi Sep 27 '18 at 18:20
  • 1
    $\begingroup$ I think your trivial type system might be too trivial. In particular, usually recursion principles allow an arbitrary target type, and you have suggested here that avoiding recursion into bottom solves the problem, but this only works because there are only two types and we know which ones are supposed to be inhabited. In any reasonable type system with empty types, it is not decidable to determine if a type is empty, so this doesn't work. $\endgroup$ – Mario Carneiro Sep 27 '18 at 22:18
  • 1
    $\begingroup$ @chi You have to be careful with that kind of $\mathrm{fix}$: taking $n=\mathrm{fix}\ \mathrm{nat}\ 0\ S$, with the appropriate computational rules on $\mathrm{fix}$, you should be able to prove $n=S\ n$, which implies a contradiction! It isn't enough to restrict fixed points to inhabited types: they must also have a consistent semantics. In Agda, natural numbers are definite, i.e. they must have a precisely defined value in terms of the constructors. $\endgroup$ – cody Sep 28 '18 at 14:39
  • 1
    $\begingroup$ @MarioCarneiro The point is, in Agda using a inductive naturals type $\sf nat$, you can prove $\forall x:{\sf nat}.\ x\neq S x$. This copes with the counterexample by cody: $x={\sf fix\ nat\ 0}\ S : {\sf nat}$ $\endgroup$ – chi Sep 28 '18 at 20:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.