++++++++++++++++++ FME2001: - Review reports for paper 30 +++++++++++++++++++++ - Dear author(s) : this file was extracted automatically from a very large - mailbox. In case you find any problem concerning mail encodings (or any - other kind of anomaly disturbing your understanding of the reviews) please - email any of the PC cochairs (pamela@research.att.com,jno@di.uminho.pt). ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ PAPER NUMBER: 30 CATEGORY: 2 TITLE: Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics AUTHOR(S): Mícheál Mac an Airchinnigh -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): The paper presents a bridge from classical model-theoretic formal methods to topos-theoretic formal methods. From Heyting algebras, cartesian closed category and topos (that provides an intrinsic logic) the case study of the spelling checker dictionary model is developed. Moreover, it explores the fibring of a classic VDM map. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2-3 Please comment your rating: The potential interest is in fact major but the way of presentation and the case studies do not emphasize enough this interest. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3 -4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 4 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: the work reported is new and significant and it could be not clear from the style of the presentation. It will be a new specific way for the development of model-theoretic specification languages. The move from classical formal methods to intuitionistic or topos based formal methods is important for the future. 6. How WORTHWILE is the goal of the authors? Comment: The goal must be better defined and emphasized from the initial philosophical point of view. Anyway even if it would be reduced to the use of a topos and intuitionistic structures for formal methods then it would be enough important. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The new principles are well introduced and explained but their impact with respect to classical models have to be better analyzed. Are they more connected to improvements about notation, or about unification of concepts or about proof developments ? The expected impacts have to be clarified. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The technical parts are simple and sound. They are mainly parts of the development of case studies 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: the work is more conceptual than theoretical and the implications in terms of applicability need more details (for instance from section 4). The arguments about this new approach of formal methods could be more satisfactory for instance with the presentation of a case study that is difficult to develop in the classical way and very easy and natural in the proposed approach. Here, the fact that one has a more natural framework with good properties is an argument to develop in a better way. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The quality of the presentation is good. But there is a strange gap between the first part (to section 3) and the second one (from section 4) that starts with a new case study without presentation of the motivations. In fact the relationships between both parts and the use of fibre bundles need more explanations wrt the natural character of the framework. The section 4 including the use of fibred spaces have to be better presented (more dedicated to a computer scientist reader) and needs more developments in order to convince the reader of its effective interest. A conclusion including perspectives has to be inserted between the related work section and the acknowledgements 11. Were there any formatting or mechanical problems with this paper?: Are the figures and length acceptable?: Are the references correct?: No problem about that. 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 30 CATEGORY: 2 TITLE: Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics AUTHOR(S): Mícheál Mac an Airchinnigh -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): Heyting algebras are embraced as an acceptable foundation for the Irish school of VDM. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 2 Please comment your rating: I don't think that the majority of the symposium is interested in a change of (or adaptation of?) formal foundation without a clear indication how this would make the method more powerful. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 3 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating oof your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: Nothing very new, in my experience researchers with a fundamental algebraic approach tend to discover "new" abstract frameworks in which they can re-express their previous results (and sometimes a little more) on a very regular basis. However, it may be felt to be significant that VDM-IRL has found such a framework. 6. How WORTHWILE is the goal of the authors? Comment: Worthwhile in the context of unifying theories; yet another exploration of how all these frameworks allow similar things at a practical level doesn't seem as worthwhile to me. 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: Quite well. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: As far as I can see, they are. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: This is the weak point of the paper - it concentrates on re-expressing what was previously possible, with occasional hints (many-valued logic, generalised quantifiers) at what could be extra. 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The author's delight in discovering and presenting the various links is evident, and this makes for a pleasurable read. Very well written, all I could spot was:- an f which should be italic on p17 l-8 - unusual (non)capitalisation of OO and Corba in the last reference. 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++ PAPER NUMBER: 30 CATEGORY: 2 TITLE: Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics AUTHOR(S): Mícheál Mac an Airchinnigh -------------------------------------------------------------------------------- 1. Briefly SUMMARIZE the paper (2-3 lines): This paper describes a re-interpretation of classical model-oriented (set-theoretic) semantics, "a la VDM", in terms of logic-free and membership-free semantic devices such as Heyting algebras, cc-categories and topoi. This is regarded as a theoretical foundation for the Irish School of Constructive Mathematics. 2. RELEVANCE: Please provide a rating of the paper's relevance to the FME Symposium, using the scale: 0 = Out of scope 1 = Marginal interest 2 = Minority interest 3 = Majority interest 4 = Outstanding interest Numeric Rating: 3 Please comment your rating: Traditional "naive" set-theory is insufficient as a foundation for model-oriented specification semantics. The prospect of alternative foundations is therefore a relevant area of research. 3. OVERALL RECOMMENDATION: Please provide a rating of the paper's acceptability, using the scale: 1 = Strong reject 2 = Weak reject 3 = Could go either way 4 = Weak accept 5 = Strong accept Numeric Rating: 4 NB: There should be a correlation between the two rates above. 4. CONFIDENCE LEVEL: Please provide a rating of your expertise in the area addressed by the paper, using the scale: 1 = Know virtually nothing about this area 2 = Not too knowledgeable, but I know a bit 3 = Know a moderate amount, about average I'd say 4 = Not my main area of work, but I know a lot about it 5 = My area of work, I know it extremely well Numeric Rating: 3 NB: PC members are responsible for ensuring that 1 is not used here. 5. ORIGINALITY. What is NEW and SIGNIFICANT in the work reported here? Comment: The use of Heyting algebras as a reasoning device dealing without naive set-theoretical membership. Heyting algebras have been known for a long time but little used as a basis for calculations. The link to a suitable categorial underpinning is also interesting. For instance, people who avoid categories (many of them actually hate categories!) could accept the Heyting algebra style as a kind of "in the middle" approach... 6. How WORTHWHILE is the goal of the authors? Comment: It is worthwhile, see 2. above 7. How well is this goal EXPLAINED and JUSTIFIED? Comment: The paper is careful in explaining the purpose of things, perhaps in a too bold style here and there. The examples provided could more elaborate in order to better "justify" the approach. 8. TECHNICAL QUALITY. Are the technical parts (definitions, statements, specifications, proofs, algorithms, etc.) SOUND? Comment: The paper deals with simple technical notions and the calculations presented are sound and easy to follow. Anyway, I somewhat failed to understand the overall relevance of the "ordered atom" structural implementation of section 3.1. 9. APPLICABILITY. If the work is primarily theoretical or conceptual, are the implications in terms of applicability adequately justified? If the paper is about a new formal technique, are satisfactory arguments presented in favor of the new technique? If a methodology is proposed, is it sound? If experimental results are presented, is their relevance justified? Comment: One of the motivations for running away from the traditional "naive" set-theoretical semantics of model-oriented specification is the complexity of the proofs and calculations involved in real-life specification and refinement problems. There is clearly a need for a compact calculation style similar to eg. the Bird-Meertens point-free style in functional programming. The proposed reasoning-style seems to have some potential in this respect but the examples provided are too simple for me to evaluate the approach in terms of "applicability". 10. PRESENTATION: Describe the QUALITY of the writing, including suggestions for changes where appropriate. Comment: The paper is very well written and carefully typeset. Just the following suggestions for improvement: p.2, l.-27: "relationship been" -> "relationship between" p.9, l.+8: "((Mac Lane and Moerdijk 1992, 268))" -> "(Mac Lane and Moerdijk 1992, 268)" p.16, l.+1: "this secion" -> "this section" p.17, l.-8: "map f. Again" -> "map $f$. Again" 11. Were there any formatting or mechanical problems with this paper?: No Are the figures and length acceptable?: Yes Are the references correct?: Yes 12. OTHER COMMENTS you believe would be useful to the author(s), including pointers to missing relevant work: p.6, l.+3: the set H of "many truth values" is neither properly motivated (the "H" presumably standing for "Heyting") nor suitably related to equation (62) on p. 14. p.9, l.-13: \emptyset is recovered from {a} \cap {b} only if ~(a=b) p.15, section 4: An attempt to generalize "hash tables" in a way similar to what is suggested in this section is given in a paper entitled "Fractal Types: an Attempt to Generalize Hash Table Calculation", presented in "Workshop on Generic Programming (WGP'98)", Marstrand, Sweden, June, 1998 and available from http://www.cs.ruu.nl/people/johanj/wgp98.html. p.18, section 5.1: The following report (which is about to, if not already become a paper) @techreport{HM96, author = "P. Hoogendijk and O. de Moor", title = "What is a data type?", number = "96/16", institution = "Eindhoven University of Technology and Oxford PRG", month = "August", year = "1996" } should be mentioned as work in the related area of "polytypic datatype membership". p.18, section 5.1: Being in favour of "functions and maps" being "primary", as the author writes in the "Epilogue", I find harder pieces of mathematics to tackle in such a re-definition of model-oriented semantics which the author does not mention. For instance, the fact that powersets (like in the DICT model) and finite mappings (A -m-> B) are *not* inductive datatypes (ie they are non-initial) and therefore their morphisms cannot be defined by a universal construction. This rules out a lot of calculation properties (reflection, fusion, absorption etc) which one would welcome in reasoning about these (so often used) data models... Does the Irish MC school provide an alternative in this respect? +++++++++++++++++++++ End of FME 2001 Paper Review Report ++++++++++++++++++++++