Skip to main content
SpringerLink
Log in
Book cover

International Conference on Intelligent Computer Mathematics

CICM 2018: Intelligent Computer Mathematics pp 76–86Cite as

Biform Theories: Project Description

  • Conference paper
  • First Online:

  • 586 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11006))

Abstract

A biform theory is a combination of an axiomatic theory and an algorithmic theory that supports the integration of reasoning and computation. These are ideal for specifying and reasoning about algorithms that manipulate mathematical expressions. However, formalizing biform theories is challenging as it requires the means to express statements about the interplay of what these algorithms do and what their actions mean mathematically. This paper describes a project to develop a methodology for expressing, manipulating, managing, and generating mathematical knowledge as a network of biform theories. It is a subproject of MathScheme, a long-term project at McMaster University to produce a framework for integrating formal deduction and symbolic computation.

This research is supported by NSERC.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Other computer algebra systems have similar commands.

  2. 2.

    Computer scientists would call this denotational semantics rather than mathematical meaning.

References

  1. Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, 2nd edn. Kluwer, Dordrecht (2002)

    Book  Google Scholar 

  2. Barwise, J., Seligman, J.: Information Flow: The Logic of Distributed Systems, Tracts in Computer Science, vol. 44. Cambridge University Press, Cambridge (1997)

    Book  Google Scholar 

  3. Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23, 552–593 (2013). https://doi.org/10.1017/S095679681300018X

    Article  MathSciNet  MATH  Google Scholar 

  4. Carette, J.: Gaussian elimination: a case study in efficient genericity with MetaOCaml. Sci. Comput. Program. 62, 3–24 (2006). Special Issue on the First MetaOCaml Workshop 2004

    Article  MathSciNet  Google Scholar 

  5. Carette, J., Elsheikh, M., Smith, S.: A generative geometric kernel. In: Proceedings of the 20th ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, pp. 53–62. ACM, New York (2011). https://doi.org/10.1145/1929501.1929510

  6. Carette, J., Farmer, W.M.: High-level theories. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 232–245. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85110-3_19

    Chapter  Google Scholar 

  7. Carette, J., Farmer, W.M.: Formalizing mathematical knowledge as a biform theory graph: a case study. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 9–24. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_2

    Chapter  Google Scholar 

  8. Carette, J., Farmer, W.M., Jeremic, F., Maccio, V., O’Connor, R., Tran, Q.M.: The MathScheme library: some preliminary experiments. Technical report, University of Bologna, Italy (2011). uBLCS-2011-04

    Google Scholar 

  9. Carette, J., Farmer, W.M., Kohlhase, M.: Realms: a structure for consolidating knowledge about mathematical theories. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 252–266. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_19

    Chapter  Google Scholar 

  10. Carette, J., Farmer, W.M., Laskowski, P.: HOL light QE. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. LNCS. Springer (2018, forthcoming)

    Chapter  Google Scholar 

  11. Carette, J., Farmer, W.M., O’Connor, R.: MathScheme: project description. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 287–288. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_23

    Chapter  Google Scholar 

  12. Carette, J., Farmer, W.M., Sorge, V.: A rational reconstruction of a system for experimental mathematics. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM -2007. LNCS (LNAI), vol. 4573, pp. 13–26. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_2

    Chapter  Google Scholar 

  13. Carette, J., Kiselyov, O.: Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code. In: Glück, R., Lowry, M. (eds.) GPCE 2005. LNCS, vol. 3676, pp. 256–274. Springer, Heidelberg (2005). https://doi.org/10.1007/11561347_18

    Chapter  Google Scholar 

  14. Carette, J., Kiselyov, O.: Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code. Sci. Comput. Program. 76, 349–375 (2011)

    Article  MathSciNet  Google Scholar 

  15. Carette, J., Kiselyov, O., Shan, C.: Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages. J. Funct. Program. 19, 509–543 (2009). https://doi.org/10.1017/S0956796809007205

    Article  MathSciNet  MATH  Google Scholar 

  16. Carette, J., Kucera, M.: Partial evaluation for maple. In: ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation, pp. 41–50 (2007)

    Google Scholar 

  17. Carette, J., Kucera, M.: Partial evaluation of maple. Sci. Comput. Program. 76, 469–491 (2011)

    Article  Google Scholar 

  18. Carette, J., O’Connor, R.: Theory presentation combinators. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 202–215. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_14

    Chapter  Google Scholar 

  19. Carette, J., Shan, C.C.: Simplifying probabilistic programs using computer algebra. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016, vol. 9585, pp. 135–152. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-28228-2_9

    Chapter  Google Scholar 

  20. Christiansen, D., Brady, E.: Elaborator reflection extending Idris in Idris. SIGPLAN Not. 51, 284–297 (2016). https://doi.org/10.1145/3022670.2951932

    Article  MathSciNet  MATH  Google Scholar 

  21. Christiansen, D.R.: Type-directed elaboration of quasiquotations: a high-level syntax for low-level reflection. In: Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages, IFL 2014, pp. 1:1–1:9. ACM, New York (2014). https://doi.org/10.1145/2746325.2746326

  22. Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56–68 (1940)

    Article  MathSciNet  Google Scholar 

  23. Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of the ACM on Programming Languages (ICFP), vol. 1, p. 34 (2017)

    Article  Google Scholar 

  24. Farmer, W.M.: Formalizing undefinedness arising in calculus. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 475–489. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-25984-8_35

    Chapter  Google Scholar 

  25. Farmer, W.M.: Biform theories in chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM -2007. LNCS (LNAI), vol. 4573, pp. 66–79. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_6

    Chapter  Google Scholar 

  26. Farmer, W.M.: The seven virtues of simple type theory. J. Appl. Logic 6, 267–286 (2008)

    Article  MathSciNet  Google Scholar 

  27. Farmer, W.M.: The formalization of syntax-based mathematical algorithms using quotation and evaluation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 35–50. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_3

    Chapter  Google Scholar 

  28. Farmer, W.M.: Theory Morphisms in Church’s type theory with quotation and evaluation. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 147–162. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-62075-6_11

    Chapter  Google Scholar 

  29. Farmer, W.M.: Incorporating quotation and evaluation into Church’s type theory. Inf. Comput. 260, 9–50 (2018)

    Article  MathSciNet  Google Scholar 

  30. Farmer, W.M., Guttman, J.D., Javier Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55602-8_192

    Chapter  Google Scholar 

  31. Farmer, W.M., von Mohrenschildt, M.: An overview of a formal framework for managing mathematics. Ann. Math. Artif. Intell. 38, 165–191 (2003)

    Article  MathSciNet  Google Scholar 

  32. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)

    MATH  Google Scholar 

  33. Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60–66. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_4

    Chapter  Google Scholar 

  34. Henkin, L.: Completeness in the theory of types. J. Symb. Logic 15, 81–91 (1950)

    Article  MathSciNet  Google Scholar 

  35. van Hoeij, M.: Factoring polynomials and the knapsack problem. J. Number Theory 95, 167–189 (2002). http://www.sciencedirect.com/science/article/pii/S0022314X01927635

    Article  MathSciNet  Google Scholar 

  36. Kohlhase, M.: Mathematical knowledge management transcending the one-brain-barrier with theory graphs. Eur. Math. Soc. Newsl. 92, 22–27 (2014)

    MathSciNet  MATH  Google Scholar 

  37. Kohlhase, M., Mance, F., Rabe, F.: A universal machine for biform theory graphs. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS (LNAI), vol. 7961, pp. 82–97. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39320-4_6

    Chapter  Google Scholar 

  38. Kucera, M., Carette, J.: Partial evaluation and residual theorems in computer algebra. In: Ranise, S., Bigatti, A. (eds.) Proceedings of Calculemus 2006. Electronic Notes in Theoretical Computer Science, Elsevier (2006)

    Google Scholar 

  39. Larjani, P.: Software specialization as applied to computational algebra. Ph.D. thesis, McMaster University (2013)

    Google Scholar 

  40. de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover. In: Automated Deduction - CADE-25, Proceedings of 25th International Conference on Automated Deduction, Berlin, Germany, 1–7 August 2015 (2015)

    Google Scholar 

  41. Narayanan, P., Carette, J., Romano, W., Shan, C., Zinkov, R.: Probabilistic inference by program transformation in Hakaru (system description). In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 62–79. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-29604-3_5

    Chapter  Google Scholar 

  42. Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)

    Google Scholar 

  43. Norell, U.: Dependently typed programming in Agda. In: Kennedy, A., Ahmed, A. (eds.) Proceedings of TLDI 2009, pp. 1–2. ACM (2009)

    Google Scholar 

  44. Rabe, F., Kohlhase, M.: A scalable model system. Inf. Comput. 230, 1–54 (2013)

    Article  Google Scholar 

  45. Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study (2013). https://homotopytypetheory.org/book

  46. Von Zur Gathen, J., Gerhard, J.: Modern Computer Algebra. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  47. van der Walt, P.: Reflection in Agda. Master’s thesis, Universiteit Utrecht (2012)

    Google Scholar 

