Programs viewed as Skolem functions

• Ralf Steinbrüggen
Part II. Deductive Program Development
Part of the Lecture Notes in Computer Science book series (LNCS, volume 544)

Abstract

Deductive approaches to programming that start from existential propositions, enter the level of pre-algorithmic formulation by means of a transformation rule that formalizes Skolem's idea of quantifier elimination. From this entry on, programs are subjects of mathematical theorems, technically speaking, they are sub-expressions of logical expressions. They should not be isolated from this environment throughout the whole program development for two reasons:
1. (1)

Program transformations depend on theorems. They use theorems that incorporate “constructive ideas” and, of course, theorems that simplify. These must all be textually accessible. Thus this collection of theorems forms a useful framework for the program.

2. (2)

The descendancy relation that establishes the connection between all intermediate versions of the program under development, is monotonic with respect to the logical context. Therefore the statement about the Skolem function is true about the derived algorithm also. Hence, a correctness statement is delivered quite explicitly.

References

1. Bauer, F. L., and Wössner, H. (21984): Algorithmische Sprache und Programmentwicklung. Berlin: Springer.Google Scholar
2. Skolem, Thoralf (1920): Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theorem über dichte Mengen. Skrifter utgitt av Videnskapsselskapet i Kristiania, 1, Mat. Naturv. Kl. 4. English translation in: Heijenoort, J. van (ed.) (1967): From Freege to Gödel. A Source Book in Mathematical Logic, 1879–1931. Cambridge, Mass.: Havard Univ. Press, 252–263.Google Scholar
3. Steinbrüggen, R. (1986): Line-Drawing on a Discrete Grid. TU München, Institut für Informatik, TUM-18610.Google Scholar
4. Steinbrüggen, R. (1988): Brons Decompositions of the Chain Code of a Straight Line. TU München, Institut für Informatik.Google Scholar