Simple translation

A simple translation (ST) is a relationship between two programming languages. It is a particular type of equivalence between languages. It was developed to formalize the notion of a minimization from one language to another. Simple translations can translate between languages when they are equipped with an underlying algebraic structure called a monoid which allows each program to be analyzed in terms of primitive words.

Definition

Intuitively, a language is a ST of another language if a translation table exists between those languages preserving certain properties. For each row, a translation table contains a single symbol from the source language in the left column and a finite sequence of symbols from the destination language in the right column. Use the translation table to convert from the source language to the destination language and back. If semantics are preserved during this process, then the destination language is a ST of the source language.

Formally,

Definition. A simple translation between alphabets A and B, relative to equivalences R and S, is an isomorphism between monoids <A|R> and <B|S>.

That is, if the monoids with different presentations are in-fact the same monoid, which we might call C, then we may simply translate A to B or vice versa using its translation table. The translation table is actually a pair of tables, one between A and C, and one between B and C, built from the generators of R and S respectively.

To unpack that definition, suppose we have language A with commands a₁, a₂, ... a_n and language B with commands b₁, b₂, ... b_m (note that neither A nor B must possess an infinite number of commands). A translation table from A to B looks like

(1)
A	B equivalent
a1	β1,1β1,2...β1,p1
a2	β2,1β2,2...β2,p2
...	...
an	βn,1βn,2...βn,pn

where β_i,j is one of b_k. A translation table from B to A looks like

(2)
B	A equivalent
b1	α1,1α1,2...α1,q1
b2	α2,1α2,2...α2,q2
...	...
bm	αm,1αm,2...αm,qm

where α_i,j is one of a_k. Notice that both sub-tables must exist; a translation table is a pair of sub-tables.

The main goal of constructing simple translations is to witness minimizations.

Definition. A minimization from A to B is a simple translation between A and B where B has fewer generators than A.

Techniques

A simple translation must preserve all semantics, which implies that the equivalences R and S must be extremely rich; in general, they could be uncomputable. However, we may take sub-relations R₀ and S₀ instead; these sub-relations may generate larger monoids which have higher rank, so reasoning with them will produce inequalities which bound the rank of <A|R> and <B|S>. In 2020, User:Orby used this technique to show several results about brainfuck variants:

Theorem. The rank of brainfuck is less than or equal to seven. (Orby, 2020)

Theorem. The rank of brainfuck without input/output is less than or equal to five. (Orby, 2020)

Theorem. The rank of Reversible Bitfuck is less than or equal to three. (Orby, 2020)

These theorems can be used constructively to synthesize languages with relatively small syntax. For example, the above theorem was used to construct Nanofuck.

Semantics of simple translation

Take a program consisting of a sequence symbols in A denoted by x₀. Translate that program to B using (1) to produce y. Translate y back to A using (2) to produce x₁. If, for an arbitrary initial state, x₀ halts if and only if x₁ halts and they produce equivalent final states, then B is a ST of A.

This is an extremely strong statement at first glance, since it seems to impose an extra semantic condition. However, note that if B is a ST of A, then B has implicit semantics defined by (2) in terms of A. This effectively provides a definition for B which may or may not match some other semantic interpretation. Under the implicit semantic interpretation, B is clearly Turing complete (TC) if and only if A is TC.

The idea of implicit semantics can be formalized too. Suppose that A is equipped with a homomorphism to some semantic domain S. The category ST(A,S) over that homomorphism is the category whose objects are languages and arrows are translation tables equipped with paths to A and therefore to S; alternatively, ST(A,S) is the path category on a path-connected graph of translation tables which includes A as a vertex. Every object of ST(A,S) can be interpreted in S; as such, either every object is Turing-complete or none are. This also, by the underlying definition of category requiring everything in sight to commute, requires all of the different translations of B in ST(A,S) to be equivalent in S.