Axiomatic Synthesis of Computer Programs and Computability Theorems

TL;DR

This paper introduces a formal program calculus using inference rules to generate and prove properties of programs, including fundamental results like the unsolvability of the halting problem, with applications across logic, number theory, and computability.

Contribution

It presents a novel axiomatic framework for synthesizing programs and proving their properties, formalizing key computability theorems and exploring extensions to various domains.

Findings

Formalized the halting problem as an unprovable program requirement.

Generated programs to determine number divisibility and employee hierarchies.

Proved the unsolvability of the halting problem within the calculus.

Abstract

We introduce a set of eight universal Rules of Inference by which computer programs with known properties (axioms) are transformed into new programs with known properties (theorems). Axioms are presented to formalize a segment of Number Theory, DataBase retrieval and Computability Theory. The resulting Program Calculus is used to generate programs to (1) Determine if one number is a factor of another. (2) List all employees who earn more than their manager. (3) List the set of programs that halt no on themselves, thus proving that it is recursively enumerable. The well-known fact that the set of programs that do not halt yes on themselves is not recursively enumerable is formalized as a program requirement that has no solution, an Incompleteness Axiom. Thus, any axioms (programs) which could be used to generate this program are themselves unattainable. Such proofs are presented to formally generate several additional theorems, including (4) The halting problem is unsolvable. Open problems and future research is discussed, including the use of temporary sort files, programs that calculate statistics (such as counts and sums), the synthesis of programs to solve other well-known problems from Number Theory, Logic, DataBase retrieval and Computability Theory, application to Programming Language Semantics, and the formalization of incompleteness results from Logic and the semantic paradoxes.