Commit ba58cfdf authored by Dennis Müller's avatar Dennis Müller


parent 01769b00
......@@ -10,6 +10,14 @@ We regret having to cut short some of the more thorough explanation. The proofs
We acknowledge the preliminary nature of our work and that (as mentioned by Reviewer #4) more views should be found in the described PVS/NASA library. However, explaining our results requires investigating and going into detail on the specific methodologies, practices and idiosyncracies of the PVS system in general and the NASA library development in particular. While we could certainly go into more detail, as Reviewer #3 mentions the paper is already somewhat terse without a certain amount of background knowledge regarding PVS, which is not the central topic. We consider analyzing and describing the results in more detail in an extended version.
Reviewer #4 asked about why we were looking for views *out of* our example theory of "beautiful sets" (instead of into). The reason being that in this use case we want to see whether the full theory (or instances thereof) already exists in some library. The section "Enabled Applications" in the Conclusion somewhat covers the directionality of the algorithm, including reuse of results as pointed our by the reviewer (see the application "Folklore-based Conjecturing").
Our use of "meta-theories" is actually intended to be morally equivalent to the common usage. We assume Reviewer #4s very understandable confusion stems from a lack of provided background on MMT itself. A meta-theory in MMT indeed lives on a different semantic level from a logical point of view - however, one core feature of the MMT system is that all theories are represented uniformly. In fact, LF too is not hard coded in MMT, but a theory in the same sense as e.g. the foundational theory for PVS or a theory within the PVS/NASA library. Hence the meta-theory relation becomes a relation between "object-level" (from the point of view of the MMT system) theories. We will consider adapting the Preliminaries-section accordingly.
The instatiation of theory parameters in our discussion of their contravariant elimination would indeed not be possible during the viewfinding process itself and would be part of the preprocessing of theories.
We mention using theorem proving in the beginning of Section 3, but decide to forego this option for the current paper for efficiency reasons. Searching for proofs would be prohibitively expensive for most applications described, where the results of viewfinding should be available while actively editing/writing theories. This is a conscious design choice regarding the trade-off between speed and accuracy.
[1] M. Iancu, M. Kohlhase, F. Rabe, J. Urban - "The Mizar Mathematical Library in OMDoc: Translation and Applications", Journal of Automated Reasoning 50/2, p.191-202
- The authors say: "we present the design and implementation of a generic view finder that works with arbitrary
corpora represented in MMT."
How costly is it to take a mathematical library and represent it in MMT? this will determine the applicability of the tool described here and needs to be addressed. Just knowing that the reference "M. Kohlhase, D. M¨uller, S. Owre, and F. Rabe. “Making PVS Accessible to Generic Services by Interpretation in a Universal Format”, 2017" *exists*, is not enough to assuage my fears that the tool is only applicable to very restricted contexts.
-> Rebuttal?
- Since we're talking about theory morphisms mostly, the kind of algorithm described here should be applicable (perhaps?) to mathematical libraries, such as Mathematical Structures ( or the database of mathematical sequences, where the kind of refactoring that could be achieved would be amazing. This depends of course on not needing the theorem prover capabilities of PVS or HOL or Twelf, but only on the represented mathematical knowledge being faithfully translated. I am afraid I am not able to know if this is true or not. Can you clarify?
-> Rebuttal?
- "view finder" is not a concept that most people will be familiar with, you should explain it at the beginning of the paper.
- they do not give the complete details of their algorithm often saying "we leave the details out."
-> Due to page limitations - rebuttal?
- They also claim their algorithm is efficient, but do not offer any type of analysis showing this fact.
-> check
- Finally, the paper contains several lemmata without proofs. This makes it difficult to check their results validity. I recommend the authors add proofs to the appendix or to an online report.
-> Proofs probably wouldn't be illuminating, but we could/should consider an online report anyway.
- the authors mention twice that details are being skipped---it's not so easy to grok.
-> See above
- When the key phrase 'view finder' is introduced it should have some explanatory annotation to avoid semantic dissonance as the tyro reader meets it for the first time. For example "With a view finder (something to helpfind logical views) ..." or something better.
- Popular proof assistants such is Isabelle/HOL, Coq and Mizar have large amounts of theory knowledge tied up in various ways in their type systems. The paper does not discuss how this knowledge could be accessed. Has this been considered and what are the challenges?
-> Don't know much about Isabelle/Coq/Mizar -- @Florian?
- The weakest part of the presentation is the explanation of
the experimental results in Section 4.2. More space and effort on
this would help the reader appreciate what has been achieved and what
needs to be tackled next.
-> Rebuttal?
- (Here and elsewhere). The emphasis on finding morphism targets given a fixed source theory is odd. A primary use case is having have theory under development and wanting to know if there are related existing theories whose results can be drawn on. The running example of "Beautiful Sets" is an example of this. With such a use case one cares more to ask about morphism sources for a given target. Once such a source is found, one can transfer over theorems from the source theory to the target theory. It seems this emphasis turns out to be reasonable only because of the simple restriction on morphisms and the existence then of an inverse morphism when the morphism is 1-1. Please discuss this issue.
-> Check
- Up front, this section needs to make clear that the "constants" of a theory include types, constants, functions and proof witnesses as in Automath or constructive type theories, and that in declarations "c : E", the types E can be not only types, but also type classses and propositions (by a propositions as types correspondence). A concrete simple example of of a theory would help ensure the reader appreciates this.
-> Check
......@@ -51,9 +22,6 @@ needs to be tackled next.
- Explicitly define what it means for a view to be total.
- The use of the term "meta-theory" is confusing and differs from its common usage. It seems that what are called "meta-theories" here could better be called "base theories"; they are theories on the same semantic level as the main theories being considered that get included into every one of these main theories. Then reserve the term "meta-theory" for this LF like theory in which the MMT system encodes all object theories.
-> Confused? Rebuttal?
- A few more words on the "module system" would help, given that expanding out theory imports and instantiations is a key part of the normalisation pre-processing step.
-> Check
......@@ -87,9 +55,6 @@ needs to be tackled next.
- Sec 4: The discussion of meta-views is very condensed. Could an example be given which illustrates how they have to be approximated?
-> Check
- The contravariant elimination proposal needs further qualification. As is, with the described simple view inference, no parameter instantiation is possible. And when parameter instantiation is coded, it has to happen uniformly for all theory constants.
-> Rebuttal? (Preprocessing)
- Fig 5. The ability to discover commutative operators seems very poor. Can this be discussed?
-> Check
......@@ -106,9 +71,6 @@ needs to be tackled next.
- Here and elsewhere the paper has good discussion of possible applications of morphism discovery. But the evidence that the implemented system generates falls far short of what these applications need. More honesty is needed about the preliminary nature of the work and the challenges ahead.
-> Rebuttal?
- This reviewer's guess is that further work has to move beyond syntactic matching for axioms/theorems and has to bring in automatic theorem proving of some kind. It was suprising that this avenue forward is quickly dismissed as intractable at the start of Section 3 and not picked up on again in the further work discussion in the Conclusions.
-> Inefficient. Rebuttal?
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment