Tuesday, May 19, 2020

Basic Balanced Ternary Arithmetic.

This page was last edited on July 23rd, 2022.

This column builds on A prior column on "Just in Time Subtraction"

What is Balanced Ternary Arithmetic?

Well, it is a modification of standard base three arithmetic.

OK, what is base three (ternary) arithmetic?

Base three arithmetic is like base 10, except that we only have digits 0, 1, 2 instead of 0 through 9. This means that counting has to carry to the next column after your digits get bigger than two, instead of when they get bigger than nine. In base 10, an integer has a "one's column", a "ten's column", a "hundred's column", and so on. In base 3, an integer has a "one's column", "a "three's column, a "nine's column", and so on.

On to balanced ternary

Balanced ternary is almost exactly like regular ternary arithmetic, except that instead of digits being 0, 1, and 2, they are +1, 0, and -1. This is awkward to write, so I'll follow a common convention and use "+", "0", and "-" as the digits.
Terminology aside: In binary, a digit is referred to as a "bit", short for Binary digiIT. In ternary (or balanced ternary) a digit is called a "trit", short for TeRnary digIT.

Lets try counting:

 
Base 10, Binary, Ternary,  Balanced Ternary

      0,      0,       0,        0
      1,      1,       1,        +
      2,     10,       2,       +-
      3,     11,      10,       +0
      4,    100,      11,       ++
      5,    101,      12,      +--
      6,    110,      20,      +-0
      7,    111,      21,      +-+
      8,   1000,      22,      +0-
      9,   1001,     100,      +00
     10,   1010,     101,      +0+
     11,   1011,     102,      ++-
     12,   1100,     110,      ++0
     13,   1101,     111,      +++
     14,   1110,     112,     +---
     15,   1111,     120,     +--0
     16,  10000,     121,     +--+
     17,  10001,     122,     +-+-
     18,  10010,     200,     +-+0
      .       .        .         .
      .       .        .         .
      .       .        .         .
I imagine that many of my readers are looking at that last column and cringing. No doubt many feel that it is ugly, complex, non-intuitive, etc.. And, I'm sure some question why anyone, in their right mind, would want to compute in balanced ternary.

I don't think anyone would actually want to compute in it. But it, like binary, is great for COMPUTERS to compute with. Balanced ternary does have many nice properties. The famous computer scientist/mathematician Donald Knuth described it as the most elegant of the number bases. For example, in the traditional number bases you have a negative number you mark it with a negative sign ("-6", for example). This convention is called "signed magnitude form". In binary, this convention leads to more complexity in the logic than some other choices. Other representations include "two's complement binary" and "One's complement binary" representations. You don't need to know what these are for this discussion, and you can Google them if you want details. But with balanced ternary you don't need anything other than the number, since the left most non-zero trit is not only a digit, but is also the sign of the number, so we don't need anything extra. As Knuth points out, rounding and truncating are EXACTLY the same in balanced ternary. This is true even to the left of the ternary point if you understand "truncating" as "make all digits to the right be zeros". So there is no complex code needed to deal with rounding. Negating a number is just "flipping the signs all the way through. For example 6 is +0-, and negative six is just -0+. For arithmetic logic units balanced ternary has numerous advantages. For example, the multiplication times table has *no* carries.



      Balanced Ternary
Multiplication        Addition          

* | - 0 +            + |  -   0   +
--.------            --.-----------
- | + 0 -            - | +-   -   0
0 | 0 0 0            0 |  -   0   +
+ | - 0 +            + |  0   +  -+
  0 carries            2 carries

      Contrast with Ternary

* | 0  1  2          + |  0  1  2
--.--------          --.---------
0 | 0  0  0          0 |  0  0  0
1 | 0  1  2          1 |  0  1 10
2 | 0  2 11          2 |  0 10 11
  1 carry              3 carries


Technical/historical aside: Most modern machines using binary use two's compliment arithmetic for signed numbers, because it is straight forward to implement, intuitive, and easy to describe. Some computers (Univac mainframes, CRAY super computers and some others) use one's complement arithmetic instead. As an example of disadvantages of one's complement include that it has both a positive and a negative zero, and it can count down one more than it can count up. The arithmetic unit has to do an "End around carry or borrow" in many cases to make the arithmetic work. An obvious question is why anyone would want to use representation that has those bad properties. I'm told that the answer is that they didn't really want to, but IBM had patents on two's compliment arithmetic, which effectively prevented others from using it. So why is it that modern machines are almost all using two's complement? Simple, the patents expired. END ASIDE

