Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

A Mathematical Model of CPU

Yatsuka Nakamura
Shinshu University, Nagano
Andrzej Trybulec
Warsaw University, Bialystok
The work has been done while the second author was visiting Nagano in autumn 1992.

Summary.

This paper is based on a previous work of the first author [13] in which a mathematical model of the computer has been presented. The model deals with random access memory, such as RASP of C. C. Elgot and A. Robinson [12], however, it allows for a more realistic modeling of real computers. This new model of computers has been named by the author (Y. Nakamura, [13]) Architecture Model for Instructions (AMI). It is more developed than previous models, both in the description of hardware (e.g., the concept of the program counter, the structure of memory) as well as in the description of instructions (instruction codes, addresses). The structure of AMI over an arbitrary collection of mathematical domains N consists of: \begin{description} \item{ - }a non-empty set of objects, \item{ - }the instruction counter, \item{ - }a non-empty set of objects called instruction locations, \item{ - }a non-empty set of instruction codes, \item{ - }an instruction code for halting, \item{ - }a set of instructions that are ordered pairs with the first element being an instruction code and the second a finite sequence in which members are either objects of the AMI or elements of one of the domains included in N, \item{ - }a function that assigns to every object of AMI its kind that is either {\em an instruction} or {\em an instruction location} or an element of N, \item{ - }a function that assigns to every instruction its execution that is again a function mapping states of AMI into the set of states. \end{description} By a state of AMI we mean a function that assigns to every object of AMI an element of the same kind. In this paper we develop the theory of AMI. Some properties of AMI are introduced ensuring it to have some properties of real computers: \begin{description} \item{ - }a von Neumann AMI, in which only addresses to instruction locations are stored in the program counter, \item{ - }data oriented, those in which instructions cannot be stored in data locations, \item{ - }halting, in which the execution of the halt instruction is the identity mapping of the states of an AMI, \item{ - }steady programmed, the condition in which the contents of the instruction locations do not change during execution, \item{ - }definite, a property in which only instructions may be stored in instruction locations. \end{description} We present an example of AMI called a Small Concrete Model which has been constructed in [13]. The Small Concrete Model has only one kind of data: integers and a set of instructions, small but sufficient to cope with integers.

MML Identifier: AMI_1

The terminology and notation used in this paper have been introduced in the following articles [15] [8] [17] [16] [2] [18] [5] [6] [11] [1] [9] [14] [10] [3] [4] [7]

Contents (PDF format)

1. Preliminaries
2. General concepts
3. Preliminaries
4. Superproducts
5. General theory
6. Finite substates
7. Preprograms
8. Computability

Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.
[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[9] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.
[10] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[11] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[12] C.C. Elgot and A. Robinson. Random access stored-program machines, an approach to programming languages. \em J.A.C.M., 11(4):365--399, Oct 1964.
[13] Yatsuka Nakamura. On a mathematical model of CPU and algorithm. Technical report, Shinshu University, Aug 1991.
[14] Andrzej Trybulec. Binary operations applied to functions. Journal of Formalized Mathematics, 1, 1989.
[15] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[16] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[17] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[18] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received October 14, 1992