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?
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.)