Why do computers, almost universally, use binary, instead of ternary or balanced ternary? Slamming a current level all the way on, or all the way off, is a good match for a transistor, or even a vacuum tube. Trying to exactly hit any intermediate level exactly leads to much more complexity. Transistors devices that can drive a line positive, negative, and zero are much more complex than a single transistor. Why would Russian's Setsun series computers use balanced ternary anyway, given the engineering issue above? I'm told that they didn't want to. But after the US invented the transistor, the military uses were clear... you could (for example) make smaller, lighter, more reliable missile guidance systems. So the US restricted the export of transistors. So in Russia, Computer Science folk at Universities had a very hard time getting access to them. [Of course, they did get them, but they were big budget items due to the difficulty of getting the transistors.] Therefore they were not cost effective for computer logic units. So, what is an engineer to do? You can do logic with things other than transistors. Vacuum tubes work, but are unreliable and relatively short lived, easily broken, quite expensive, and relatively large (100's of times larger).

You can reliably tell the difference between current in one direction, current in the other direction, or no current at all. But, if you wind coils on a metal rod or donut, you can use it for logic. A perfect match to balanced ternary. And diodes were available.


Example of two coils on a metalic rod:

Opposite directions  In the same direction.

  | - 0 +              | - 0 +
--.------            --.-------
- | 0 - 0            - | - 0 0
0 | - 0 +            0 | - 0 +
+ | 0 + 0            + | 0 0 +

You can combine signals directly by different winding arrangement and organizations, and while the russians didn't have easy access to transistors, they had access to diodes (which had been around at least since the old crystal radios)
You can use many many windings on one core, if the windings have the same orientation this is an "OR" gate, with however many inputs as you want. You can make a "NOT" of a signal by reversing the direction of the winding. (You get zero if it is zero, and the opposite direction otherwise. Just like "NOT AND" and "NOT OR" can generate any other binary function, there are "complete" functions for three valued logic. And, there are a lot more than two of them, leaving a lot of room for creative design. You can send the output to other logic gates also, and assemble much more complex logic units.

In a ternary, or balanced ternary, computer one has to communicate with humans, and binary computers. So code or hardware needs to be able to convert balanced ternary (or ternary) numbers to base ten for people, and two or eight for binary computers. There is an method discussed in Just in Time Subtraction I and Just in Time Subtraction II that provides fast divides by any power of the base plus or minus 1. In decimal, that gives you divides and modulo by 10-1 = 9) and 10+1 = 11, 100-1 = 99 and 100+1 = 101... which doesn't seem all that useful. But in base three (balanced or not) it gives fast divides (and modulo functions) by 3-1 = 2, 3+1 = 4, 9-1 = 8, 9+1 = 10, ... Both 2 and 10 are exactly what we need to convert numbers for use by binary computers and humans.


Navigation:

next post | previous post

Friday, May 15, 2020

Logic: Axioms, Single axioms.

(Last edited May 11th, 2022 -JH)

Axioms

You have to start somewhere when dealing with a new area of math or logic. In the western tradition, this is often done with axioms (αξιώματα, classical Greek: worthy, later Greek: fitting). Axioms are, theoretically, statements about the topic that are so obvious that they need no proof. And (hopefully) they allow you to prove ANY valid statement in the system in question, and nothing that is not valid in the system.

Euclid (Εὐκλείδης) of Alexandria pioneered this with geometry around 300 BC, or so. He wrote a series of books on it that are still in print, and have been translated in quite a few languages. David Hilbert formalized axiomatic proofs for logic ("Hilbert style proofs"), and once you have logic you can define all mathematics subject to the usual arguments of exactly which axioms and definitions to use. [As shown by Russell and Whitehead in "Principia Mathmatica"] Computer theorem provers are usually working in axiomatic systems of one sort or another.

Basics:

Notation: I give axioms and theorems as axiom in Łukasiewicz notation, often called Polish Notation, a slash ("/"), and then the infix notation that I suspect more of my readers are more used to. For example the axiom of Modus Ponens is:
CpCCpqq / p -> ((p->q) -> q)

An axiomatic basis for a system has a number of parts. There are rules of inference, and axioms.

The default rules of inference are usually Modus Ponens (MP), and Uniform Substitution (US). If you have those two, you provably also have a rule called Condensed Detachment (CD) that is easier to use for computers and almost subsumes both.

Modus Ponens says that if you have a theorem of the form
   Cpq / p -> q
