Skip to main content
SpringerLink
Log in

Reasoning about partial functions with the aid of a computer

  • Published:
Erkenntnis Aims and scope Submit manuscript

Abstract

Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows how the traditional approach to partial functions can be formalized in a range of formalisms that includes first-order logic, simple type theory, and Von-Neumann—Bernays—Gödel set theory. It argues that these new formalisms allow one to directly reason about partial functions; are based on natural, well-understood, familiar principles; and can be effectively implemented in mechanized mathematics systems.

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

  • Barringer, H., J. H. Cheng, and C. B. Jones: 1984, ‘A Logic Covering Undefinedness in Program Proofs’,Acta Informatica 21, 251–69.

    Google Scholar 

  • Beeson, M.: 1981, ‘Formalizing Constructive Mathematics: Why and How?’, in F. Richman (ed.),Constructive Mathematics: Proceedings, New Mexico, 1980, Vol. 873 ofLecture Notes in Mathematics, Springer-Verlag, Berlin, pp. 146–90.

    Google Scholar 

  • Beeson, M. J.: 1985,Foundations of Constructive Mathematics, Springer-Verlag, Berlin.

    Google Scholar 

  • Burge, T.: 1971,Truth and Some Referential Devices, Ph.D. thesis, Princeton University.

  • Burge, T.: 1991, ‘Truth and Singular Terms’, in K. Lambert (ed.),Philosophical Applications of Free Logic, Oxford University Press, Oxford, pp. 189–204.

    Google Scholar 

  • Cheng, J. H. and C. B. Jones: 1991, ‘On the Usability of Logics which Handle Partial Functions’, in C. Morgan and J. C. P. Woodcock (eds.),3rd Refinement Workshop, Springer-Verlag, Berlin, pp. 51–69.

    Google Scholar 

  • Church, A.: 1940, ‘A Formulation of the Simple Theory of Types’,Journal of Symbolic Logic 5, 56–68.

    Google Scholar 

  • Constable, R. L.: 1982, ‘Partial Functions in Constructive Formal Theories’, in A. B. Cremers and H. P. Kriegel (eds.),Theoretical Computer Science, Vol. 145 ofLecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 1–18.

    Google Scholar 

  • Constable, R. L. and S. F. Smith: 1987, ‘Partial Objects in Constructive Type Theory’, in A. K. Chandra (ed.),Symposium on Logic in Computer Science (Proceedings), Computer Society of the IEEE, Washington, D.C., pp. 183–93.

    Google Scholar 

  • Farmer, W. M.: 1990, ‘A Partial Functions Version of Church's Simple Theory of Types’,Journal of Symbolic Logic 55, 1269–91.

    Google Scholar 

  • Farmer, W. M.: 1993, ‘A Simple Type Theory with Partial Functions and Subtypes’,Annals of Pure and Applied Logic 64, 211–40.

    Google Scholar 

  • Farmer, W. M.: 1994, ‘Theory Interpretation in Simple Type Theory’, in: J. Heering et al. (eds.),Higher-Order Algebra, Logic, and Term Rewriting, Vol. 816 ofLecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 96–123.

    Google Scholar 

  • Farmer, W. M., J. D. Guttman, and F. J. Thayer: 1993a, ‘Imps: An Interactive Mathematical Proof System’,Journal of Automated Reasoning 11, 213–48.

    Google Scholar 

  • Farmer, W. M., J. D. Guttman, and F. J. Thayer: 1993b, ‘TheImps User's Manual’,Technical Report M93B-138, TheMitre Corporation, Bedford, Massachusetts.

    Google Scholar 

  • Farmer, W. M., J. D. Guttman, and F. J. Thayer: 1995, ‘Contexts in Mathematical Reasoning and Computation’,Journal of Symbolic Computation 19, 201–16.

    Google Scholar 

  • Feferman, S.: 1990, ‘Polymorphic Typed Lambda-Calculi in a Type-Free Axiomatic Framework’,Contemporary Mathematics 106, 101–36.

    Google Scholar 

  • Gödel, K.: 1940,The Consistency of the Axiom of Choice and the Generalized Continuum Hypothesis with the Axioms of Set Theory, Vol. 3 ofAnnals of Mathematical Studies, Princeton University Press, Princeton.

    Google Scholar 

  • Hailperin, T. and H. Leblanc: 1959, ‘Non-Designating Singular Terms’,Philosophical Review 68, 239–43.

    Google Scholar 

  • Hintikka, J.: 1959, ‘Existential Presuppositions and Existential Commitments’,Journal of Philosophy 56, 125–37.

    Google Scholar 

  • Hoogewijs, A.: 1987, ‘Partial-Predicate Logic in Computer Science’,Acta Informatica 24, 381–93.

    Google Scholar 

  • Kerber, M. and M. Kohlhase: 1994, ‘A Mechanization of Strong Kleene Logic for Partial Functions’, in A. Bundy (ed.),Automated Deduction — CADE-12, Vol. 814 ofLecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 371–85.

    Google Scholar 

  • Kuper, J.: 1993, ‘An Axiomatic Theory for Partial Functions’,Information and Computation 107, 104–50.

    Google Scholar 

  • Lambert, K.: 1963, ‘Existential Import Revisited’,Notre Dame Journal of Formal Logic 4, 288–92.

    Google Scholar 

  • Lambert, K. (ed.): 1991,Philosophical Applications of Free Logic, Oxford University Press, Oxford.

    Google Scholar 

  • Lambert, K. and B. C. van Fraassen: 1972,Derivation and Counterexample, Dickenson Publishing, Encino, California.

    Google Scholar 

  • Leonard, H. S.: 1956, ‘The Logic of Existence’,Philosophical Studies 4, 49–64.

    Google Scholar 

  • Lepage, F.: 1992, ‘Partial Functions in Type Theory’,Notre Dame Journal of Formal Logic 33, 493–516.

    Google Scholar 

  • Lucio-Carrasco, F. and A. Gavilanes-Franco: 1989, ‘A First Order Logic for Partial Functions’, in B. Monien and R. Cori (eds.),STACS 89, Vol. 349 ofLecture Notes in Computer Science, Springer-Verlag, Berlin, pp. 47–58.

    Google Scholar 

  • Mendelson, E.: 1964,Introduction to Mathematical Logic, Van Nostrand, Princeton.

    Google Scholar 

  • Monk, L. G.: 1986, ‘Pdlm: A Proof Development Language for Mathematics’, Technical Report M86-37, TheMitre Corporation, Bedford, Massachusetts.

    Google Scholar 

  • Novak, I. L.: 1950, ‘A Construction for Models of Consistent Systems’,Fundamenta Mathematicae 37, 87–110.

    Google Scholar 

  • Parnas, D. L.: 1993, ‘Predicate Logic for Software Engineering’,IEEE Transactions on Software Engineering 19, 856–61.

    Google Scholar 

  • Rescher, N.: 1959, ‘On the Logic of Existence and Denotation’,Philosophical Review 68, 157–80.

    Google Scholar 

  • Rosser, J. B. and H. Wang: 1950, ‘Non-Standard Models for Formal Logics’,Journal of Symbolic Logic 15, 113–29.

    Google Scholar 

  • Schock, R.: 1968,Logics without Existence Assumptions, Almqvist & Wiksells, Stockholm.

    Google Scholar 

  • Scott, D. S.: 1967, ‘Existence and Description in Formal Logic’, in R. Schoenmann (ed.),Bertrand Russell: Philosopher of the Century, Allen and Unwin, London, pp. 181–200.

    Google Scholar 

  • Scott, D. S.: 1979, ‘Identity and Existence in Intuitionistic Logic’, in M. P. Fourman et al. (eds.),Application of Sheaves: Proceedinys, Durham 1977, Vol. 753 ofLecture Notes in Mathematics, Springer-Verlag, Berlin, pp. 660–96.

    Google Scholar 

  • Shoenfield, J.: 1954, ‘A Relative Consistency Proof’,Journal of Symbolic Logic 19, 21–8.

    Google Scholar 

  • Smiley, T.: 1960, ‘Sense Without Denotation’,Analysis 20, 125–35.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Center for Integrated Intelligence Systems, The MITRE Corporation, 202 Burlington Road, 01730-1420, Bedford, MA, USA

    William M. Farmer

Authors
  1. William M. Farmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Additional information

Supported by the MITRE-Sponsored Research program. This paper is a written version (with references) of an address given at the Partial Functions and Programming: Foundational Questions conference held 17 February 1995 at the University ol California at Irvine.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Farmer, W.M. Reasoning about partial functions with the aid of a computer. Erkenntnis 43, 279–294 (1995). https://doi.org/10.1007/BF01135375

Download citation

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01135375

Keywords

Search

Navigation