<p>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.</p>

<p>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.</p>

<p>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 &amp; \text{if $M(y)$ halts in fewer than $n$ steps of simulation}\\\\
0 &amp; \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.</p>

<p>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$.</p>

<p>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 <em>can</em> compute a corresponding canonical code $Z(A)$. See my blog post on <a href="http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/">juggling double exponentials</a> where I explicitly construct $Z$.</p>

<p>We could also ask whether it is possible to make Turing machines somehow more powerful so that we <em>can</em> 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 <a href="http://arxiv.org/pdf/math/9808093.pdf">infinite-time Turing machines</a> (ITTM), then canonical codes for maps $\mathtt{string} \to \mathtt{string}$ <em>are</em> computable. The ITTM's therefore <em>can</em> 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 <a href="http://math.andrej.com/2011/06/15/constructive-gem-an-injection-from-baire-space-to-natural-numbers/">embedding $\mathbb{N}^{\mathbb{N}}$ into $\mathbb{N}$</a> for details.</p>

<p>P.S. Apologies for blatant self-propaganda.</p>

CC BY-SA 3.0
2013-08-26T10:32:35.480Z
2013-08-26T10:32:35.480Z
Andrej Bauer
<p>As Igor Shinkar explains, no Turing-complete language can satisfy your criteria.  This sharply limits the expressibility of any such language.</p>

<p>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.)</p>

<p>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.)</p>

CC BY-SA 3.0
2013-08-25T05:59:34.047Z
2013-08-25T05:59:34.047Z
D.W.
<p>Is there any programming language in which any equivalent program has a unique normal representation, and that normal representation is decidable? </p>

<p>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).</p>

<p>Finally, that language should be able to encode boolean logic.</p>

<p>Is there such a language?</p>

CC BY-SA 3.0
2013-08-25T03:38:19.680Z
wouldn't that allow us to solve the halting problem?
Igor Shinkar
CC BY-SA 3.0
2013-08-25T03:48:36.583Z
@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
CC BY-SA 3.0
2013-08-25T06:01:06.897Z
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.
CC BY-SA 3.0
2013-08-25T06:12:30.640Z
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
CC BY-SA 3.0
2013-08-25T06:24:36.170Z
To add to my previous comment, I think propositional logic is powerful enough to express CFGs so your requirements can not be met.
Shitikanth
CC BY-SA 3.0
2013-08-25T08:51:13.420Z
I don't think CFGs are powerful enough to express it. Anyway this requirement shouldn't be taken literarily: it is just there to exclude languages that certainly can't be used to express any useful computation, such as regex. COQ, for example, is not turing-complete, yet can express many useful computations such as solving algebraic expressions. This way, I want to find a language that is not turing complete yet useful enough to be used in a practical sense. There must be another category of languages fitting that idea, even though I'm not sure how to formalize that.
MaiaVictor
CC BY-SA 3.0
2013-08-26T18:12:57.443Z
@Shitikanth, propositional logic can only encode the skeletal structure of a control flow graph, not the labels, and not the semantics of the labels. Program equivalence in most standard senses, will have to consider the semantics of labels.
Vijay D
CC BY-SA 3.0
2013-08-27T17:27:42.693Z
think there is a nearby question here that I was just coincidentally thinking of asking. ie, what are any "weak" "programming" "languages" (broadly construed) that are not TM complete yet still are decidable...?
vzn
CC BY-SA 3.0
2014-05-08T21:42:25.060Z
BTW, even a programing language that expresses only primitive recursion is out: Coq and other total programing languages are much to expressive to satisfy your above criterion.
cody
<ds.algorithms><reference-request><pl.programming-languages><computability>
Is there any programming language in which any equivalent program has a unique, decidable normal representation?
MaiaVictor
# Is there any programming language in which any equivalent program has a unique, decidable normal representation?

(Asked by: username_0 on 2013-08-25)

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?

**Tags:** ds.algorithms, reference-request, pl.programming-languages, computability

> **Comments:**
> **username_1**: wouldn't that allow us to solve the halting problem?  
> **username_0**: @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!  
> **username_2**: 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$)?  
> **username_3**: 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.  
> **username_3**: To add to my previous comment, I think propositional logic is powerful enough to express CFGs so your requirements can not be met.  
> **username_0**: I don't think CFGs are powerful enough to express it. Anyway this requirement shouldn't be taken literarily: it is just there to exclude languages that certainly can't be used to express any useful computation, such as regex. COQ, for example, is not turing-complete, yet can express many useful computations such as solving algebraic expressions. This way, I want to find a language that is not turing complete yet useful enough to be used in a practical sense. There must be another category of languages fitting that idea, even though I'm not sure how to formalize that.  
> **username_4**: @username_3, propositional logic can only encode the skeletal structure of a control flow graph, not the labels, and not the semantics of the labels. Program equivalence in most standard senses, will have to consider the semantics of labels.  
> **username_5**: think there is a nearby question here that I was just coincidentally thinking of asking. ie, what are any "weak" "programming" "languages" (broadly construed) that are not TM complete yet still are decidable...?  
> **username_6**: BTW, even a programing language that expresses only primitive recursion is out: Coq and other total programing languages are much to expressive to satisfy your above criterion.  

---

## 2 answers

### Answer by username_7 on 2013-08-26. Score: 8

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](http://math.andrej.com/2009/10/12/constructive-gem-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](http://arxiv.org/pdf/math/9808093.pdf) (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}$](http://math.andrej.com/2011/06/15/constructive-gem-an-injection-from-baire-space-to-natural-numbers/) for details.

P.S. Apologies for blatant self-propaganda.


---

### Answer by username_2 on 2013-08-25. Score: 2

As username_1 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.)


---

