Finite runs on a transition system
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
asked Nov 22 at 11:37
Javier
645723
add a comment |
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
asked Nov 22 at 11:37
Javier
645723
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some states, then the universal quantifier in the second case is trivially satisfied.
– Manuel Eberl
Nov 22 at 12:04
add a comment |
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
asked Nov 22 at 11:37
Javier
645723
I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:
inductive finite_runs for R where
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.
isabelle
isabelle
asked Nov 22 at 11:37
Javier
645723
asked Nov 22 at 11:37
Javier
645723
edited Nov 23 at 10:50
asked Nov 22 at 11:37
Javier
645723
asked Nov 22 at 11:37
Javier
645723
asked Nov 22 at 11:37
Javier
645723
645723
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some states, then the universal quantifier in the second case is trivially satisfied.
– Manuel Eberl
Nov 22 at 12:04
add a comment |
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some states, then the universal quantifier in the second case is trivially satisfied.
– Manuel Eberl
Nov 22 at 12:04
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some state
s, then the universal quantifier in the second case is trivially satisfied.– Manuel Eberl
Nov 22 at 12:04
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some state
s, then the universal quantifier in the second case is trivially satisfied.– Manuel Eberl
Nov 22 at 12:04
add a comment |
2 Answers
2
active
oldest
votes
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 at 12:05
Manuel Eberl
4,639520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 at 11:34
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 at 11:57
René Thiemann
93642
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
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
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53430148%2ffinite-runs-on-a-transition-system%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 at 12:05
Manuel Eberl
4,639520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 at 11:34
add a comment |
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 at 12:05
Manuel Eberl
4,639520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 at 11:34
add a comment |
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 at 12:05
Manuel Eberl
4,639520
There is Wellfounded.termip in the standard library. I think it should do exactly what you want.
It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.
answered Nov 22 at 12:05
Manuel Eberl
4,639520
answered Nov 22 at 12:05
Manuel Eberl
4,639520
answered Nov 22 at 12:05
Manuel Eberl
4,639520
answered Nov 22 at 12:05
Manuel Eberl
4,639520
4,639520
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 at 11:34
add a comment |
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.{(y,x) | (x,y) ∈ R}).
– Manuel Eberl
Nov 23 at 11:34
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
the r^-^- in where "termip r ≡ accp (r¯¯)" stands for the backward version of r^+^+ I guess?
– Javier
Nov 23 at 10:57
Without checking: No, I think it's simply the converse of the relation (i.e.
{(y,x) | (x,y) ∈ R}).– Manuel Eberl
Nov 23 at 11:34
Without checking: No, I think it's simply the converse of the relation (i.e.
{(y,x) | (x,y) ∈ R}).– Manuel Eberl
Nov 23 at 11:34
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 at 11:57
René Thiemann
93642
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 at 11:57
René Thiemann
93642
add a comment |
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 at 11:57
René Thiemann
93642
If you mean that finite runs means absence of infinite runs, then you can use the strong-normalization-on predicate SN_on of the AFP-entry Abstract-Rewriting. However your definition permits also runs like
a -> a -> a -> ...
which is not permitted by SN_on.
answered Nov 22 at 11:57
René Thiemann
93642
answered Nov 22 at 11:57
René Thiemann
93642
answered Nov 22 at 11:57
René Thiemann
93642
answered Nov 22 at 11:57
René Thiemann
93642
93642
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
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
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53430148%2ffinite-runs-on-a-transition-system%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
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
Required, but never shown
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
Required, but never shown
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
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
I think your first case is actually unnecessary since it is a special case of the second one. If there are no transitions from some state
s, then the universal quantifier in the second case is trivially satisfied.– Manuel Eberl
Nov 22 at 12:04