From utebachmeier at gmail.com Thu Aug 18 22:26:10 2011 From: utebachmeier at gmail.com (Sabrina Friedman) Date: Thu, 18 Aug 2011 23:26:10 +0300 Subject: [Flirts] CafeOBJ modules V Haskell type classesfrom Sabrina Message-ID: Hi, Intorduction ============ I am a PhD student and my thesis is concerned with applying formal techniques for specifying geographical information systems (GIS). My background is in GIS and information systems. I do not have that much expertise in functional languages or formal methods. Nevertheless, my thesis requires a comparison between Haskell and CafeOBJ (Diaconescu and Futatsugi 1998; Diaconescu, Futatsugi et al. 2003; Diaconescu 2008). The Haskell language is very popular among geo-scientist for specification and prototyping (Frank and Kuhn 1995), (Frank 1997). In the geo-domain Haskell has be used in several distinct ways: interface specification language Frank and Kuhn (Frank and Kuhn 1998), an ontology language(Kuhn 2004), a pure specification language (Frank, Nittel et al. 2000), and a specification and prototyping language (Medak 1999). I suspect that institution based languages(Goguen and Burstall 1992), such as CafeOBJ offer a much broader canvas than Haskell in the area of specification and prototyping though not for actual programming. CafeOBJ has a reasonable set logics and proof technologies (equational and a first order OTTER-like theorem prover), model checking (Maude like facilities), and a small object oriented language (FOOPS like). CafeOBJ is also a programming language hence it has some relation with the current practice of using Haskell in the geo-domain. I feel that CafeOBJ has a sufficient set of logics and sufficiently powerful module algebra to allow me to construct a three level geographic model: Layer 1 consists of an ontology level model that uses First Order Predicate Logic, based on SNAP and SPAN(Grenon and Smith 2004) Layer 2 consists of domain specific specification of geographic spatial-temporal objects such as road networks and land parcels. At this level I use behavioral logic (Diaconescu 2005)and equational logic (Goguen and Lin 2005). Layer 3 consists of prototype using Rewriting Logic (Meseguer 2003),(Lechner 1997),(Lyabakh 2001) and equational logic again. For my thesis I wish to compare Haskell and CafeOBJ. Much of this comparison seems to revolve around 3 points: 1)The higher abstraction and expresive range available in CafeOBJ equations. For example, a conditional equation for injective property is executable using the apply command, ceq [inj] : b = b' if g b == g b' . 2) the multiple logics explicitly in CafeOBJ 3) the modularization provided by CafeOBJ modules compared to Haskell's type classes Any general comparison between type classes and institution based languages would probably serve my purpose. In this posting wish to focus the discussion on point 3 and identify the advantages and dissadvantages of using institution base module systems over Haskell type classes for both specifying and prototyping (but not the actual programming of complex systems). My assumption is that CafeOBJ modules offer better structuring facilities than Haskell type classes in terms of encapsulation, a variety of import methods and multiple logics. Not being a specialist in the area I need some literature or domain expert to validate this assumption. Unfortunately, I have found few papers relating these Haskell type classes and modules. Some papers that come close to my required comparison are (Wehr 2005), (Schr?der and Mossakowski 2002), (Basin and Denker: 2000), (Shields and Jones 2002), (Kahl and Scheffczyk 2001), (Schroder, Mossakowski et al. 2005; Schroder 2006), (Kothar and Sulzmann 2005). My Current understanding ========================= Below is my understanding of the CafeOBJ Module System (CMS) and Haskell Type Classes (HTC). It may not be possible to focus on the modularity issue in isolation so I have included my understanding of some more general points of comparison between the two languages. 1. Both techniques were originally designed to address different issues, HTC for ad-hoc polymorphism and CMS system structuring. But there seems to be some overlap in there respective usages. HTC can be used for constructing specifications(Frank 1997) and CMS can be used for a form of higher order programming(Goguen 1990). Note Frank's paper favours higher order functions whereas Goguen's does not. HTC seems to be synonymous with higher order, but some institutions based languages such as Specware are higher order(DeCloss 2006). 2. HTC is based on Curry-Howard isomorphism between types, propositions and objects of a Cartesian closed category. A HTC is a proposition about a type. 3) CMS is based on the logic independent theory of institutions(Goguen and Burstall 1992). 4) Some work has been done on the unification of Curry-Howard isomorphism and institutions (Goguen, Mossakowski et al. 2007), (Rabe 2008). Is it too naive to say that a foundational level: Institutions are based on model theory and Haskell type classes are based on type theory? 5) Haskell type classes do not provide name spaces (Wehr 2005). Two different type classes cannot define two associated type synonyms or two methods with the same name (unless the two classes are defined in different Haskell modules). 6) Type classes and instances in Haskell 98 may contain only methods; extensions to Haskell 98 also allow type synonyms (e.g. type Name = String ) and data types (e.g. data Anniversary = Birthday Date | Wedding Date).(Wehr 2005). There exists no extension that allows nested type classes and instances (Wehr 2005). 5) My interpretation is that a loose module in CafeOBJ roughly corresponds to a Haskell class, while a tight module corresponds to a Haskell instance. CafeOBJ modules can be parameterized by other modules whereas Haskell class/instances are parameterized by types. CafeOBJ modules can also import other modules. This importation includes facilities to rename elements (sorts and functions). Importation also allows the user to construct logically valid mappings between elements in the imported module and the importing module. Haskell type classes do not import in this sense, their only structuring mechanisms are parameterization (by classes or type?) and inheritance of other classes. True importing in Haskell is handled by Haskell's own module system which operates above and independently of the type class system. The Haskell module can handle HTC. 6) The instances of HTC are not named in standard Haskell whereas all CafeOBJ modules and views are named. 7) HTC are conceptually predicates on types (Neubauer, Thiemann et al. 2002) 8) Frank and Kuhn (Frank and Kuhn 1998) assert that classes in Haskell describe (define?) classes of algebras and instances define particular models. This seems to be pretty close to what modules can achieve. 9) In Haskell class instances may be spread over several modules(Neubauer, Thiemann et al. 2002). Issues: Order of imports (no colimit). Where is the class declared? Are their conflicting instances?. 10) While it is possible to reason about a Haskell program the logic of Haskell is not always explicitly present. Some formal reasoning can be done but no formal semantic is written for Haskell. This makes it difficult to write formal tools for Haskell. This point may be more related to what is in a module than how modules may be combined. Question. ======== I now have a set of questions that should help me identify the relative strengths and weakness of HTC and CMS: Question 1: Is my rough understand of HTC and CMS reasonable? Obviously, I am not talking at a very detailed or formal level, but from the point of view of a user who wishes to construct specifications and understand the basics of strengts and limitations of each approach. Question 2: Notwithstanding my current understanding of Haskell set out above, is there any way of 'importing'(in the CafeOBJ sense) type classes into type classes or instances into instances. Question 3: Lutz Schroder (Schroder 2006) talks about type classes being a 'pre-institution' for polymorphism. My understanding of his paper is that type classes do not support 'model expansion', because expanded models may have more types. Is this due to the lack of an import facility in Haskell's type classes? Is this a serious drawback for real specification construction? Question 4: Haskell type classes can be used to express axioms about their operations (loose model or theoy). We can have many instances of a class(each a tight model). These can be combined in various ways with instances of other classes. But I am not sure if HTC has the ability to mix loose and initial models. Conclusion. ========== I hope that my questions are not to naive or off the mark. What I really need is a set of theoretically sound advantages and disadvantages of CHS and HTC. Intuitively I feel the CMS is superior to HTC for specification but I cannot prove or even intelligently articule this point. These advantages and disadvantage should be understood by average computer practitioner and geo-scientist who has little knowledge of formal methods but is willing to put in an effort to gain enough knowledge to grasp the main issues. Best regards, Pat Browne http://www.comp.dit.ie/pbrowne/ References DeCloss, D. P. (2006). An Analysis Of Specware And Its Usefulness In The Verification Of High Assurance Systems. Naval Postgraduate School Monterey, California. Diaconescu, R. (2005). "Behavioural Specification for Hierarchical Object Composition." Theoretical Computer Science 343(3): 305-331. Diaconescu, R. (2008). A Methodological Guide to the CafeOBJ Logic. Logics of Specification Languages. D. Bj?rner and M. Henson, Springer. Diaconescu, R. and K. Futatsugi (1998). CafeOBJ Report, World Scientific Publishing Co. Pte. Ltd. Diaconescu, R., K. Futatsugi, et al. (2003). "CafeOBJ: Logical Foundations and methodologies." Computing and Informatics 22(Numbers 3-4): 257-283. Frank, A. and W. Kuhn (1995). Specifying Open GIS with Functional Languages. In Advances in Spatial Databases (4th International Symposium, Ssd'95 in Portland, Me), Main, USA., Springer-Verlag, 1995. Frank, A. U. (1997). Higher order functions necessary for spatial theory development. Proceedings of Auto-Carto 13, Seattle, USA. Goguen, J. (1990). Higher-order functions considered unnecessary for higher-order programming. Research Topics in Functional Programming. D. Turner, Addison Wesley. Goguen, J. and R. Burstall (1992). "Institutions: abstract model theory for specification and programming." Journal of the ACM 39(1): 95-146. Goguen, J. and K. Lin (2005). Specifying, Programming and Verifying with Equational Logic. Articles in Honor of Dov Gabbay's 60th Birthday. Sergei N. Art?mov, Howard Barringer, Artur S. d'Avila Garcez, Lu?s C. Lamb and J. Woods, Kings College Press, 2005. Goguen, J., T. Mossakowski, et al. (2007). "An Institutional View on the Curry-Howard-Tait-Isomorphism." International Journal of Software Informatics 1(1): 129?152. Grenon, P. and B. Smith (2004). "SNAP and SPAN: Towards Dynamic Spatial Ontology." SPATIAL COGNITION AND COMPUTATION 4(1): 69-104. Kothar, S. and M. Sulzmann (2005). C++ templates/traits versus Haskell type classes. Singapore, Technical Report TRB2/05, The National University of Singapore, 2005. Lechner, U. (1997). Object-oriented specifications of distributed systems. Dept. of Mathematics and Information, Passau, Germany. 4. Lyabakh, N. (2001). Design and Rigorous Prototyping of Object-Oriented Modeling with Syntropy., Books on Demand GmbH, Germany. Meseguer, J. (2003). Executable Computational Logics: Combining Formal Methods and Programming Langauge Based System Design. MEMOCODE 2003. Neubauer, M., P. Thiemann, et al. (2002). "Functional logic overloading." ACM SIGPLAN Notices 37(1): 233-244. Rabe, F. (2008). Representing Logics and Logic Translations. Computer Science, Jacobs University Bremen, School of Engineering and Science. Bremen. Schroder, L. (2006). Higher Order and Reactive Algebraic Specification and Development, Department of Computer Science, University of Bremen. > Basin, D. A. and G. Denker: (2000). \"Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis.\" Electr. Notes Theor. Comput. Sci. 36: (2000) 36: (2000). > > Frank, A., S. Nittel, et al. (2000). Abstract Modeling with Functional Languages, OPENGIS PROJECT DOCUMENT 00-030. > > Frank, A. U. and W. Kuhn (1998). A Specification Language for Interoperable GIS. Interoperating Geographic Information Systems. M. E. Goodchild, M.J.; Fegeas, R.; Kottman, C., Kluwer Academic Publishers Norwell, MA, USA. > > Goguen, J., T. Mossakowski, et al. (2007). \"An Institutional View on Categorical Logic.\" Int J Software Informatics 1(1): 129-132. > > Goguen, J., T. Mossakowski, et al. (2007). \"An Institutional View on the Curry-Howard-Tait-Isomorphism.\" International Journal of Software Informatics 1(1): 129?152. > > Kahl, W. and J. Scheffczyk (2001). Named Instances for Haskell Type Classes. Proc. Haskell Workshop 2001, ENTCS vol. 59 no. 2. > > Kuhn, W. (2004). Why Information Science needs Cognitive Semantics. Proceedings of the Workshop on the Potential of Cognitive Semantics for Ontologies (part of FIOS 2004). > > Medak, D. (1999). Lifestyles - A Paradigm for the description of spatiotemporal databases. Faculty of Science and Technology. Vienna, Technical University Vienna. Ph.D. > > Neubauer, M., P. Thiemann, et al. (2002). \"Functional logic overloading.\" ACM SIGPLAN Notices 37(1): 233-244. > > Rabe, F. (2008). Representing Logics and Logic Translations. Computer Science, Jacobs University Bremen, School of Engineering and Science. Bremen. > > Schroder, L. (2006). Higher Order and Reactive Algebraic Specification and Development, Department of Computer Science, University of Bremen. > > Schroder, L. (2006). Higher Order and Reactive Algebraic Specification and Development. > > Schr?der, L. and T. Mossakowski (2002). HasCASL: Towards Integrated Specification and Development of Haskell Programs. 9th International Conference on Algebraic Methodology And Software Technology, AMAST 2002, St. Gilles les Bains, Reunion Island, France, Springer. > > Schroder, L., T. Mossakowski, et al. (2005). Type class polymorphism in an institutional framework. Recent Trends in Algebraic Development Techniques, Springer LNCS. 3423: 234-251. > > Shields, M. and S. P. Jones (2002). \"First-Class Modules for Haskell.\" > > Wehr, S. (2005). ML Modules and Haskell Type Classes: A Constructive Comparison. Institut fur Informatik. Freiburg, Germany., Universitat Freiburg. MSc. > > Sabrina Friedman Billige Fl?ge Marketing GmbH Emanuelstr. 3, 10317 Berlin Deutschland Telefon: +49 (33) 5310967 Email: utebachmeier at gmail.com Site: http://flug.airego.de - Billige Fl?ge vergleichen From Till.Mossakowski at dfki.de Fri Oct 7 11:34:16 2011 From: Till.Mossakowski at dfki.de (Till Mossakowski) Date: Fri, 07 Oct 2011 11:34:16 +0200 Subject: [Flirts] ISO standard for heterogeneous ontologies Message-ID: <4E8EC798.7000803@dfki.de> Dear Flirters, I am chairing an effort to design an ISO standard "Ontology integration and interoperability". The standard will comprise a "distributed ontology language" (DOL) that integrates different ontology languages. The semantics will be institution-based; heterogeneity is obtained via a Grothendieck institution. Attached a couple of slides and a working draft. Here are some more resources: Mailing list: ontoiop-wg at interop.cim3.net Archive at http://interop.cim3.net/forum/ontoiop-wg/ Community file repository: http://interop.cim3.net/file/work/OntoIOp/ (please tell me if you want to have access) Homepage: Official (OntoIOp to be added): http://bit.ly/ISO-TC37-SC3-OntoIOp Community (to be updated): http://ontolog.cim3.net/cgi-bin/wiki.pl?OntoIOp All the best, Till -- Prof. Dr. Till Mossakowski Cartesium, room 2.51 Phone +49-421-218-64226 DFKI GmbH Bremen Fax +49-421-218-9864226 Safe & Secure Cognitive Systems Till.Mossakowski at dfki.de Enrique-Schmidt-Str. 5, D-28359 Bremen http://www.dfki.de/sks/till Deutsches Forschungszentrum fuer Kuenstliche Intelligenz GmbH principal office, *not* the address for mail etc.!!!: Trippstadter Str. 122, D-67663 Kaiserslautern management board: Prof. Wolfgang Wahlster (chair), Dr. Walter Olthoff supervisory board: Prof. Hans A. Aukes (chair) Amtsgericht Kaiserslautern, HRB 2313 -------------- next part -------------- A non-text attachment was scrubbed... Name: 2011-10-06-meeting-slides.pdf Type: application/pdf Size: 86149 bytes Desc: not available URL: -------------- next part -------------- A non-text attachment was scrubbed... Name: WD_OntoIOp_current.pdf Type: application/pdf Size: 466359 bytes Desc: not available URL: