Partial function in Coq / underdefined?
I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages used in that text.
For context I have finished writing the compiler, and am now in the verification stage, however I had to make a significant difference to Concrete Semantics in the definition of machine instruction execution. This difference seemed necessary in Agda, but now is making the verification stage incredibly complex.
In trying to do the simpler version of instruction execution given in Concrete Semantics, I've come across this line, which may explain why I am having trouble directly translating this into Agda:
Also useful are the head of a list, its first element, and the tail, the rest of the list:
fun hd :: 'a list ⇒ 'a
hd (x # xs) = x
Note that since HOL is a logic of total functions,
hdis defined, but we do not know what the result is. That is,hdis not undefined but underdefined.
What is does it mean for hd to be underdefined? Is this the equivalent of having an incomplete pattern in Agda?
The assembly instruction execution function relies heavily on hd. In my implementation of it in Agda I gave indices to multiple types to allow me to build proofs that the stack always has the minimum number of elements, in order to avoid the incomplete pattern matching problem. Now that I am trying to verify the compiler the proofs are magnitudes more complex than the proofs in Concrete Semantics, since I have to work with these indices.
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
compiler-construction isabelle agda
edited Nov 22 at 18:25
Bruno
134
asked Nov 22 at 16:22
Jacob Ward
394
add a comment |
I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages used in that text.
For context I have finished writing the compiler, and am now in the verification stage, however I had to make a significant difference to Concrete Semantics in the definition of machine instruction execution. This difference seemed necessary in Agda, but now is making the verification stage incredibly complex.
In trying to do the simpler version of instruction execution given in Concrete Semantics, I've come across this line, which may explain why I am having trouble directly translating this into Agda:
Also useful are the head of a list, its first element, and the tail, the rest of the list:
fun hd :: 'a list ⇒ 'a
hd (x # xs) = x
Note that since HOL is a logic of total functions,
hdis defined, but we do not know what the result is. That is,hdis not undefined but underdefined.
What is does it mean for hd to be underdefined? Is this the equivalent of having an incomplete pattern in Agda?
The assembly instruction execution function relies heavily on hd. In my implementation of it in Agda I gave indices to multiple types to allow me to build proofs that the stack always has the minimum number of elements, in order to avoid the incomplete pattern matching problem. Now that I am trying to verify the compiler the proofs are magnitudes more complex than the proofs in Concrete Semantics, since I have to work with these indices.
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
compiler-construction isabelle agda
edited Nov 22 at 18:25
Bruno
134
asked Nov 22 at 16:22
Jacob Ward
394
2
This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/…
– Li-yao Xia
Nov 22 at 17:09
add a comment |
I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages used in that text.
For context I have finished writing the compiler, and am now in the verification stage, however I had to make a significant difference to Concrete Semantics in the definition of machine instruction execution. This difference seemed necessary in Agda, but now is making the verification stage incredibly complex.
In trying to do the simpler version of instruction execution given in Concrete Semantics, I've come across this line, which may explain why I am having trouble directly translating this into Agda:
Also useful are the head of a list, its first element, and the tail, the rest of the list:
fun hd :: 'a list ⇒ 'a
hd (x # xs) = x
Note that since HOL is a logic of total functions,
hdis defined, but we do not know what the result is. That is,hdis not undefined but underdefined.
What is does it mean for hd to be underdefined? Is this the equivalent of having an incomplete pattern in Agda?
The assembly instruction execution function relies heavily on hd. In my implementation of it in Agda I gave indices to multiple types to allow me to build proofs that the stack always has the minimum number of elements, in order to avoid the incomplete pattern matching problem. Now that I am trying to verify the compiler the proofs are magnitudes more complex than the proofs in Concrete Semantics, since I have to work with these indices.
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
compiler-construction isabelle agda
edited Nov 22 at 18:25
Bruno
134
asked Nov 22 at 16:22
Jacob Ward
394
I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages used in that text.
For context I have finished writing the compiler, and am now in the verification stage, however I had to make a significant difference to Concrete Semantics in the definition of machine instruction execution. This difference seemed necessary in Agda, but now is making the verification stage incredibly complex.
In trying to do the simpler version of instruction execution given in Concrete Semantics, I've come across this line, which may explain why I am having trouble directly translating this into Agda:
Also useful are the head of a list, its first element, and the tail, the rest of the list:
fun hd :: 'a list ⇒ 'a
hd (x # xs) = x
Note that since HOL is a logic of total functions,
hdis defined, but we do not know what the result is. That is,hdis not undefined but underdefined.
What is does it mean for hd to be underdefined? Is this the equivalent of having an incomplete pattern in Agda?
The assembly instruction execution function relies heavily on hd. In my implementation of it in Agda I gave indices to multiple types to allow me to build proofs that the stack always has the minimum number of elements, in order to avoid the incomplete pattern matching problem. Now that I am trying to verify the compiler the proofs are magnitudes more complex than the proofs in Concrete Semantics, since I have to work with these indices.
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
compiler-construction isabelle agda
compiler-construction isabelle agda
edited Nov 22 at 18:25
Bruno
134
asked Nov 22 at 16:22
Jacob Ward
394
edited Nov 22 at 18:25
Bruno
134
asked Nov 22 at 16:22
Jacob Ward
394
edited Nov 22 at 18:25
Bruno
134
edited Nov 22 at 18:25
Bruno
134
edited Nov 22 at 18:25
Bruno
134
134
asked Nov 22 at 16:22
Jacob Ward
394
asked Nov 22 at 16:22
Jacob Ward
394
asked Nov 22 at 16:22
Jacob Ward
394
394
2
This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/…
– Li-yao Xia
Nov 22 at 17:09
add a comment |
2
This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/…
– Li-yao Xia
Nov 22 at 17:09
2
2
This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/…
– Li-yao Xia
Nov 22 at 17:09
This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/…
– Li-yao Xia
Nov 22 at 17:09
add a comment |
1 Answer
1
active
oldest
votes
hd in Isabelle/HOL is defined; it has a value, but you don't know anything about that value. It is possible to prove that hd = hd because x = x holds for all x, but you'll be unable to prove anything else (non-trivial) on hd .
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
They are not incomplete. Proofs that rely on behaviour of hd will most likely assume that the list on which hd is called is non-empty, or prove that it is non-empty based on other assumptions.
answered Nov 24 at 11:53
larsrh
2,014321
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%2f53434947%2fpartial-function-in-coq-underdefined%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
hd in Isabelle/HOL is defined; it has a value, but you don't know anything about that value. It is possible to prove that hd = hd because x = x holds for all x, but you'll be unable to prove anything else (non-trivial) on hd .
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
They are not incomplete. Proofs that rely on behaviour of hd will most likely assume that the list on which hd is called is non-empty, or prove that it is non-empty based on other assumptions.
answered Nov 24 at 11:53
larsrh
2,014321
add a comment |
hd in Isabelle/HOL is defined; it has a value, but you don't know anything about that value. It is possible to prove that hd = hd because x = x holds for all x, but you'll be unable to prove anything else (non-trivial) on hd .
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
They are not incomplete. Proofs that rely on behaviour of hd will most likely assume that the list on which hd is called is non-empty, or prove that it is non-empty based on other assumptions.
answered Nov 24 at 11:53
larsrh
2,014321
add a comment |
hd in Isabelle/HOL is defined; it has a value, but you don't know anything about that value. It is possible to prove that hd = hd because x = x holds for all x, but you'll be unable to prove anything else (non-trivial) on hd .
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
They are not incomplete. Proofs that rely on behaviour of hd will most likely assume that the list on which hd is called is non-empty, or prove that it is non-empty based on other assumptions.
answered Nov 24 at 11:53
larsrh
2,014321
hd in Isabelle/HOL is defined; it has a value, but you don't know anything about that value. It is possible to prove that hd = hd because x = x holds for all x, but you'll be unable to prove anything else (non-trivial) on hd .
Am I missing something or are the proofs in Concrete Semantics incomplete with hd not being defined?
They are not incomplete. Proofs that rely on behaviour of hd will most likely assume that the list on which hd is called is non-empty, or prove that it is non-empty based on other assumptions.
answered Nov 24 at 11:53
larsrh
2,014321
answered Nov 24 at 11:53
larsrh
2,014321
answered Nov 24 at 11:53
larsrh
2,014321
answered Nov 24 at 11:53
larsrh
2,014321
2,014321
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%2f53434947%2fpartial-function-in-coq-underdefined%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
2
This blogpost might be useful to understand undefinedness in Isabelle joachim-breitner.de/blog/…
– Li-yao Xia
Nov 22 at 17:09