Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 6/2020

30-11-2019

Exploring the Structure of an Algebra Text with Locales

Author: Clemens Ballarin

Published in: Journal of Automated Reasoning | Issue 6/2020

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Locales, the module system of the theorem prover Isabelle, were designed so that developments in abstract algebra could be represented faithfully and concisely. Whether these goals were met is assessed through a case study. Parts of an algebra textbook, Jacobson’s Basic Algebra, that are challenging structurally were formalised. Key parts of the formalisation are presented in greater detail. An analysis of the work from both qualitative and quantitative perspectives substantiates that the design goals were met. In particular, the size ratio of formal to “pen and paper” text does not increase when going further into the book. The analysis also yields guidance on locales including patterns of use, which are identified and described.
previous article Efficient Strategies for CEGAR-Based Model Checking
next article A Library for Formalization of Linear Error-Correcting Codes

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
Counted were the entries containing locale declarations—more precisely, where at least one theory file contained a line matching the regular expression https://static-content.springer.com/image/art%3A10.1007%2Fs10817-019-09537-9/MediaObjects/10817_2019_9537_Figa_HTML.gif .
 
2
Readers wishing to reproduce the examples in Isabelle should use bold, not regular, “1” (input token https://static-content.springer.com/image/art%3A10.1007%2Fs10817-019-09537-9/MediaObjects/10817_2019_9537_Fige_HTML.gif ).
 
3
In locale expressions outside locale declarations, the for clause retains its usual semantics as a binder.
 
4
Jacobson requires S to be non-vacuous, but this was not required in the formalisation.
 
5
Isabelle requires escaping the single quote character in syntax declarations; “ https://static-content.springer.com/image/art%3A10.1007%2Fs10817-019-09537-9/MediaObjects/10817_2019_9537_Figch_HTML.gif ” yields “ https://static-content.springer.com/image/art%3A10.1007%2Fs10817-019-09537-9/MediaObjects/10817_2019_9537_Figci_HTML.gif ”.
 
6
\(K_R(G)\) denotes the group of right translations \(k_R : G \rightarrow G\) for \(k \in K\). Jacobson leaves right translations as an exercise, which had to be formalised as well. For the corresponding work on left translations, see Sect. 3.5 above.
 
7
In reproducing Gunter’s definition I have changed \((G, {\textit{prod}} \ )\) to \(\mathcal {G}\). Her original definition \( inv \, (G, {\textit{prod}} \ ) \, x \equiv \varepsilon y. \, y \in G \wedge ({\textit{prod}} \ \, y \, x = id \, (G, {\textit{prod}} \ ))\) does not involve the projections \({ fst } \ \) and \({\textit{snd}} \ \), but many others of her definitions do. Further, since defined operations are well-defined on the carrier set definite choice is sufficient for making definitions. There is no need for the axiom of choice.
 
9
Wiedijk [26] supposes that the mathematical text is available in computer-readable form and suggests the factor be computed by comparing sizes of compressed files of the formalisation and its mathematical source. I have chosen to simply compare numbers of lines as is common practice when measuring code size in computer science.
 
10
This paragraph reproduces my response to a post in the Isabelle Users mailing list: https://​lists.​cam.​ac.​uk/​pipermail/​cl-isabelle-users/​2019-September/​msg00074.​html.
 
Literature
1.
Aransay, J., Ballarin, C., Rubio, J.: A mechanized proof of the basic perturbation lemma. J. Autom. Reason. 40(4), 271–292 (2008)MathSciNetCrossRef
2.
Bailey, A.: The Machine-Checked Literate Formalisation of Algebra in Type Theory. Ph.D. Thesis, University of Manchester (1998)
3.
Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) Types for Proofs and Programs, TYPES 2003, Torino, Italy, LNCS 3085, pp. 34–50. Springer, Berlin (2004)
4.
Ballarin, C.: Tutorial to locales and locale interpretation. In: Lambán, L., Romero, A., Rubio, J. (eds.) Contribuciones Científicas en honor de Mirian Andrés Gómez. Servicio de Publicaciones de la Universidad de La Rioja, Logroño, Spain, Also part of the Isabelle user documentation (2010)
5.
Ballarin, C.: Reading an algebra textbook. In: Lange C. et al. (eds.) CEUR Workshop Proceedings 1010. Intelligent Computer Mathematics, Bath (2013)
6.
7.
8.
9.
Chan, H.-L., Norrish, M.: Mechanisation of AKS algorithm: Part 1–the main theorem. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving, ITP 2015, Nanjing, China, LNCS 9236, pp. 117–136. Springer, Berlin (2015)
10.
Farmer, W.M.: Theory interpretation in simple type theory. In: Heering, J., Mainke, K., Möller, B., Nipkow, T. (eds.) Higher-Order Algebra, Logic, and Term Rewriting, HOA ’93, Amsterdam, The Netherlands, LNCS 816, pp. 96–123. Springer, Berlin (1994)CrossRef
11.
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39(1), 95–146 (1992)MathSciNetCrossRef
12.
Gunter, E.L.: Doing Algebra in Simple Type Theory. Technical Report MS-CIS-89-38, University of Pennsylvania (1989)
13.
Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for proofs and programs, TYPES 2006, Nottingham, UK, LNCS 4502, pp. 160–174. Springer, Berlin (2007)
14.
Haftmann, F., Wenzel, M., (2009) Local theory specifications in Isabelle, Isar. In: Berardi S., Damiani F., de’Liguoro U. (eds) Types for Proofs and Programs, TYPES, Torino, Italy, LNCS 5497, pp. 153–168. Springer, Berlin (2008)
15.
Harper, R., Pierce, B.C.: Design considerations for ML-style module systems. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2005)MATH
16.
Jacobson, N.: Basic Algebra, vol. I, 2nd edn. Freeman, Dallas (1985)MATH
17.
Kammüller, F.: Modular Reasoning in Isabelle. Ph.D. Thesis, University of Cambridge, Computer Laboratory, Also Technical Report No. 470 (1999)
18.
Kammüller, F., Wenzel, M., Paulson, L.C.: Locales: a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics: TPHOLs’99, Nice, France, LNCS 1690, pp. 149–165. Springer, Berlin (1999)CrossRef
19.
Mahboubi, A., Tassi, E.: Canonical structures for the working Coq user. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, ITP 2013, Rennes, France, LNCS 7998, pp. 19–34. Springer, Berlin (2013)
20.
Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Theorem Proving in Higher Order Logics, LNCS 1479. Springer, pp 349–366 (1998)
21.
Paulson, L.C.: Defining functions on equivalence classes. ACM Transactions on Computational Logic 7(4), 658–675 (2006)MathSciNetCrossRef
22.
Soubiran, E.: Modular Development of Theories and Name-Space Management for the Coq Proof Assistant. Ph.D. Thesis, École Polytechnique (2012)
23.
van Benthem Jutting, L.S.: Checking Landau’s “Grundlagen” in the Automath System. Ph.D Thesis, Technische Hogeschool Eindhoven (1977)
24.
25.
Wenzel, M.: Isabelle/Isar–a generic framework for human-readable proof documents. Stud. Log. Gramm. Rhetor. 10(23), 277–298 (2007). (Festschrift in Honour of Andrzej Trybulec)
26.
Metadata
Title
Exploring the Structure of an Algebra Text with Locales
Author
Clemens Ballarin
Publication date
30-11-2019
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 6/2020
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-019-09537-9

Premium Partner

    Image Credits