Информационная система "Конференции"

Abstracts

Applications of logic in computer science

One of the key problems that arises at developing automatic computing systems is caused by restrictions on available amount of memory resources. Due to it computer implementations of arithmetic cannot satisfy standard arithmetic axioms that have only infinite models. Nevertheless arithmetic devices are required to have supported numbers behaving similarly to their theoretical originals. Software engineers qualify this situation as conflict between functional and non-functional requirements to computation models. With regard to semiconductor computers this conflict is considered as de-facto resolved few decades ago (although, as shown in the report, not ideally). However, when developing novel non-traditional computing devices the problem arises again.

General mathematical methods are needed to solve it. Traditionally, the Abstract Data Type technique is used [5]. However it doesn’t help because it doesn’t offer tools for abstract modeling of infinite entities by finite structures. The author of the report has suggested one such tool in [3]: it is special modification of standard model-theoretic approach called partial interpretation of first-order theory T. It lies in constructing algebraic system that must verify only those statements from T that contain only terms that can be substituted by constants from given finite subsignature of its signature. The set of such statements is called projection of T to this subsignature. Thus the formal specification of resource available to represent objects described by T is constituted by the explicitly given set of constant symbols.

Computer arithmetics are formally specified as partial interpretations of arithmetic theories over universe E_n+1={0,1,...,n}. In this report such partial interpretations of integral arithmetic are considered that show high degree of similarity to originals according to certain formally defined criteria. The following two partial interpretations are most adequate: overflow arithmetic

OA_n+1 = <E_n+1, 0, 1, ..., n-1, =, |+|, |-|, |x|>

and modulo n arithmetic

MA_n+1 = <E_n+1, 0, 1, ..., [(n-1)/2], -[n/2], ..., -1, (=), (+), (-), (x), Carry>.

These specifications are used to perform mapping of computing algorithms to computer architecture, i.e. binding stream of computations to functional capabilities of employed computing devices [8]. Abstract mathematical method of modeling computer architectures is needed here. It should offer verification technique based on formal proof. As a basis for such method the author of the report has suggested to employ multiple-valued Lukasiewicz logic [4]. Numerical data storage units (variables) are used as architecture elements of computer arithmetic. Their values (states) correspond to logical constants. Computation operations are described as compositions of base logic functions. Such setting traditionally disposes one to apply multiple-valued logics but Lukasiewicz logic and its enrichments weren’t thoroughly employed earlier. It allows evaluating efficiency of computing models against different criteria: power, performance, consumption etc.

For these purposes Lukasiewicz logic is represented as matrix L_n+1 – special algebraic system with universe E_n+1 [2]. The following results are obtained.

Theorem 1.
(i) Operations =, |+|, |-|, |x| are expressible in L_n+1.
(ii) Set of functions {|+|, |-|} forms base in certain clone which is maximal in L_n+1.
(iii) Set of functions OAL_n+1 = {=, |-|} forms base in L_n+1.

Corollary 1.1. Set of constants and functions of arithmetic OA_n+1 is complete in Post logic P_n+1.

Theorem 2.
(i) Operations (=), (+), (-), (x), Carry are expressible in L_n+1.
(ii) Set of functions {(+), (-), (x), Carry} forms base in certain proper subclone of L_n+1.
(iii) Set of functions MAL_n+1 = {(+), (-), Carry, max} (n>2) forms base in L_n+1.

Corollary 2.1. Set of constants and functions of arithmetic MA_n+1 is neither complete nor maximal in P_n+1 but becomes complete after enrichment by function max(x,y).

As a spin-off, the way to employ Lukasiewicz logic proof technique to find roots of polynomials over modulo ring Z_n is shown.

Some aspects of implementation of computer arithmetic are considered. In the majority of contemporary hardware platforms and programming environments MA_n+1 is implemented with n=2^q (usually q equals to 16, 32 or 64). However, functional incompleteness of this system leads to necessity of such inefficient operations as conditional branch. Important alternative is offered by multiple-valued arithmetic-logical units (MVALU) such as hardware implementation of overflow subtraction |-| by polymer conductors [6]. It has been proven that it is enough to implement this operation in order to build full-functional MVALU.

References

1. Evans T., Schwartz P.B. On Slupecki T-functions // J. Symbolic Logic. 1958. Vol. 23. P. 267-270.
2. Karpenko A.S. Lukasiewicz’s Logics and Prime Numbers. Moscow: Nauka, 2000. [In Russian]
3. Kovalyov S.P. Analysis models of computer arithmetic // Siberian Journal of Industrial Mathematics. 2003. V. 6, №3. P. 88-102. [In Russian]
4. Kovalyov S.P. Lukasiewicz logic as an architecture model of arithmetic // Siberian Journal of Industrial Mathematics. 2003. V. 6, №4. P. 32-50. [In Russian]
5. Liskov B.H., Zilles S.N. Specification techniques for data abstractions // IEEE Trans. on Software Engineering. 1975. SE-1, 1. P. 7-19.
6. Mills J.W. Polymer Processors. Indiana University, Computer Science Dept, Technical Report TR580. Indiana University, 2003.
7. Rosenberg I.G. Completeness properties of multiple-valued logic algebras // Computer Science and Multiple-Valued Logic. Amsterdam: North Holland, 1977. P. 144-186.
8. Voevodin V.V. Mapping computational problems to computer architecture // Computational Methods and Programming. 2000. V. 1. P. 37-44. [In Russian]

Mail to Webmaster alc9@math.nsc.ru

|Home Page| |English Part|

Go to Home