Mathematical Foundations of Computer Arithmetics

S. P. Kovalyov

Matematičeskie trudy, Tome 8 (2005) no. 1, pp. 3-42.

Résumé

We propose mathematical methods aimed at formalizing the computer implementation of arithmetic computations. A model-theoretic method of partial interpretation is elaborated for constructing formal specifications of computation models which takes resource limitations into account. Using this method we produce and analyze various integer and rational computation models including, in particular, the positional number systems. Architecture models of the arithmetic are created based on the language of the finite-valued Łukasiewicz logic and logics that enrich it. The weak completeness of such logics enabled us to research into the structural characteristics of operations independent of the representation of numbers. In particular, the mechanisms of detection and processing overflows have been analyzed. Various computation models are represented as bases of logic functions. A technique is proposed for verifying the absence of overflow in computing arithmetic expressions by proving many-valued logic theorems.

Bibliographie

[1] Bauer F. L., Gooz G., Informatika, Vvodnyi kurs, t. 1–2, Mir, M., 1990 | MR

[2] Bochvar D. A., Finn V. K., “O mnogoznachnykh logikakh, dopuskayuschikh formalizatsiyu antinomii. I”, Issledovaniya po matematicheskoi lingvistike, matematicheskoi logike i informatsionnym yazykam, Nauka, M., 1972, 238–295

[3] Vazhennn A. P., “Parallelnye vychisleniya s dinamicheskoi dlinoi operandov: problemy i perspektivy”, Sistemnaya informatika, 7, Nauka, Novosibirsk, 2000, 225–274

[4] Voevodin V. V., “Otobrazhenie problem vychislitelnoi matematiki na arkhitekturu vychislitelnykh sistem”, Vychislitelnye metody i programmirovanie, 1 (2000), 37–44

[5] Gashkov S. B., Chubarnkov V. N., Arifmetika. Algoritmy. Slozhnost vychislenii, Vysshaya shkola, M., 2000

[6] Karpenko A. S., Logiki Lukasevicha i prostye chisla, Nauka, M., 2000 | MR

[7] Kensler G., Chen Ch. Ch., Teoriya modelei, Mir, M., 1977 | MR

[8] Kovalëv S. P., “Analiticheskie modeli mashinnoi arifmetiki”, Sib. zhurn. ind. mat., 6:3 (2003), 88–102 | MR

[9] Kovalëv S. P., “Logika Lukasevicha kak arkhitekturnaya model arifmetiki”, Sib. zhurn. ind. mat., 6:4 (2003), 32–50 | MR

[10] Tarskni A., Vvedenie v logiku i metodologiyu deduktivnykh nauk, IP , Birobidzhan, 2000

[11] Uorren G., Algoritmicheskie tryuki dlya programmistov, Izd-vo , M., 2003

[12] Yablonskii S. V., Diskretnaya matematika i matematicheskie voprosy kibernetiki, Nauka, M., 1974, 9–66

[13] Yablonskii S. V., “Funktsionalnye postroeniya v $k$-znachnoi logike”, Tr. Mat. in-ta im. V. A. Steklova, 51, 1958, 5–142 | Zbl

[14] Beavers G., “Automated theorem proving for Lukasiewicz logics”, Studia Logica, 52:2 (1993), 183–195 | DOI | MR | Zbl

[15] Evans T., Schwartz P. B., “On Slupecki $T$-functions”, J. Symbolic Logic, 23 (1958), 267–270 | DOI | MR

[16] Kahan W., Lecture Notes on the Status of IEEE Standard 754 for Binary Floating-Point Arithmetic, Berkeley, 1996; http://www.cs.berkeley.edu/\allowbreakw̃kahan/ieee754status/IEEE754.pdf

[17] McNaughton R., “A theorem about infinite-valued sentential logic”, J. Symbolic Logic, 16 (1951), 1–13 | DOI | MR | Zbl

[18] Onneweer S. P., Kerkhoff H. G., “High-radix current-mode CMOS circuits based on the truncated-difference operator”, Proc. of the 17th Int. Symp. on Multiple-Valued Logic, IEEE, Boston, 1987, 188–195

[19] Rosenberg I. G., “Completeness properties of multiple-valued logic algebras”, Computer Science and Multiple-Valued Logic, North-Holland, Amsterdam, 1977, 144–186