The mathematical construction of a program (Q796289)

The paper offers an interesting point of view on the formal theory of programming, using specific mathematical tools at different levels of abstraction, to develop an entirely formal axiomatic basis to program semantics - program construction and correctness proof-checking. The declared aims of the paper are to discuss an elementary theory of theories, to apply this theory at the construction of a (mathematical) proof checker, and to use this proof checker to verify proofs expressed within various theories. A special underlining deserves the multi-level mathematical abstraction approach used by the author to describe the properties of formal theories: theories are initially considered as binary relations on a set of facts; facts are initially defined as non- structured members of a certain set, then as finite sets of atomic facts, later as finite sequences of such facts; atomic facts are identified with finite oriented trees, then with well-formed-formulae, later they are represented by finite sequences corresponding to their pre-order. Theory properties (closedness, generalization functions, specialization functions, etc.) and general useful mechanisms for program construction (change of variables, instantiation, etc.) are developed. Theories based on deductions (section 2) are made up of atomic facts, facts, basic rules (axioms), rules of inference and derived rules (theorems). Using an additive generalization, a general framework for writing down proofs is ketched. Correctness conditions on proofs are formulated. Formulae are characterized as finite oriented trees built on a certain set of symbols. The properties of the operation of instantiation - performed on a tree - are formally defined and proved. Defining the arity of each symbol, the instantiation relation, and other mathematical objects, the correctness conditions on proofs within theories can be redefined so that they can be computed. Section 3 discusses the theories based on definitions (seen as syntactic equivalences), and give two function-based generalizations of such theories. The most frequently met theories are based on both deductions and definitions (section 4). Definitions are generalized to conditional definitions. Such theories are made up from two constituent sub-theories: a deduction-based one and a definition-based one. As an illustration (section 5) on the proposed approach, the propositional calculus and the predicate calculus theories are formalized and the proof checker used to verify proof correctness conditions. To achieve this goal, ''small'' theories of non-dependence and substitution are necessary along with predicate calculus axioms.