Mixing
About the relationship between non-termination and inconsistency?
Clash Royale CLAN TAG#URR8PPP
up vote
3
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 2 hours ago
Tiago Loriato Simões
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
add a comment |Â
up vote
3
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 2 hours ago
Tiago Loriato Simões
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
1
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
2 hours ago
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
1 hour ago
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
1 hour ago
add a comment |Â
up vote
3
down vote
favorite
up vote
3
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 2 hours ago
Tiago Loriato Simões
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
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 2 hours ago
Tiago Loriato Simões
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 hours ago
Tiago Loriato Simões
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
edited 2 hours ago
asked 2 hours ago
Tiago Loriato Simões
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
asked 2 hours ago
Tiago Loriato Simões
184
asked 2 hours ago
Tiago Loriato Simões
184
184
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
New contributor
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
Tiago Loriato Simões is a new contributor to this site. Take care in asking for clarification, commenting, and answering.
Check out our Code of Conduct.
1
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
2 hours ago
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
1 hour ago
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
1 hour ago
add a comment |Â
1
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
2 hours ago
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
1 hour ago
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
1 hour ago
1
1
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
2 hours ago
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
2 hours ago
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
1 hour ago
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
1 hour ago
2
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
1 hour ago
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
1 hour ago
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
3
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 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$.
You can also allow recursion on $top$, if you 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 1 hour ago
chi
10.6k1628
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
54 mins ago
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
41 mins ago
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
3
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 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$.
You can also allow recursion on $top$, if you 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 1 hour ago
chi
10.6k1628
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
54 mins ago
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
41 mins ago
add a comment |Â
up vote
3
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 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$.
You can also allow recursion on $top$, if you 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 1 hour ago
chi
10.6k1628
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
54 mins ago
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
41 mins ago
add a comment |Â
up vote
3
down vote
accepted
up vote
3
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 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$.
You can also allow recursion on $top$, if you 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 1 hour ago
chi
10.6k1628
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 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$.
You can also allow recursion on $top$, if you 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 1 hour ago
chi
10.6k1628
edited 50 mins ago
answered 1 hour ago
chi
10.6k1628
answered 1 hour ago
chi
10.6k1628
answered 1 hour ago
chi
10.6k1628
10.6k1628
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
54 mins ago
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
41 mins ago
add a comment |Â
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
54 mins ago
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
41 mins ago
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
54 mins ago
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
54 mins ago
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
41 mins ago
@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
41 mins ago
add a comment |Â
Tiago Loriato Simões is a new contributor. Be nice, and check out our Code of Conduct.
Tiago Loriato Simões is a new contributor. Be nice, and check out our Code of Conduct.
Tiago Loriato Simões is a new contributor. Be nice, and check out our Code of Conduct.
Tiago Loriato Simões is a new contributor. Be nice, and check out our Code of Conduct.
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
1
Forcibly add a reduction rule $t to t$, and normalization is lost, but all the logical properties are preserved :)
– chi
2 hours ago
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
1 hour ago
2
Done. I don't think my answer will be really satisfactory, but at least it points out a few trivial cases.
– chi
1 hour ago