Formal definition of string-to-term substitution

Question

Forgive me if this question seems elementary. Let L be a nonempty alphabet. We have an intuitive notion of substituting words for letters in a word. For example, substituting 'cd' for 'b' in the word 'bab' results in 'cdacd'. And, in the word 'aad', the substitution would result in 'aad'. We also have a notion of simultaneous substitution. For example, substituting 'bb' for 'a' and simultaneously 'aa' for 'b' in the word 'ab' results in 'bbaa'. Now I can set up the question. How is simultaneous substitution formally defined? More precisely, if some set of letters S is mapped to a set of words W, how is the simultaneous substitution of S to W defined for all words over L? I have looked on the internet, but haven't found a formal definition.

Answer 1

Let $f$ be the given function from some set $S$ of letters to a set $W$ of words. The "substitute according to $f$" function $g$ from words to words can be defined by recursion on the length of the input words as follows:

$g$ maps the empty word to itself.

If $w$ is $u^\frown x$, where $u$ is a word and $x$ is a letter in $S$ (and ${}^\frown$ means concatenation), then $g(w)=g(u)^\frown f(x)$.

If $w$ is $u^\frown x$, where $u$ is a word and $x$ is a letter not in $S$, then $g(w)=g(u)^\frown x$.

Answer 2

You can see : J.L.Bell & Moshe Machover, A Course in Mathematical Logic (1977) : Ch.2 First-order Logic, para 3 : Substitution (pag.57-67) there is a detailed treatment of substitution and simultaneous substitution for first-order language.

I think that the basic machinery is available.

Answer 3

Let $A$ be an alphabet and let $A^*$ be the free monoid on $A$ (that is, the set of words on the alphabet $A$). Let now $f: A \to B^*$ be a function. Then $f$ can be extended in a unique way to a monoid morphism from $A^*$ to $B^*$.

Example 1. Let $A = \{a,b,d\}$ and $B = \{a,c,d\}$. Let $f(a) = a$, $f(b) = cd$ and $f(d)=d$. Then $f(bab) = cdacd$, $f(aad) = aad$.

Example 2. Let $A = B = \{a,b\}$ and $f(a) = bb$, $f(b) = aa$. Then $f(ab) = bbaa$.

This is a standard notion in automata theory.