Substitution, Unification and Term Rewriting

Unification is the basis of term rewriting system, and unification algorithms is the heart of the computation model of logic programs.

Term:

terms are expressions which can be obtained from constant symbols, variables and function symbols. Constant symbols are the 0-ary functions, so no special syntactic class is needed for them.

• Function symbols: one that has no other property than its name and arity
• Terms that do not contain free variables are known as ground terms
• A ground term of a formal system is a term that does not contain any free variables;
• free variable: y is free variable in $\forall x \in X \bullet (x+y) > 0$
• bound variable: x is bound variable in $\forall x \in X \bullet (x+y) > 0$
• Hence $\forall x \in X \bullet (x+y) > 0$ is not a ground term, but $\forall x \in X \bullet x > 0$ is a ground term
• x and y are variables, and f is a binary function symbol, then $f(x,y)$ is a term

Arity - the number of arguments or operands the functions or operation accepts. For example, the arity of $f(x)=x+1$ is 1; the arity of $f = 3$ is 0; the arity of $f(x,y,z) = x + y + z$ is 3.

• 0-ary function or operation: (arity == 0) constant symbols
• unary function or operation: (arity == 1) such as $f(x) = x * 2$, (unary operator) $-x$
• binary function or operation: (arity == 2) such as $f(x,y) = x + y$
• ternary function or operation: (arity == 3)

Signature:

A signature $\Sigma$ is a set of function symbols, where each $f \in \Sigma$ is associated with a non-negative integer n, the arity of $f$. $\Sigma^{0}$ denotes a set of constant symbols, while $\Sigma^{n}$ denotes a set of n-ary function symbols.

• For example, group $\Sigma_G := \{e, i, f \}$ where e is 0-ary, i is 1-ary, and f is 2-ary
• For example, a set of non-negative integers. e for smallest non-negative integer, i denotes the successor function $succ(x) = x + 1$, and f denotes the addition function $f(x,y) = x + y$

Substitution:

Substitution is a syntactic transformation on strings of symbols of a formal language

• a substitution is a finite set of the form $$\theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$ , where 
• $v_i$: distinct variables; 
• $t_i$: terms with $t_i \ne v_i$;
• $v_i \mapsto t_i$: binding

• Substitution application:  $E \theta$
• E - expression
• $\theta$ - substitution
• Simultaneously replacing each occurrence of $v_i$ in E with $t_i$
• For example, $E = p(x,y,f(a))$, $\theta = \{x \mapsto b, y \mapsto x\}$, $E \theta = p(b,x,f(a))$.
  

• Substitution Composition
• Two substitutions:  $$\theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$ $$\sigma =  \{u_1 \mapsto s_1, ..., u_n \mapsto s_n \}$$ $$\theta \sigma =  \{v_1 \mapsto t_1 \sigma, ..., v_n \mapsto t_n \sigma,  u_1 \mapsto s_1, ..., u_n \mapsto s_n\}$$
• For example, $\theta = \{x \mapsto f(y), y \mapsto z\}$, $\sigma = \{x \mapsto a, y \mapsto b, z \mapsto y\}$, $\theta \sigma = \{x \mapsto f(b), z \mapsto y\}$

• Empty Substitution $\varepsilon$
• Renaming substitution
• $\theta =  \{x_1 \mapsto y_1, ..., x_n \mapsto y_n \}$ is a renaming substitution if $y_i$ are distinct variables

• More general substitution (MGS)
• a substitution $\theta$ is more general than a substitution $\sigma$, written $\theta \leq \sigma$, iff there exists a substitution $\lambda$ that $$\theta \lambda = \sigma$$

Abstract Reduction System:

• An abstract reduction system is a pair $(A, \to)$, where the reduction $\to$ is a binary relation on the set A, i.e. $\to \subseteq A \times A$. Written $a \to b$, instead of $(a,b) \in \to$
• Program evaluation: $a0 \to a1 \to ...$. Starting from the initial program a0, and try to reach a normal formal
• Normal formal is the program which can not be reducible
• Let $\Sigma$ be a signature and $V$ a countably infinite set of variables disjoint from $\Sigma$. A $\Sigma$-identity is a pair $(s,t) \in T(\Sigma, V) \times T(\Sigma, V)$. Identities will be written as $s \approx t$
• reduction relation $\to_E$, where E is a set of $\Sigma$-identity
  

Unification:

Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal. Unification is widely used in automated reasoning, logic programming and programming language type system implementation

• Unification is the process of solving the satisfiability problem: given $E$, $s$ and $t$, find a substitution $\theta$ such that $\theta s \approx_E \theta t$
• For special case, where $E=\emptyset$, this case of unification is called syntactic unification, because the unification aims to find a $\theta$ such that $\theta s = \theta t$ i.e. $\theta s$ and $\theta t$ are syntactically identical.
• If $E \neq \emptyset$, this is referred to semantic unification
• Unifier of Expressions: a substitution $\theta$ is a unifier of expressions E and F iff $$\theta E = \theta F$$
• For example, $E = f(x,b,g(z)), F = f(f(y),y,g(u))$. Then $\theta = \{x \mapsto f(b), y \mapsto b, z \mapsto u\}$ is a unifier of E and F since $$\theta E = f(f(b),b,g(u))$$ $$\theta F = f(f(b),b,g(u))$$

• Unifier is a solution to the equation by substitution. Find a substitution to make two expressions E and F are equal and this substitution is a solution to this equation, named unifier.

Unification in Prolog:

Unification in Perl: