Are equalizers of regular functions always regular languages? (My guess is no because PCP, but...) Edit: I originally defined a regular function as a function computable by a Mealy machine, but Denis pointed out that that was a weaker model than what I was thinking of.

So to be more precise, by a "finite-state transducer" with input alphabet $A$ and output alphabet $B$, I mean a deterministic finite automaton over $(A \cup \{\epsilon\}) \times (B \cup \{\epsilon\})$. 

In particular, if both of the following hold for a transducer, then the transducer computes a function:


Every transition $(q, (x,y), q')$ is uniquely determined by $q$ and $x$;
If there is a transition $(q, (\epsilon, x), q')$ for any $x$, then there are no other transitions from state $q$.


Feel free to generalize or restrict as desired.



Definitions:

Let $L$ and $M$ be languages. A regular function $f:L\to M$ is a function computable by a finite-state transducer $A$ such that $(l,m)\in L(A)$ if and only if $l \in L$ and $m=f(L)\in M$. Note that it is decidable whether the relation computed by a given FST is a function. 

Define the equalizer $Eq(f,g)$ of two regular functions $f,g:A\to B$ as the set of all strings $x\in A$ such that $f(x)=g(x)=y$ for some $y\in B$.

"Theorem": The equalizer of two regular functions is regular.

"Proof": Since $f$ and $g$ are regular functions, they are also regular relations. In particular, we can take their intersection $h=f\cap g$. By definition, we have $(x,y)\in h$ if and only if $(x,y)\in f$ and $(x,y)\in g$; in function notation this becomes $(x,y)\in h$ iff $f(x)=g(x)=y$. By the closure properties of regular relations, it follows that $h$ is a regular relation; and since $f$ and $g$ are functions, $h$ is also a function.

Since $h$ is a regular relation, it is recognized by some finite state transducer $T$. We can take the input projection $\pi_1 T$, giving us a finite automaton which accepts a string $x$ if and only if $(x,y)\in h$ for some $y$. Let $E$ denote the language of the automaton $\pi_1 T$. By the definitions of $h$, $f$, and $g$, it follows that $x\in E$ if and only if $x\in A$ and $f(x)=g(x)=y$ for some $y\in B$. $\square$

But wait. Suppose $A$ is the set of all nonempty strings $\Sigma^+$ over some alphabet $\Sigma$, and suppose $f$ and $g$ are homomorphisms (every homomorphism is a regular function.) Then we can take the equalizer $P=Eq(f,g)$, which is regular by the above "theorem".

Now $P$ will be nonempty iff there is a string $x\in \Sigma^+$ such that $f(x)=g(x)$. In other words, $P$ encodes the Post correspondence problem (PCP) for $f$ and $g$. 

But since $P$ is regular, it is recognized by some finite automaton, and emptiness is decidable for finite automata. Since intersection and projection are computable constructions on transducers, we therefore have a method to solve PCP given the transducers for the homomorphisms $f$ and $g$. But this is impossible since PCP is undecidable. So where am I wrong?
If you use Mealy machines, it forces your functions to be length-preserving, and therefore you cannot encode PCP with them.

Your regularity theorem holds with length-preserving functions.
If you want to allow length-increasing functions (that you need for PCP), you need a more powerful transducer model, for which undecidability quickly kicks in.