Consider the language
$$L_{\times 2} = \big\{ x\bot y\bot z \mid x,y,z\in \{0,1\}, \#_0(x)=\#_0(y) \text{ and } |x|+|y|=z\big \}$$
(where $\#_0(x)$ denotes the number of zeros in $x$).
It is easy to decide $L_{\times 2}$ using a HAL machine — observe that the machine needs to keep track of two properties: the number of zeros in $x$ vs $y$ and the length of $x,y$ (vs $z$). It can push a 0 into the heap for every zero it sees in $x$ (and then later pop 0 for any zero seen in $y$); additionally it pushes 1 for any bit in $x,y$ (and later pops 1 for any bit of $z$). Since all the 1s are pushed down the heap, they don't interfere with the 0 count. The $\bot$ serves as a delimiter, and can be practically ignored.
Now, let $L = L_{\times 2}^R$, be the reverse language. That is,
$$ L = \big\{z\bot y \bot x \mid x,y,z\in \{0,1\}, \#_0(x)=\#_0(y) \text{ and } |x|+|y|=z\big \}$$
We will show that no HAL machine can decide $L$.
The intuition is the following. As above, the machine must keep track of both the length of $z$ and the number of zeros in $x,y$. However, in this case it need to track them simultaneously. This cannot be done via a heap. In more details, after reading $z$, the heap contains information about the length of $|x|+|y|$.
while reading $y$ the machine must also keep in the heap the number of zeros in $y$. However, this information cannot interfere with the information the heap already has on the length we expect $x$ to be. Very intuitively, either the information about the number of zeros will be "below" the information about the length of $x$, and then we cannot access it while reading $x$, or it is "above" that information, rendering the latter inaccessible, or the two information will be "mixed" and become meaningless.
More formally, we are going use some kind of a "pumping" argument. That is, we will take a very long input, and show that the "state" of the machine must repeat itself during processing that input, which will allow us to "replace" the input once the machine repeats its "state".
For the formal proof, we require a simplification of the structure of the HAL machine, namely, that it doesn't contain a "loop" of $\varepsilon$-transitions$^1$. With this assumption we can see that for every input symbol the machine processes, the content of the heap can increase/decrease by at most $c$ (for some large enough constant $c$).
Proof.
Assume $H$ decides $L$, and consider a long enough input (say, of length $4n$, thus $|x|=|y|=n$, $|z|=2n$, ignoring the $\bot$s hereinafter). To be concrete, fix $z,y$ and assume that $\#_0(y) = n/2$. Observe that there are ${n \choose n/2}$ different $x$'s such that $z\bot y \bot x \in L$.
Consider the heap's content immediately after processing $z\bot y$. It contains at most $3nc$ symbols (where each symbol is from a fixed alphabet $\Gamma$), by our assumption. However, there are ${n \choose n/2}$ different $x's$ that should be accepted (which is substantially larger than the amount of possible different contents for the heap, as this increases exponentially, while the different number of heaps increases polynomially, see below).
Take two inputs $x_1,x_2$ that should be accepted, so that the following holds:
- The prefix of length $n/2$ of $x_1$ has different number of zeros than the prefix of $x_2$ of the same length.
- By the time the machine reads a prefix of length $n/2$ of the $x$ part, the heap looks the same for both $x_1$ and $x_2$, and also, the machine is in the same state (this must happen for some $x_1,x_2$, for large enough $n$, as there are more than $2^{0.8n}$ different options$^2$ for $x_1,x_2$, and at most $(3.5cn)^{|\Gamma|}|Q|$ different options for heap content and state$^3$).
It is clear that the machine must accept the word $z\bot y \bot x_1^px_2^s$, where $x_1^p$ is a prefix of $x$ of length $n/2$ and $x_2^s$ is a suffix of $x_2$ of the same length. Note that the number of zeros in $x_1^px_2^s$ differs from the number of zeros in $x_1$ and $x_2$ (that is, from $\#_0(y)$), due to the way we chose $x_1$ and $x_2$, thus we reached a contradiction.
$^1$ Does this assumption damages generality? I don't think so, but this indeed requires a proof. If someone sees how to get around this extra assumption, I'd love to know.
$^2$ Let's fix $x_1$ so that it's prefix (of length $n/2$ has exactly $n/4$ zeros). Recall that using Stirling's approximation we know that $\log {n \choose k} \approx nH(k/n)$ where $H()$ is the Binary entropy funciton. Since $H(1/4) \approx 0.81$ we have ${n \choose n/4} > 2^{0.8n}$ for large enough $n$.
$^3$ Assuming alphabet $\Gamma$, there are $|\Gamma|^n$ different strings of length $n$, so if this was a stack we were screwed. However, pushing "01" into a heap is equivalent to pushing "10" - the heap stores only the sorted version of the content. The number of different sorted strings of size $n$ is ${n+1 \choose |\Gamma|-1}\approx n^{|\Gamma|}$, for a constant $|\Gamma|$.
