×

Partial and nested recursive function definitions in higher-order logic. (English) Zbl 1214.68335

Summary: Based on inductive definitions, we develop a tool that automates the definition of partial recursive functions in higher-order logic (HOL) and provides appropriate proof rules for reasoning about them. Termination is modeled by an inductive domain predicate which follows the structure of the recursion. Since a partial induction rule is available immediately, partial correctness properties can be proved before termination is established. It turns out that this modularity also facilitates termination arguments for total functions, in particular for nested recursions. Our tool is implemented as a definitional package extending Isabelle/HOL. Various extensions provide convenience to the user: pattern matching, default values, tail recursion, mutual recursion and currying.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: to Truth through Proof. Academic Press, London (1986) · Zbl 0617.03001
[2] Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comp. Sci. 236(1–2), 133–178 (2000) · Zbl 0938.68051
[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). Lecture Notes in Computer Science, vol. 3085, pp. 34–50. Springer, New York (2004) · Zbl 1100.68615
[4] Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Hagiya, M., Wadler, P. (eds.) Functional and Logic Programming (FLOPS 2006). Lecture Notes in Computer Science, vol. 3945, pp. 114–129. Springer, New York (2006) · Zbl 1185.68616
[5] Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Types for Proofs and Programs (TYPES 2000). Lecture Notes in Computer Science, vol. 2277, pp. 24–40. Springer, New York (2000) · Zbl 1054.68133
[6] Berghofer, S., Reiter, M.: Formalizing the logic-automaton connection. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2009). Lecture Notes in Computer Science, vol. 5674, pp. 147–163. Springer, New York (2009) · Zbl 1252.68250
[7] Berghofer, S., Wenzel, M.: Inductive datatypes in HOL–lessons learned in formal-logic engineering. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’99). Lecture Notes in Computer Science, vol. 1690, pp. 19–36. Springer, New York (1999) · Zbl 0947.68128
[8] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, New York (2004) · Zbl 1069.68095
[9] Bove, A.: Programming in Martin-Löf type theory: unification - a non-trivial example. Licentiate thesis, Department of Computer Science, Chalmers University of Technology (1999)
[10] Bove, A.: General recursion in type theory. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs (TYPES 2002). Lecture Notes in Computer Science, vol. 2646, pp. 39–58. Springer, New York (2002) · Zbl 1023.03532
[11] Bove, A., Capretta, V.: Nested general recursion and partiality in type theory. In: Boulton, R.J., Jackson, P.B. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2001). Lecture Notes in Computer Science, vol. 2152, pp. 121–135. Springer, New York (2001) · Zbl 1005.68512
[12] Bove, A., Capretta, V.: Modelling general recursion in type theory. Math. Struct. Comput. Sci. 15(4), 671–708 (2005) · Zbl 1084.03026
[13] Bove, A., Capretta, V.: Recursive functions with higher-order domains. In: Urzyczyn, P. (ed.) Typed Lambda Calculi and Applications (TLCA 2007). Lecture Notes in Computer Science, vol. 3461, pp. 116–130. Springer, New York (2005) · Zbl 1114.68028
[14] Bove, A., Capretta, V.: Computation by prophecy. In: Rocca, S.R.D. (ed.) Typed Lambda Calculi and Applications (TLCA 2007). Lecture Notes in Computer Science, vol. 4583, pp. 70–83. Springer, New York (2007) · Zbl 1215.03047
[15] Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979) · Zbl 0448.68020
[16] Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988) · Zbl 0655.68117
[17] Bulwahn, L., Krauss, A., Nipkow, T.: Finding lexicographic orders for termination proofs in Isabelle/HOL. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007). Lecture Notes in Computer Science, vol. 4732, pp. 38–53. Springer, New York (2007) · Zbl 1144.68352
[18] Cowles, J., Greve, D., Young, W.: The while-language challenge: first progress. In: ACL2 Workshop Proceedings (2007)
[19] Dubois, C., Donzeau-Gouge, V.: A step towards the mechanization of partial functions: domains as inductive predicates. In: CADE-15 Workshop on Mechanization of Partial Functions (1998)
[20] Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65(2), 525–549 (2000) · Zbl 0960.03048
[21] Finn, S., Fourman, M., Longley, J.: Partial functions in a total setting. J. Autom. Reason. 18(1), 85–104 (1997) · Zbl 0870.68136
[22] Giesl, J.: Termination of nested and mutually recursive algorithms. J. Autom. Reason. 19(1), 1–29 (1997) · Zbl 0882.68019
[23] Giesl, J.: Induction proofs with partial functions. J. Autom. Reason. 26(1), 1–49 (2001) · Zbl 0971.03016
[24] Gordon, M., Melham, T. (eds.): Introduction to HOL: a Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993) · Zbl 0779.68007
[25] Greve, D.: Assuming termination. In: ACL2 Workshop Proceedings (2009)
[26] Greve, D.A., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz-Reina, J.-L., Sumners, R., Vroon, D., Wilding, M.: Efficient execution in an automated reasoning environment. J. Funct. Program. 18(1), 15–46 (2008) · Zbl 1128.68090
[27] Haftmann, F., Nipkow, T.: A code generator framework for Isabelle/HOL. Technical report 364/07, Department of Computer Science, University of Kaiserslautern (2007)
[28] Harrison, J.: The HOL Light theorem prover. http://www.cl.cam.ac.uk/users/\(\sim\)jrh13/hol-light
[29] Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer, Dordrecht (2000)
[30] Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning (IJCAR 2006). Lecture Notes in Artificial Intelligence, vol. 4130, pp. 589–603. Springer, New York (2006) · Zbl 1222.68367
[31] Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) Automated Deduction (CADE-21). Lecture Notes in Computer Science, vol. 4603, pp. 460–476. Springer, New York (2007) · Zbl 1213.68571
[32] Krstić, S., Matthews, J.: Inductive invariants for nested recursion. In: Basin, D.A., Wolff, B. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2003). Lecture Notes in Computer Science, vol. 2758, pp. 253–269. Springer, New York (2003) · Zbl 1279.68289
[33] Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Principles of Programming Languages (PoPL 2001), pp. 81–92 (2001) · Zbl 1323.68216
[34] Manna, Z., Waldinger, R.: Deductive synthesis of the unification algorithm. Sci. Comput. Program. 1, 5–48 (1981) · Zbl 0472.68054
[35] Manolios, P., Moore, J.S.: Partial functions in ACL2. J. Autom. Reason. 31(2), 107–127 (2003) · Zbl 1060.68109
[36] McBride, C.: Dependently typed functional programs and their proofs. PhD thesis, University of Edinburgh (1999)
[37] Müller, O., Slind, K.: Treating partiality in a logic of total functions. Comput. J. 40(10), 640–652 (1997) · Zbl 05470453
[38] Naraschewski, W., Wenzel, M.: Object-oriented verification based on record subtyping in higher-order logic. In: Grundy, J., Newey, M.C. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’98). Lecture Notes in Computer Science, vol. 1479, pp. 349–366. Springer, New York (1998) · Zbl 0927.03026
[39] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – a Proof Assistant for Higher-order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, New York (2002) · Zbl 0994.68131
[40] Nishihara, T., Minamide, Y.: Depth first search. In: Klein, G., Nipkow, T., Paulson, L. (eds.) The Archive of Formal Proofs. http://afp.sf.net/entries/Depth-First-Search.shtml . Formal proof development (2004)
[41] Owens, S., Slind, K.: Adapting functional programs to higher-order logic. Higher-order and Symbolic Computation 21(4), 377–409 (2008) · Zbl 1175.68103
[42] Paulson, L.C.: Verifying the unification algorithm in LCF. Sci. Comput. Program. 5, 143–170 (1985) · Zbl 0567.68054
[43] Paulson, L.C.: A fixedpoint approach to implementing (co)inductive definitions. In: Bundy, A. (ed.) Automated Deduction (CADE-12). Lecture Notes in Computer Science, vol. 814, pp. 148–161. Springer, New York (1994)
[44] Slind, K.: Function definition in higher-order logic. In: von Wright, J., Grundy, J., Harrison, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’96). Lecture Notes in Computer Science, vol. 1125, pp. 381–397. Springer, New York (1996)
[45] Slind, K.: Reasoning about terminating functional programs. PhD thesis, Institut für Informatik, Technische Universität München (1999)
[46] Slind, K.: Another look at nested recursion. In: Aagaard, M., Harrison, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLS 2000). Lecture Notes in Computer Science, vol. 1869, pp. 498–518. Springer, New York (2000) · Zbl 0974.68180
[47] Urban, C.: Nominal techniques in Isabelle/HOL. J. Autom. Reason. 40(4), 327–356 (2008) · Zbl 1140.68061
[48] Walther, C.: On proving the termination of algorithms by machine. J. Artif. Intell. 71(1), 101–157 (1994) · Zbl 0938.68819
[49] Wenzel, M.: Isabelle/Isar–a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, Technische Universität München (2002)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.