Problem 7 - Type Inference

Let $\boldsymbol{V}$ be a countably infinite set of variables, let $c$ ba a constant symbol, and let $f$ and $g$ be function symbols. We define the set $\boldsymbol{T}$ of terms as the least set closed under the following rules:

$$c\in \boldsymbol{T}$$

$$\forall x.(x\in \boldsymbol{V} \Rightarrow x\in \boldsymbol{T})$$

$$\forall t.(t\in \boldsymbol{T} \Rightarrow f(t)\int \boldsymbol{T})$$

$$\forall t_1,t_2.(t_1,t_2\in \boldsymbol{T} \Rightarrow g(t_1,t_2)\in \boldsymbol{T})$$

If variables $x_1, \dots, x_n$ are distinct from each other, $[t_1/x_1, \dots, t_n/x_n]t$ denotes the term obtained from $t$ by replacing all the occurrences of each $x_i\;(i=1,\dots,n)$ with $t_i$. We call $\theta=[t_1/x_1, \dots, t_n/x_n]$ a substitution. Answer the following questions.

1.

A substitution $\theta$ is called a unifier of $t_1$ and $t_2$ if it satisfies $\theta t_1=\theta t_2$. Check whether a unifier exists for the following each pair of terms. If so, answer a unifier.

• $g(x_1,f(c))$ and $g(f(x_2),x_1)$.
• $f(x_1)$ and $x_1$.

2.

A unifier $\theta$ of $t_1$ and $t_2$ is called a most general unifier of $t_1$ and $t_2$ if, for any unifier $\theta'$ of $t_1$ and $t_2$, there exists a substitution $\theta''$ such that $\forall t\in \boldsymbol{T}.(\theta''(\theta t)=\theta' t)$. Show that if both $\theta$ and $\theta'$ are most general unifiers of $t_1$ and $t_2$, then there is a substitution $[y_1/x_1, \dots, y_n/x_n]$ such that $\forall t.([y_1/x_1, \dots, y_n/x_n](\theta t)=\theta' t)$ and $y_1, \dots, y_n$ are mutually distinct variables. (In other words, show the uniqueness of the most general unifier up to renaming of variables.)

3.

Prove that if there is a unifier of $t_1$ and $t_2$, then there is also a most general unifier of $t_1$ and $t_2$.

1.

• $g(x_1,f(c))$ and $g(f(x_2),x_1)$:
  If $\theta = [f(c)/x_1, c/x_2]$, then $\theta g(x_1,f(c)) = \theta g(f(x_2),x_1)$ and $\theta$ is a unifier.
• $f(x_1)$ and $x_1$: Since $\forall t.(f(t)\neq t)$, there is no unifier for that pair of terms.