Download references

Acknowledgments

This research was supported by NSERC. The authors would like to thank the referees for their comments and suggestions.

Author information

Authors and Affiliations

  1. Computing and Software, McMaster University, Hamilton, Canada

    Jacques Carette, William M. Farmer & Yasmine Sharoda

Authors
  1. Jacques Carette
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. William M. Farmer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Yasmine Sharoda
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to William M. Farmer .

Editor information

Editors and Affiliations

  1. Department of Computer Science, Friedrich-Alexander-Universität Erlangen-Nürnberg, Erlangen, Bayern, Germany

    Florian Rabe

  2. Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada

    William M. Farmer

  3. University of Cambridge, Cambridge, United Kingdom

    Grant O. Passmore

  4. Department of Computer Science, The George Washington University, Washington, District of Columbia, USA

    Abdou Youssef

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Carette, J., Farmer, W.M., Sharoda, Y. (2018). Biform Theories: Project Description. In: Rabe, F., Farmer, W., Passmore, G., Youssef, A. (eds) Intelligent Computer Mathematics. CICM 2018. Lecture Notes in Computer Science(), vol 11006. Springer, Cham. https://doi.org/10.1007/978-3-319-96812-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-96812-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-96811-7

  • Online ISBN: 978-3-319-96812-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation