Definitions

A predicate-augmented finite state transducer (pfst) M is a tuple $(Q,\Sigma,\Pi,E,S,F)$ with Q a finite set of states, $\Sigma$ a set of symbols, $\Pi$ a set of predicates over $\Sigma$. As before, S and F are sets of start states and final states respectively. E is a finite set $Q\times (\Pi\cup\{\epsilon\}) \times (\Pi\cup\{\epsilon\}) \times Q \times \{0,1\}$. The final component of a transition is used to indicate identities. For all transitions (p,d,r,q,1) it must be the case that $d=r\not =\epsilon$.⁵

We define the function str from $\Pi\cup\{\epsilon\}$ to $2^{\Sigma^*}$.

$$\begin{array}{l} \mbox{str}(\epsilon) = \{\epsilon\}\\ \mbox{str}(\pi) = \{\sigma\in\Sigma\vert\pi(\sigma)\} \end{array}$$

If $\pi\in\Pi$ and $\mbox{str}(\pi)$ is a singleton set, then the transitions $(p,\pi,\pi,q,i)$ where $i\in\{0,1\}$ are equivalent.

The relation $\widehat{E} \subseteq Q \times \Sigma^*\times \Sigma^*\times Q$ is defined inductively.

1. for all p: $(p,\epsilon,\epsilon,p)\in\widehat{E}$.
2. for all $(p,\phi,\psi,q,0)\in E, x\in\mbox{str}(\phi), y\in\mbox{str}(\psi)$: $(p,x,y,q)\in\widehat{E}$.
3. for all $(p,\pi,\pi,q,1)\in E$, $x\in\mbox{str}(\pi)$: $(p,x,x,q)\in\widehat{E}$.
4. if (q₀,x₁,y₁,q₁) and (q₁,x₂,y₂,q) are both in $\widehat{E}$ then $(q_0,x_1x_2,y_1y_2,q)\in\widehat{E}$

The relation R(M) accepted by a pfst M is defined to be $\{(w_d,w_r)\vert q_s\in S, q_f\in F, (q_s,w_d,w_r,q_f)\in\widehat{E}\}$.