Email Gateway (Apr 12 2022 at 09:59): Email Gateway (Apr 12 2022 at 09:59):From: Fabian Huch <huch@in.tum.de>
To collect data on which concepts are important and which theorems are
central in AFP entries, I have sent around some e-mails with suggestions
and asking for feedback - the goal of this is to improve AFP navigation
and ease of understanding (on the web page), by generating such
suggestions for all entries.
If you've received such a mail, a reply would be greatly appreciated!
Feel free to ask any questions here.
Best,
Fabian
Email Gateway (Apr 12 2022 at 10:03):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
When you say "which theorems are central", do you mean "which are the main theorems", or do you mean,
"which theorems are in some sense a central part of the reasoning"? The suggestions you sent seem to
be mostly things that are heavily used, rather than those that are the main points.
Some roughly similar clarification on "which concepts are important" would also be helpful. I also
do not have a clear idea as to how the suggestions here might have been generated or what the overall
thrust of this is supposed to be.
Email Gateway (Apr 12 2022 at 10:08):From: Fabian Huch <huch@in.tum.de>
On 4/12/22 12:03, Eugene W. Stark wrote:
When you say "which theorems are central", do you mean "which are the
main theorems", or do you mean,
"which theorems are in some sense a central part of the reasoning"?
The suggestions you sent seem to
be mostly things that are heavily used, rather than those that are the
main points.
The question is meant as "which theorems are in some sense a central
part of the reasoning".
Some roughly similar clarification on "which concepts are important"
would also be helpful.
Whatever locales, constants, classes, types you consider most important
in the entry overall.
I also
do not have a clear idea as to how the suggestions here might have
been generated or what the overall
thrust of this is supposed to be.
Finding out how to best generate them is part of the research ;)
The suggestions come from analyzing metrics on the underlying theorem
dependency network.
Fabian
Email Gateway (Apr 12 2022 at 22:24):From: Gerwin Klein <kleing@unsw.edu.au>
On 12 Apr 2022, at 20:08, Fabian Huch <huch@in.tum.de> wrote:
On 4/12/22 12:03, Eugene W. Stark wrote:
When you say "which theorems are central", do you mean "which are the main theorems", or do you mean,
"which theorems are in some sense a central part of the reasoning"? The suggestions you sent seem to
be mostly things that are heavily used, rather than those that are the main points.The question is meant as "which theorems are in some sense a central part of the reasoning".
I'm confused about this, because that's not what I would usually be interested in when I look at an AFP entry (or any formalisation, really). I'd want to see the top-level theorems.
Central to reasoning will be helper lemmas, maybe strengthened statements for induction or intermediate constructions, but why would I care about that unless I want to repeat the development? If I want to use an entry or understand what it proves, I'd need the top-level statements, any axioms/assumptions, and the definitions used in the top-level statement.
This may be somewhat different if the entry is a library, but then there are also not 5 central lemmas, but likely dozens of lemmas that I can now use.
Some roughly similar clarification on "which concepts are important" would also be helpful.
Whatever locales, constants, classes, types you consider most important in the entry overall.
That one works for me.
I also
do not have a clear idea as to how the suggestions here might have been generated or what the overall
thrust of this is supposed to be.Finding out how to best generate them is part of the research ;)
The suggestions come from analyzing metrics on the underlying theorem dependency network.
There is also a hint many authors give, which is using "theorem" instead of "lemma" when they state something important. Of course, that's not used consistently, but if it can be extracted automatically, it might be helpful.
Cheers,
Gerwin
Email Gateway (Apr 13 2022 at 11:05):From: Fabian Huch <huch@in.tum.de>
On 4/13/22 00:24, Gerwin Klein wrote:
On 12 Apr 2022, at 20:08, Fabian Huch <huch@in.tum.de> wrote:
On 4/12/22 12:03, Eugene W. Stark wrote:
When you say "which theorems are central", do you mean "which are the main theorems", or do you mean,
"which theorems are in some sense a central part of the reasoning"? The suggestions you sent seem to
be mostly things that are heavily used, rather than those that are the main points.
The question is meant as "which theorems are in some sense a central part of the reasoning".
I'm confused about this, because that's not what I would usually be interested in when I look at an AFP entry (or any formalisation, really). I'd want to see the top-level theorems.Central to reasoning will be helper lemmas, maybe strengthened statements for induction or intermediate constructions, but why would I care about that unless I want to repeat the development? If I want to use an entry or understand what it proves, I'd need the top-level statements, any axioms/assumptions, and the definitions used in the top-level statement.
I agree that most central theorems are not helpful for an overview - but
they are important in understanding the dependency network. Only the
"Important concepts" aspects is something to show on top level.
There is also a hint many authors give, which is using "theorem" instead of "lemma" when they state something important. Of course, that's not used consistently, but if it can be extracted automatically, it might be helpful.
Yes, I agree.
Fabian
Last updated: Jul 15 2022 at 23:21 UTC