Is there any programming language in which any equivalent program has a unique, decidable normal representation?

Is there any programming language in which any equivalent program has a unique normal representation, and that normal representation is decidable?

Is other words, suppose A and B are programs written on that hypothetic language. Suppose, too, that for any input x, A(x) = B(x) - that is, those programs are equivalent. There should, then, be an algorithm Z for which Z(A) = Z(B).

Finally, that language should be able to encode boolean logic.

Is there such a language?

• wouldn't that allow us to solve the halting problem? – Igor Shinkar Aug 25 '13 at 3:38
• @IgorShinkar No, because I didn't state it is a turing complete language! But indeed, if it is a language "useful enough" to be used as a practical programming language, then we would effectively "get rid" of the halting program in our lives! – MaiaVictor Aug 25 '13 at 3:48
• I think you should edit the question to specify more carefully what you mean by "able to encode boolean logic". Do you include quantifiers ($\forall,\exists$) and propositions with multiple levels of nested quantifiers? Or only boolean expressions generated by input variables ($v_1,\dots,v_n$), logical and ($\land$), logical or ($\lor$), and negation ($\neg$)? – D.W. Aug 25 '13 at 6:01
• Regular expressions is such a "programming language". Given a regular expression you can find a unique minimal DFA that accepts the words matching the regular expression and you can use this to check if two regular expressions are equivalent. On the other hand, testing the equivalence of two context free grammars is undecidable. So any such programming language would not have the power to write parsers for a general CFG. – Shitikanth Aug 25 '13 at 6:12
• To add to my previous comment, I think propositional logic is powerful enough to express CFGs so your requirements can not be met. – Shitikanth Aug 25 '13 at 6:24

What you are asking for does not exist for a general-purpose programming language (by which we mean that the language can simulate Turing machines, and that Turing machines can simulate the language). Let me first recall the proof, and then turn the question around to discover something interesting.

We have to make your question just a bit more precise. Let us suppose that when you speak of inputs and outputs you mean strings, and that your programs are total (defined on all inputs). Now suppose there were an algorithm $Z$ which maps programs to programs (that is, strings to strings) such that, given any two valid programs $A$ and $B$ which map strings to strings, $Z(A)$ and $Z(B)$ are defined and $$Z(A) = Z(B) \iff \forall x \in \mathtt{string} . A(x) = B(x).$$ Notice that I did not even require that $Z(A)$ be a program equivalent to $A$, it can be any string whatsoever, the important thing is that it maps $A$ and $B$ to the same string if, and only if, they represent equivalent programs. We can now solve the halting oracle as follows.

Let $A$ be a program which always outputs the string 0, i.e., $A(x) = 0$ for all $x \in \mathtt{string}$, and let $x_0 = Z(A)$. Consider any Turing machine $M$ and an input $y$. Because we assumed our language is Turing-complete, from a description of $M$ and a given input $y$ we can construct a program $B_{M,y}$, which computes as $$B_{M,y}(n) = \begin{cases} 1 & \text{if M(y) halts in fewer than n steps of simulation}\\\\ 0 & \text{otherwise} \end{cases}$$ Notice that $B_M$ and $A$ are equivalent if, and only if, $M(y)$ diverges. But now we can decide whether $M(y)$ halts: if $Z(B_{M,y}) = x_0$ then $M(y)$ does not halt, otherwise it halts.

The above argument shows that programs of type $\mathtt{string} \to \mathtt{string}$ do not have canonical codes. How about other kinds of programs? Well, in some cases we obviously can produce canonical codes. For instance, a program $A$ of type $\mathtt{bool} \to \mathtt{bool}$ can be represnted canonically by the list $[A(\mathtt{false}), A(\mathtt{true})]$, from which the corresponding $Z$ can be easily constructed. If we replace $\mathbb{bool}$ with some other finite datatype, we also obtain canonical codes by simply listing the values of $A$.

But did you know that there are canonical codes for programs of type $(\mathtt{nat} \to \mathtt{bool}) \to \mathtt{bool}$? That is, given a program $A$ which takes as input infinite binary streams and outputs a bit, we can compute a corresponding canonical code $Z(A)$. See my blog post on juggling double exponentials where I explicitly construct $Z$.

We could also ask whether it is possible to make Turing machines somehow more powerful so that we can compute canonical code, and thereby solve the Halting problem. Well, adding an oracle will not help because exactly the same reasoning goes through. But we use infinite-time Turing machines (ITTM), then canonical codes for maps $\mathtt{string} \to \mathtt{string}$ are computable. The ITTM's therefore can solve the Halting problem for ordinary Turing machines, but they still cannot solve their own halting problem (which is not reducible to comparison of two functions mathtt{string} \to \mathtt{string}$). See my paper on embedding$\mathbb{N}^{\mathbb{N}}$into$\mathbb{N}\$ for details.

P.S. Apologies for blatant self-propaganda.

As Igor Shinkar explains, no Turing-complete language can satisfy your criteria. This sharply limits the expressibility of any such language.

On the other hand, regular expressions would be one example of a language that does satisfy your condition, since it is decidable to find a minimal regular expression (or minimal DFA) that is equivalent to a given regexp. (However, there is no guarantee that the normal form can be computed efficiently; in the worst case, it might take exponential time.)

Another example would be boolean circuits: it is decidable to find a minimal boolean circuit that is equivalent to a given circuit. (However, the normal form cannot be computed efficiently.)

For any programming language in which the programs are computably enumerable,

"any equivalent program has a unique normal representation,
and that normal representation is decidable"

is equivalent to

"the equivalence of programs is decidable"

.

(Proof: the normal representation is the first equivalent program.)