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.

MML Identifier: SCM_COMP

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.