Programming in Constructive Set Theory: Some examples

ABSTRACT

Per Martin-Löf's Constructive Set Theory is a mathematical language with computation rules. It is primarily designed to be a language for mathematical reasoning. The language has a very simple semantics and its rules have a simple structure. Since it is a language for constructive mathematics, it is possible to execute the proof (the construction of a proposition) as a program. The language can be seen as a programming language without assignments and other side effects. Compared to traditional functional languages it has a very rich type structure in that the type of an expression can completely specify the task of the exprestion. A sorting algorithm, for instance, can be conventionally specified to have a type sort: List(A) → List(A) which is type-correct if sort is any function taking a list as argument and producing a list as result. It is, however, also possible to specify that sort is a function taking a list as argument and producing a sorted permutation of it s input as result, i.e. sort: (@@@@ x &egr; List(A)) (&Sgr; y &egr; List(A)) (Perm(x,y) × Sorted(y)) The type (or the task) of the program can be read as the proposition (@@@@x &egr; List(A)) (@@@@y &egr; List(A) (Perm(x,y) & Sorted(y)) which is read “for all lists x, there is a sorted permutation y of x”. We can prove that this proposition is true, using the rules of the language to construct a program for the task. If the proposition were not true, it would be impossible to find a program for it and we would have had an impossible task. The types of Constructive Set Theory can be seen as a specification language for the programs, but of course there is only one language, avoiding the complexity of mixing a programming language with a logical language. The similarity (or rather: identity) between a mathematical proof of a given proposition and a program for a given task suggests that programming should be similar to the mathematicians activity of finding proofs. We have illustrate d this with an example of how a proof of the Euclidean division theorem yields a program to compute the quotient and the remainder between two natural numbers. The paper contains a description of the language. Since all programs in the language terminate, the proof rules and the semantics are simple. We give some examples of programming with lists and reasoning about the programs. We also define the Ackermann function.

REFERENCES

• 1: Per Martin-Löf: "An Intuitionistic Theory of Types: Predicative Part", Logic Colloquium '73, ed. Rose, Shepherdson, North-Holland, Amsterdam, 1975, pp. 73-118.
• 2: Per Martin-Löf: "Constructive Mathematics and Computer programming", Dept of Math, University of Stockholm, 113 85 Stockholm, Sweden, read at the 6th International Congress for Logic, Methodology of Science, Hannover 1979.
• 3: Takasu: Proofs and Programs, The Third IBM Symposium on Mathematical Foundation of Computer Science, Aug. 1978.
• 4: Goto: Program Synthesis from Natural Deduction Proofs, IJCAI 1979, Tokyo.
• 5: John McCarthy: "A formal description of a subset of Algol 60", in Formal Language Description Languages, ed. Steel, North-Holland.
• 6: Dag Prawitz: "Natural Deduction, a Proof Theoretical Study", Almqvist & Wiksell, Stock-holm 1965.
• 7: Christopher Alan Goad, Computational uses of the manipulation of formal proofs, 1980

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Set theory

General Terms:
Languages, Theory