Arithmetic algorithms in a proof-oriented set-theoretic language

ABSTRACT

Recently, a pseudocode language for set-theoretic algorithms hos been investigated for use In discrete math/structures courses [1-4]. The language is highly intuitive and contains only eight elementary statements. In the language, it is possible to (a) readily express the elementary algorithms of discrete mathematics and (b) develop correctness proofs using set theory and its underlying logic (without resort to logical-invariance proofs). In this paper, it is demonstrated that correct algorithms for the arithmetic operations over natural numbers are essentially corollaries of two easily-proved theorems about primitive recursion. In essence, for a function defined over natural numbers, a correct definition by mathematical induction immediately yields a correct algorithm for computation.

REFERENCES

• 1: T. G. Windeknecht, Toward a theory of correct set algorithms, Proceedings of the 1988 ACM sixteenth annual conference on Computer science, p.37-46, February 1988, Atlanta, Georgia, United States [doi>10.1145/322609.322614]
• 2: T. 6. Wlndeknecht, "A Proof-OMented Set-Theoretlc Language', (submitted for publicatlon), 1988.
• 3: T. G. Windeknecht, "An Introduction To Set Algorithms," Technical Report No. TR-CSE-87- I0, Oakland University, Rochester, Michigan 48063, 1987.
• 4: T. G. Windeknecht, Mathematical Foundations Of COmDuter Science (Theorems. Proofs. and AlBoMthms), (book manuscript, submitted for publication), 1988.
• 5: J. L. Kelley, General Toooloqy, Van Nostrand, PMnceton, New Jersey, 1955 (appendix).
• 6: P. Suppes, AxiOmatic Set Theory, Van Nostrand, Princeton, New Jersey, 1960.
• 7: H. Hermes, Enumerabtlitq, Decldablllty, Comoutabllity, 2nd edition, Sprlnger-Verleg, New York, 1969.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Classes defined by grammars or automata (e.g., context-free languages, regular sets, recursive sets)

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

General Terms:
Algorithms, Languages, Theory, Verification