Philosophical Transactions of the Royal Society A, Mathematical, Physical and Engineering Sciences, vol.312, issue 1522
Programming as a mathematical exercise
Abstract
This paper contains a formal framework within which
logic,
set theory and
programming
are presented together.
These elements can be presented together because, in this work, we no longer regard a (procedural) programming notation (such as PASCAL) as a notation for expressing a computation; rather, we regard it as a mere extension to the conventional language of logic and set theory. The extension constitutes a convenient (economical) way of expressing certain relational statements.
A consequence of this point of view is that the activity of program construction is transformed into that of proof construction
To ensure that this activity of proof construction can be given a sound mechanizable foundation, we present a number of theories in the form of some basic deduction and definition rules.
For instance, such theories compose the two logical calculi, a weaker version of the standard Zermelo-Fraenkel set theory, as well as some other elementary mathematical theories leading up to the construction of natural numbers. This last theory acts as a paradigm for the construction of other types such as sequences or trees. Parallel to these mathematical constructions we axiomatize a certain programming notation by giving equivalents to its basic constructs within logic and set theory. A number of other non-logical theories are also presented, which allows us to completely mechanize the calculus of proof that is implied by this framework
Articles
Aucun commentaire:
Enregistrer un commentaire