and you have p, then you also have q.
This is also called "Detachment".
Uniform Substitution says that you can substitute anything well formed in for a variable in a theorem as long as you substitute the exact same thing for each and every occurrence of it. (I'm really oversimplifying here, sometimes one set of rules and an axiom basis can be the same as another set of rules and other axioms.) There are also other rules used in specialized study of (usually unusual) systems.

As an example, using the usual rules, the axioms for the (implicational fragment of) positive propositional logic are often given as:

S:  CCpCqrCCpqCpr   /    (p->(q->r))->((p->q)->(p->r))
K:  CpCqp           /     p->(q->p)

There is, in general, no "one true axiomatic basis" of a logic system. A logic can have MANY different collections of axioms that describe exactly some given system, and nothing else. These collections are called an axiomatic bases for the logic systems. For example, the collection of everything the logic can prove is an axiomatic basis, albeit one with a countable infinity of axioms. A convention that cuts the universe of bases down quite a bit is to only worry about bases that have no "redundant" axioms.

A redundant axiom is one that can be proven by the other axioms. If it is redundant, why have it at all? Removing it means one less case to worry about when doing proofs about the system.

*** EDITING NOTE. Some text has vanished here, probably an editing error.
*** I'm working to find the block of text that went here.***
-JH

CCCpqrCsCCqCrtCqt / ((p→q)→r)→(s→((q→(r→ t))→(q→t)))

(This is from Carew A. Meredith, and it is a shortest single axiom for HI (The implicational fragment of the intuitionist logic] system. (see below)

Another basis for this logic that is quite common is:


B: CCpqCCrpCrq  / (p->q)->((r->p)->(r->q))
C: CCpCqrCqCpr  / (p->(q->r))->(q->(p->r))
K: CpCqp        /  p->(q->p)
W: CCpCpqCpq    / (p->(p->q))->(p->q)

If there are two different axiomatic bases for the same logic, how do know that they are the same? First some terminology: If a logic A can be described without redundancy by some axiom set (B) that is the A set plus some axioms, that A is called a sub logic of B, and B is called an extension of A. If you have two axiom sets, A and B, that allegedly are axioms for the same logic, they each must be able to prove everything in the system. That means that each should be able to prove the other. If axiom set A can prove a set B, then B is at least a sublogic of A, or possibly is A. If B can prove A, A is at least a sublogic of B or possibly is B. If they can each prove the other, then we know that they are at least sub logics of each other, and therefor that must be the same logic. If there is a known basis for a system, another alleged basis is the same system if you can find proofs both ways between the bases. Note that this is easier said than done. Such proofs can be very difficult to find and there are lots of bases for some logics that are suspected to be an axiomatic basis for a specific logic but have not been proven or disproven for fifty or more years.


OK, now that all that is out of the way, we can go on to talk about properties of axiomatic bases. An obvious observation is that some axiomatic basis for the same logic have different numbers of axioms. And if one knows this, an obvious question to ask is whether or not a system has a basis that has only ONE axiom.
In a basis that has only one axiom the axiom is called a "Single Axiom". Like any other basis, it can prove all the theorems of the system, and nothing else. And if you have a collection of single axioms, you can ask which is the shortest. This is called *a* shortest single axiom, since there may be many of that shortest size. As an example, the system called BCI has 80 known shortest single axioms, and it is known that no shorter ones exist, and that there are a small number of candidates of that size that no one knows whether or not they are single axioms, and they've been around for around 40 or so years without anyone finding a proof or disproof of their status.

[TODO: Put in the citations to the actual articles and dates not from memory] A good question at this point is what it takes for a logic to have a single axiom. The first steps in answering that were taken by Tarski who discovered in 1925 or so, and published in 1930 or so, that there were two different sets of two theorems (one given in the text, one in a footnote) that insured that if your system had them, your system also had a single axiom. Although Tarski distributed the proof privately, it never made it to print. It was effectively lost until (1980?) when Adrian Rezus generated a proof based on Lambda Calculus and Combinators it also expanded the number of different logic systems that could proven to have single axioms. This was a constructive proof, and it produced famously long axioms. In (2008??) I produced a proof based on just the logic generally available in Tarski's time, of yet another set of theorems that insured your system had a single axiom. It was also a constructive proof, and while the axioms generated were smaller than Rezus' paper generated, they were HUGH. I was following an approach pioneered by Dr. Dolph Ulrich. He apparently proved the footnote pair of axioms from Tarski's paper... and presented it at a conference that never had the proceedings with his paper published. I was also able to weaken one of the axioms in the set (maintaining the property) Tarski had in the set in the footnotes of his paper. Over the past few years, I've generated several other such pairs of theorems. I have a growing collection of pairs of theorems that work. So far my crowning achievement has been proving that if your logic has the the pair of axioms K: (p -> (q -> p)) and C: ((p -> (q -> r)) -> (q -> (p -> r)) in your system insures that it has a single axiom. There are some other pairs whos presence that (constructively) insure that a single axiom exists.


But, alas, nobody has has been able to produce, with such constructions, anything as short as the known single axiom bases. For one popular logic, BCI, The shortest single axioms are of length 19 (in Polish notation). Rezus's single axiom is about 93 symbols long My constructions are some 50 symbols long. This is a very very large gap. Those of us working in the area would welcome some construction from the axioms that was in the ballpark of the size of known shortest single axioms for the system.


Navigation:

next post |previous post