About the relationship between non-termination and inconsistency?
Clash Royale CLAN TAG#URR8PPP
up vote
5
down vote
favorite
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?
formal-languages functional-programming
asked Sep 27 at 16:22
Tiago Loriato Simões
284
add a comment |Â
up vote
5
down vote
favorite
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?
formal-languages functional-programming
asked Sep 27 at 16:22
Tiago Loriato Simões
284
2
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
Sep 27 at 16:50
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?
– Tiago Loriato Simões
Sep 27 at 17:31
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
Sep 27 at 17:41
add a comment |Â
up vote
5
down vote
favorite
up vote
5
down vote
favorite
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?
formal-languages functional-programming
asked Sep 27 at 16:22
Tiago Loriato Simões
284
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?
formal-languages functional-programming
formal-languages functional-programming
asked Sep 27 at 16:22
Tiago Loriato Simões
284
asked Sep 27 at 16:22
Tiago Loriato Simões
284
edited Sep 27 at 16:33
asked Sep 27 at 16:22
Tiago Loriato Simões
284
asked Sep 27 at 16:22
Tiago Loriato Simões
284
asked Sep 27 at 16:22
Tiago Loriato Simões
284
284
2
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
Sep 27 at 16:50
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?
– Tiago Loriato Simões
Sep 27 at 17:31
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
Sep 27 at 17:41
add a comment |Â
2
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
Sep 27 at 16:50
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?
– Tiago Loriato Simões
Sep 27 at 17:31
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
Sep 27 at 17:41
2
2
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
Sep 27 at 16:50
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
Sep 27 at 16:50
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?
– Tiago Loriato Simões
Sep 27 at 17:31
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?
– Tiago Loriato Simões
Sep 27 at 17:31
2
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
Sep 27 at 17:41
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
Sep 27 at 17:41
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
4
down vote
accepted
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 esf 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
$$
tto 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.
answered Sep 27 at 17:31
chi
10.7k1628
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?
– Tiago Loriato Simões
Sep 27 at 18:06
2
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
1
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.
– Mario Carneiro
Sep 27 at 22:18
1
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
1
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
 |Â
show 11 more comments
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
4
down vote
accepted
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 esf 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
$$
tto 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.
answered Sep 27 at 17:31
chi
10.7k1628
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?
– Tiago Loriato Simões
Sep 27 at 18:06
2
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
1
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.
– Mario Carneiro
Sep 27 at 22:18
1
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
1
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
 |Â
show 11 more comments
up vote
4
down vote
accepted
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 esf 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
$$
tto 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.
answered Sep 27 at 17:31
chi
10.7k1628
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?
– Tiago Loriato Simões
Sep 27 at 18:06
2
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
1
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.
– Mario Carneiro
Sep 27 at 22:18
1
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
1
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
 |Â
show 11 more comments
up vote
4
down vote
accepted
up vote
4
down vote
accepted
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 esf 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
$$
tto 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.
answered Sep 27 at 17:31
chi
10.7k1628
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 esf 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
$$
tto 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.
answered Sep 27 at 17:31
chi
10.7k1628
edited Sep 27 at 20:58
answered Sep 27 at 17:31
chi
10.7k1628
answered Sep 27 at 17:31
chi
10.7k1628
answered Sep 27 at 17:31
chi
10.7k1628
10.7k1628
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?
– Tiago Loriato Simões
Sep 27 at 18:06
2
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
1
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.
– Mario Carneiro
Sep 27 at 22:18
1
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
1
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
 |Â
show 11 more comments
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?
– Tiago Loriato Simões
Sep 27 at 18:06
2
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
1
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.
– Mario Carneiro
Sep 27 at 22:18
1
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
1
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
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?
– Tiago Loriato Simões
Sep 27 at 18:06
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?
– Tiago Loriato Simões
Sep 27 at 18:06
2
2
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
@TiagoLoriatoSimoes With a powerful calculus like Agda, without normalization it can be hard to prove consistency. The $tto 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.
– chi
Sep 27 at 18:20
1
1
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.
– Mario Carneiro
Sep 27 at 22:18
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.
– Mario Carneiro
Sep 27 at 22:18
1
1
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
@chi You have to be careful with that kind of $mathrmfix$: taking $n=mathrmfix mathrmnat 0 S$, with the appropriate computational rules on $mathrmfix$, 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.
– cody
Sep 28 at 14:39
1
1
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
@MarioCarneiro The point is, in Agda using a inductive naturals type $sf nat$, you can prove $forall x:sf nat. xneq S x$. This copes with the counterexample by cody: $x=sf fix nat 0 S : sf nat$
– chi
Sep 28 at 20:44
 |Â
show 11 more comments
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fcs.stackexchange.com%2fquestions%2f97836%2fabout-the-relationship-between-non-termination-and-inconsistency%23new-answer', 'question_page');
);
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
2
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
Sep 27 at 16:50
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?
– Tiago Loriato Simões
Sep 27 at 17:31
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
Sep 27 at 17:41