Another \tt times Macro Instruction

Piotr Rudnicki

University of Alberta, Edmonton

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

Summary.

The semantics of the {\tt times} macro is given in [2] only for the case when the body of the macro is parahalting. We remedy this by defining a new {\tt times} macro instruction in terms of {\tt while} (see [11], [14]). The semantics of the new {\tt times} macro is given in a way analogous to the semantics of {\tt while} macros. The new {\tt times} uses an anonymous variable to control the number of its executions. We present two examples: a trivial one and a remake of the macro for the Fibonacci sequence (see [13]).

MML Identifier: SFMASTR2

Contents (PDF format)

1. {\SCMFSA} Preliminaries
2. Another {\tt times} Macro Instruction
3. A Trivial Example
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. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[6] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[7] Grzegorz Bancerek and Piotr Rudnicki. Two programs for \bf scm. Part I - preliminaries. 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. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[11] Jing-Chao Chen. While macro instructions of \SCMFSA. Journal of Formalized Mathematics, 9, 1997.

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

[13] Piotr Rudnicki. On the composition of non-parahalting macro instructions. Journal of Formalized Mathematics, 10, 1998.

[14] Piotr Rudnicki. The \tt while macro instructions of \SCMFSA. Part II. Journal of Formalized Mathematics, 10, 1998.

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

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

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

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

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

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

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

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