Skip to main content
SpringerLink
Log in

A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

A typed program logic LMF for recursive specification and verification is presented. It comprises a strict functional programming language with polymorphic and recursively defined partial functions and polymorphic data types. The logic is two-valued with the equality symbol as only predicate. Quantifiers range over the values, which permits inductive proofs of properties. The semantics is based on a contextual (observational) semantics, which gives a consistent presentation of higher-order functions. Our analysis also sheds new light on the the role of partial functions and loose specifications. It is also an analysis of influence of extensions of programs on the tautologies. The main result is that universally quantified equations are conservative, which is also the base for several other conservative classes of formulas.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. ACL2 Website: http://www.cs.utexas.edu/~moore/acl2 (2011). Accessed 1 May 2012

  2. Agda Website: http://wiki.portal.chalmers.se/agda (2011). Accessed 1 May 2012

  3. Barendregt, H.P.: The Lambda Calculus. Its Syntax and Semantics. North-Holland, Amsterdam, New York (1984)

  4. Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Inform. 21, 251–269 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  5. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)

  6. Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In: Antoy, S., Albert, E. (eds.) Proc. PPDP ’08, pp. 89–96. ACM, New York, NY, USA (2008)

  7. Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers: an overview. Math. Struct. Comput. Sci. (2012, to appear). Preprint available at http://www4.informatik.tu-muenchen.de/~krauss/papers/recursion.pdf dates from 2011

  8. Boyer, R.S., Moore, J.S.: Proving theorems about lisp functions. J. ACM 22(1), 129–144 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  9. Boyer, R.S., Moore, J.S.: A mechanical proof of the unsolvability of the halting problem. J. ACM 31(3), 441–458 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  10. Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Morgan, C., Woodcock, J.C.P. (eds.) 3rd Refinement Workshop, pp. 51–69. Springer (1991)

  11. Chiba, Y., Aoto, T., Toyama, Y.: Program transformation by templates based on term rewriting. In: Barahona, P., Felty, A.P. (eds.) Proc. PPDP ’05, pp. 59–69. ACM (2005)

  12. Coq Website: http://coq.inria.fr/ (2011). Accessed 1 May 2012

  13. Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Farmer, W.M.: Mechanizing the traditional approach to partial functions. In: Farmer, W., Kerber, M., Kohlhase, M. (eds.) Proceedings of the Workshop on the Mechanization of Partial Functions, pp. 27–32. CADE-13, Rutgers University, New Brunswick, New Jersey. Available from http://imps.mcmaster.ca/wmfarmer/ (1996). Accessed 1 May 2012

  16. Farmer, W.M.: Formalizing undefinedness arising in calculus. In: Basin, D.A., Rusinowitch, M. (eds.) Proc. IJCAR ’04. Lecture Notes in Comput. Sci., vol. 3097, pp. 475–489. Springer (2004)

  17. Farmer, W.M., Guttman, J.D., Thayer, F.J.: IMPS: an interactive mathematical proof system. J. Autom. Reason. 11(2), 213–248 (1993)

    Article  MATH  Google Scholar 

  18. Felleisen, M., Hieb, R.: The revised report on the syntactic theories of sequential control and state. Theor. Comput. Sci. 103, 235–271 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  19. Finn, S., Fourman, M.P., Longley, J.: Partial functions in a total setting. J. Autom. Reason. 18(1), 85–104 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  20. Fitzgerald, J., Jones, C.: The connection between two ways of reasoning about partial functions. Inf. Process. Lett. 107(3–4), 128–132 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  21. Giesl, J.: Induction proofs with partial functions. J. Autom. Reason. 26(1), 1–49 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  22. Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA (1993)

  23. Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Log. J. IGPL 13(4), 415–433 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  24. HOL4 Website: http://hol.sourceforge.net/ (2011). Accessed 1 May 2012

  25. Howe, D.: Equality in lazy computation systems. In: Parikh, R. (ed.) LICS ’89, pp. 198–203 (1989)

  26. Howe, D.: Proving congruence of bisimulation in functional programming languages. Inf. Comput. 124(2), 103–112 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  27. Isabelle/HOL Website: http://www.cl.cam.ac.uk/research/hvg/isabelle/ (2011). Accessed 1 May 2012

  28. Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice Hall International Series in Computer Science. Prentice Hall (1991)

  29. Kapur, D., Musser, D.R.: Inductive reasoning with incomplete specifications (preliminary report). In: Meyer, A. (ed.) LICS ’86, pp. 367–377. IEEE Computer Society (1986)

  30. Klein, G., Nipkow, T., Paulson, L.: The archive of formal proofs. http://afp.sf.net (2011). Accessed 1 May 2012

  31. Krauss, A.: Partial recursive functions in higher-order logic. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, 17–20 August 2006, Proceedings. Lecture Notes in Comput. Sci., vol. 4130, pp. 589–603. Springer (2006)

  32. Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reason. 44(4), 303–336 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  33. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  34. Mason, I., Talcott, C.L.: Equivalence in functional languages with effects. J. Funct. Program. 1(3), 287–327 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  35. Morris, J.: Lambda-calculus models of programming languages. Ph.D. thesis, MIT (1968)

  36. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Lecture Notes in Comput. Sci., vol. 2283. Springer (2002)

  37. Pitts, A.M.: Operationally-based theories of program equivalence. In: Pitts, A.M., Dybjer, P. (eds.) Semantics and Logics of Computation. Cambridge University Press (1997)

  38. Plotkin, G.D.: Call-by-name, call-by-value, and the lambda-calculus. Theor. Comput. Sci. 1, 125–159 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  39. Sabel, D., Schmidt-Schauß, M., Harwath, F.: Reasoning about contextual equivalence: from untyped to polymorphically typed calculi. In: Fischer, S., Maehle, E., Reischuk, R. (eds.) INFORMATIK 2009. GI Edition - Lecture Notes in Informatics, vol. 154, pp. 369; 2931–2945 (2009)

  40. Sands, D., Gustavsson, J., Moran, A.: Lambda calculi and linear speedups. In: Mogensen, T., Schmidt, D., Sudborough, I. (eds.) The Essence of Computation 2002, pp. 60–84. Springer (2002)

  41. Schieder, B., Broy, M.: Adapting calculational logic to the undefined. Comput. J. 42(2), 73–81 (1999)

    Article  MATH  Google Scholar 

  42. Schlosser, A., Walther, C., Gonder, M., Aderhold, M.: Context dependent procedures and computed types in verifun. Electron. Notes Theor. Comput. Sci. 174(7), 61–78 (2007)

    Article  Google Scholar 

  43. Schmidt-Schauß, M., Sabel, D.: On generic context lemmas for higher-order calculi with sharing. Theor. Comput. Sci. 411(11–13), 1521–1541 (2010)

    Article  MATH  Google Scholar 

  44. Schmidt-Schauß, M., Sabel, D.: A Termination Proof of Reduction in a Simply Typed Calculus with Constructors. Frank report 42, Inst. für Informatik. Goethe-Universität Frankfurt (2010)

  45. Schröder, L., Mossakowski, T.: HasCasl: integrated higher-order specification and program development. Theor. Comput. Sci. 410(12–13), 1217–1260 (2009)

    Article  MATH  Google Scholar 

  46. Scott, D.: A type-theoretical alternative to CUCH, ISWIM, OWHY. Theor. Comput. Sci. 121, 411–440 (1993)

    Article  MATH  Google Scholar 

  47. VeriFun Website: www.inferenzsysteme.informatik.tu-darmstadt.de/verifun/ (2011). Accessed 1 May 2012

  48. Walther, C.: Mathematical induction. In: Gabbay, D.M., Hogger, C.J., Robinson, J.A., Siekmann, J.H. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 127–228. Oxford University Press (1994)

  49. Walther, C., Schweitzer, S.: Reasoning about incompletely defined programs. In: Sutcliffe, G., Voronkov, A. (eds.) Proc. LPAR ’05. Lecture Notes in Comput. Sci., vol. 3835, pp. 427–442 (2005)

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, Goethe-Universität, Postfach 11 19 32, 60054, Frankfurt, Germany

    David Sabel & Manfred Schmidt-Schauß

Authors
  1. David Sabel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Manfred Schmidt-Schauß
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David Sabel.

Electronic Supplementary Material

Below is the link to the electronic supplementary material.

(PDF 392 KB)

Rights and permissions

Reprints and permissions

About this article

Cite this article

Sabel, D., Schmidt-Schauß, M. A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions. J Autom Reasoning 50, 383–421 (2013). https://doi.org/10.1007/s10817-012-9253-6

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-012-9253-6

Keywords

Search

Navigation