Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993
Association of Mizar Users
A Compiler of Arithmetic Expressions for SCM
-
Grzegorz Bancerek
-
Polish Academy of Sciences, Institute of Mathematics, Warsaw
-
Piotr Rudnicki
-
University of Alberta, Department of Computing Science, Edmonton
Summary.
-
We define a set of binary arithmetic expressions with the following
operations: $+$, $-$, $\cdot$, {\tt mod}, and {\tt div} and formalize the
common meaning of the expressions in the set of integers.
Then, we define a compile function that for a given expression
results in a program for the {\bf SCM} machine defined by Nakamura
and Trybulec in [14]. We prove that the generated program
when loaded into the machine and executed computes the value of
the expression. The program uses additional memory and runs
in time linear in length of the expression.
This work was partially supported by NSERC Grant OGP9207
while the first author visited University of Alberta, May--June 1993.
The terminology and notation used in this paper have been
introduced in the following articles
[16]
[10]
[22]
[19]
[1]
[21]
[17]
[8]
[9]
[2]
[3]
[14]
[15]
[20]
[18]
[5]
[4]
[11]
[12]
[6]
[7]
[13]
Contents (PDF format)
Bibliography
- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Grzegorz Bancerek.
K\"onig's Lemma.
Journal of Formalized Mathematics,
3, 1991.
- [3]
Grzegorz Bancerek.
Joining of decorated trees.
Journal of Formalized Mathematics,
5, 1993.
- [4]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Grzegorz Bancerek and Piotr Rudnicki.
Development of terminology for \bf scm.
Journal of Formalized Mathematics,
5, 1993.
- [6]
Grzegorz Bancerek and Piotr Rudnicki.
On defining functions on binary trees.
Journal of Formalized Mathematics,
5, 1993.
- [7]
Grzegorz Bancerek and Piotr Rudnicki.
On defining functions on trees.
Journal of Formalized Mathematics,
5, 1993.
- [8]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [9]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
- [10]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
- [11]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a non-empty sets.
Journal of Formalized Mathematics,
2, 1990.
- [12]
Patricia L. Carlson and Grzegorz Bancerek.
Context-free grammar --- part I.
Journal of Formalized Mathematics,
4, 1992.
- [13]
Jaroslaw Kotowicz.
The limit of a real function at infinity.
Journal of Formalized Mathematics,
2, 1990.
- [14]
Yatsuka Nakamura and Andrzej Trybulec.
A mathematical model of CPU.
Journal of Formalized Mathematics,
4, 1992.
- [15]
Yatsuka Nakamura and Andrzej Trybulec.
On a mathematical model of programs.
Journal of Formalized Mathematics,
4, 1992.
- [16]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [17]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
- [18]
Andrzej Trybulec.
Function domains and Fr\aenkel operator.
Journal of Formalized Mathematics,
2, 1990.
- [19]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
- [20]
Andrzej Trybulec and Yatsuka Nakamura.
Some remarks on the simple concrete model of computer.
Journal of Formalized Mathematics,
5, 1993.
- [21]
Michal J. Trybulec.
Integers.
Journal of Formalized Mathematics,
2, 1990.
- [22]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
Received December 30, 1993
[
Download a postscript version,
MML identifier index,
Mizar home page]