A model of computation dealing with infinite alphabets is proposed. Th
is model is based on replacing the equality test by substitution. It a
ppears to be a natural generalization of the classical Rabin-Scott fin
ite-state automata and possesses many of their closure and decision pr
operties. Also, when restricted to finite alphabets the model is equiv
alent to finite-state automata.