On the Composition of Non-parahalting Macro Instructions

Piotr Rudnicki

University of Alberta, Edmonton

This work was partially supported by NSERC Grant OGP9207 and NATO CRG 951368.

Summary.

An attempt to use the {\tt Times} macro, [2], was the origin of writing this article. First, the semantics of the macro composition as developed in [26], [3], [4] is extended to the case of macro instructions which are not always halting. Next, several functors extending the memory handling for {\SCMFSA}, [19], are defined; they are convenient when writing more complicated programs. After this preparatory work, we define a macro instruction computing the Fibonacci sequence (see the SCM program computing the same sequence in [9]) and prove its correctness. The semantics of the {\tt Times} macro is given in [2] only for the case when the iterated instruction is parahalting; this is remedied in [18].

MML Identifier: SFMASTR1

Contents (PDF format)

1. Good Instructions and Good Macro Instruction
2. Composition of Non-parahalting Macro Instructions
3. Memory Allocation
4. A Macro for the Fibonacci Sequence

Bibliography

[1] Noriko Asamoto. Constant assignment macro instructions of \SCMFSA. Part II. Journal of Formalized Mathematics, 8, 1996.

[2] Noriko Asamoto. The \tt loop and \tt times macroinstruction for \SCMFSA. Journal of Formalized Mathematics, 9, 1997.

[3] Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, and Andrzej Trybulec. On the composition of macro instructions. Part II. Journal of Formalized Mathematics, 8, 1996.

[4] Noriko Asamoto, Yatsuka Nakamura, Piotr Rudnicki, and Andrzej Trybulec. On the composition of macro instructions. Part III. Journal of Formalized Mathematics, 8, 1996.

[5] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[6] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[7] Grzegorz Bancerek and Piotr Rudnicki. Development of terminology for \bf scm. Journal of Formalized Mathematics, 5, 1993.

[8] Grzegorz Bancerek and Piotr Rudnicki. Two programs for \bf scm. Part I - preliminaries. Journal of Formalized Mathematics, 5, 1993.

[9] Grzegorz Bancerek and Piotr Rudnicki. Two programs for \bf scm. Part II - programs. Journal of Formalized Mathematics, 5, 1993.

[10] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[11] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[12] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[13] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[14] 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.

[15] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[16] Agata Darmochwal and Andrzej Trybulec. Similarity of formulae. Journal of Formalized Mathematics, 3, 1991.

[17] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.

[18] Piotr Rudnicki. Another \tt times macro instruction. Journal of Formalized Mathematics, 10, 1998.

[19] Piotr Rudnicki and Andrzej Trybulec. Memory handling for \SCMFSA. Journal of Formalized Mathematics, 8, 1996.

[20] Yasushi Tanaka. On the decomposition of the states of SCM. Journal of Formalized Mathematics, 5, 1993.

[21] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.

[22] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[23] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[24] Andrzej Trybulec and Yatsuka Nakamura. Some remarks on the simple concrete model of computer. Journal of Formalized Mathematics, 5, 1993.

[25] Andrzej Trybulec and Yatsuka Nakamura. Modifying addresses of instructions of \SCMFSA. Journal of Formalized Mathematics, 8, 1996.

[26] Andrzej Trybulec, Yatsuka Nakamura, and Noriko Asamoto. On the compositions of macro instructions. Part I. Journal of Formalized Mathematics, 8, 1996.

[27] Andrzej Trybulec, Yatsuka Nakamura, and Piotr Rudnicki. The \SCMFSA computer. Journal of Formalized Mathematics, 8, 1996.

[28] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[29] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.