Top

Published in:

2019 | OriginalPaper | Chapter

Towards Specifying Symbolic Computation

Authors : Jacques Carette, William M. Farmer

Published in: Intelligent Computer Mathematics

Publisher: Springer International Publishing

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

search-config

AI-assisted search

Off

Abstract

Many interesting and useful symbolic computation algorithms manipulate mathematical expressions in mathematically meaningful ways. Although these algorithms are commonplace in computer algebra systems, they can be surprisingly difficult to specify in a formal logic since they involve an interplay of syntax and semantics. In this paper we discuss several examples of syntax-based mathematical algorithms, and we show how to specify them in a formal logic with undefinedness, quotation, and evaluation.

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 "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

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

previous chapter Comparing Machine Learning Models to Choose the Variable Ordering for Cylindrical Algebraic Decomposition

next chapter Lemma Discovery for Induction

I.e., denotation.

There are nonessential Maple-isms in this routine: because of how foldr is defined, op is needed to transform a list to an expression sequence; in other languages, this is unnecessary. Note however that it is possible to express the type extremely precisely.

This is unsurprising given that the builders of both Maple and Mathematica were well acquainted with Macsyma which was implemented in Lisp.

Mathematica has similar commands.

Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed Template-Coq. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 20–39. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94821-8_2CrossRef

Beeson, M.: Logic and computation in MATHPERT: an expert system for learning mathematics. In: Kaltofen, E., Watt, S. (eds.) Computers and Mathematics, pp. 202–214. Springer, New York (1989). https://doi.org/10.1007/978-1-4613-9647-5_25CrossRef

Boyer, R., Moore, J.: Metafunctions: proving them correct and using them efficiently as new proof procedures. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Science, pp. 103–185. Academic Press, Cambridge (1981)MATH

Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Log. 4, 470–504 (2006)MathSciNetCrossRef

Carette, J., Farmer, W.M., Laskowski, P.: HOL light QE. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 215–234. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94821-8_13CrossRef

Christiansen, D.R.: Type-directed elaboration of quasiquotations: a high-level syntax for low-level reflection. In: Proceedings of the 26th 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

Dunstan, M., Kelsey, T., Linton, S., Martin, U.: Lightweight formal methods for computer algebra systems. In: Weispfenning, V., Trager, B.M. (eds.) Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, pp. 80–87. ACM (1998)

Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1(ICFP), 34 (2017)CrossRef

Farmer, W.M.: A simple type theory with partial functions and subtypes. Ann. Pure Appl. Log. 64, 211–240 (1993)MathSciNetCrossRef

10.

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_35CrossRef

11.

Farmer, W.M.: Andrews’ type system with undefinedness. In: Benzmüller, C., Brown, C., Siekmann, J., Statman, R. (eds.) Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday, pp. 223–242. Studies in Logic, College Publications (2008)

12.

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_11CrossRef

13.

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

14.

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_4CrossRef

15.

Kaliszyk, C.: Automating side conditions in formalized partial functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 300–314. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85110-3_26CrossRef

16.

Kaliszyk, C., Wiedijk, F.: Certified Computer Algebra on Top of an Interactive Theorem Prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus/MKM -2007. LNCS (LNAI), vol. 4573, pp. 94–105. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73086-6_8CrossRef

17.

Khan, M.T.: Formal specification and verification of computer algebra software. Ph.D. thesis, RISC, Johannes Kepler Universität Linz (2014)

18.

Khan, M.T., Schreiner, W.: Towards the formal specification and verification of maple programs. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 231–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31374-5_16CrossRef

19.

Limongelli, C., Temperini, M.: Abstract specification of structures and methods in symbolic mathematical computation. Theor. Comput. Sci. 104, 89–107 (1992)MathSciNetCrossRef

20.

Melham, T., Cohn, R., Childs, I.: On the semantics of ReFLect as a basis for a reflective theorem prover. Computing Research Repository (CoRR) abs/1309.5742 (2013). arxiv:1309.5742

21.

van der Walt, P., Swierstra, W.: Engineering proof by reflection in agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157–173. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41582-1_10CrossRef

22.

Watt, S.M.: Making computer algebra more symbolic. In: Proceedings of Transgressive Computing 2006, Granada, Spain, pp. 43–49 (2006)

Title: Towards Specifying Symbolic Computation
Authors: Jacques Carette
William M. Farmer
Publisher: Springer International Publishing
Book: Intelligent Computer Mathematics
Print ISBN: 978-3-030-23249-8

Electronic ISBN: 978-3-030-23250-4

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-23250-4_8

Springer Professional

Abstract

Please log in to get access to your license.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner