[XBUP] XBUP - Extensible Binary Universal Protocol

» Concepts » Protocol Formalisation

Formal: Number's Encoding

This document is part of the eXtensible Binary Universal Protocol project documentation. Provides description of the used types of encoding and development of their formal approval.

SLRUB Encoding

As the basic encoding of the natural numbers for the protocol is used the SLRUB encoding. It is a variant of gamma encoding, so far known as recursive unary-binary encoding, resulting from applying the requirements of the characteristics of the code. The emergence of encoding is described in the number's encoding document. With the extension of the referred argumentation it should be possible to formalize this encoding as the most appropriate option technique of the natural numbers representation.

Formalization of the Conditions

Following requirements which must complied for the proposed encoding have been established. …

Specified requirements:

Use of the Unlimited large numbers has been implemented in several programming languages and their main disadvantage is the greater intensity on the computing performance, but in normal cases it may be possible to use the protocol limited to standard ranges of values. It is worth mentioning that there can be no real encoded decimal numbers with the never-ending fraction, because we can only store final memory space. It is possible to store such…

Encoding Formalization

.

UBReal Encoding

It is easy to show that each of the final binary development corresponds exactly to one code. Evidence in the opposite direction is similar.

Statement: To any number with a final binary development there corresponds exactly one code in the UBReal encoding. The statement is valid in case that that the same is true for UBInteger encoding (without giving any evidence)

Argumentation: (contradiction) Assume that there are two different forms of the number corresponding to UBReal code. Then these codes differ:

a) In the Base value, or both: All bits of the Value must be present in the binary code of the value Base. Then, on the assumption that the encoding UBInteger encoding meets the same condition implies the equality of the Base code - contradiction

b) In the value of Mantissa: The binary code is a sequence of bits of the Value which ends by bit 1 (invisible one) and all the lower bits has value 0. If the value has a different value of Mantissa, the bit has position at the indentation bit of the value which is different in both the entry numbers - contradiction.

The list of resources, literature and relevant links:

Church Thesis - http://en.wikipedia.org/wiki/Church_thesis
Turing Machine - http://en.wikipedia.org/wiki/Turing_machine