<jupyter_start><jupyter_text>Unification This notebook implements the algorithm of Martelli and Montanari for the unification of terms.  Utility Functions<jupyter_code>import folParser as fp
def parseTerm(s):
    parser = fp.LogicParser(s)
    return parser.parse()
parseTerm('F(G(x),y)')<jupyter_output><empty_output><jupyter_text>The method $\texttt{apply}(t, \sigma)$ takes an object $t$ and a substitution $\sigma$ and computes the $t\sigma$, i.e. it applies the substitution $\sigma$ to $t$.  The object $t$ is either a term or a set of terms.  The substitution $\sigma$ is represented as a dictionary.  Assume that $\sigma = \bigl[ x_1 \mapsto t_1, \cdots, x_n \mapsto t_n \bigr]$.  Then $t\sigma$ is defined by induction on $t$:If $t$ is a variable, there are two cases when defining $t\sigma$:    $t = x_i$ for an $i\in\{1,\cdots,n\}$.  Then we define        $$ x_i\sigma := t_i. $$        $t = y$ where $y\in\mathcal{V}$, but $y \not\in \{x_1,\cdots,x_n\}$. Then we define         $$ y\sigma := y.$$  Otherwise we must have $t = f(s_1,\cdots,s_m)$. Then we define:       $$f(s_1, \cdots, s_m)\sigma := f(s_1\sigma, \cdots, s_m\sigma). $$<jupyter_code>def apply(t, σ):
    "Apply the substitution σ to the term t."
    if isinstance(t, frozenset):                     # t is a clause
        return frozenset({ apply(c, σ) for c in t })
    if isinstance(t, set):                           # t is a set of equations
        return { apply(c, σ) for c in t }
    if isinstance(t, str):                           # t is a variable
        if t in σ:
            return σ[t]
        else:
            return t
    else: # t must be a term, literal, or equation
        f  = t[0]
        ts = t[1:]
        return (f,) + tuple(apply(s, σ) for s in ts)
s1 = parseTerm('G(z)')
s2 = parseTerm('H(u, v)')
σ = { 'x': s1, 'y': s2 }
σ
t = parseTerm('F(x,H(y,x),G(z))')
t
apply(t, σ)<jupyter_output><empty_output><jupyter_text>If  $\sigma = \big[ x_1 \mapsto s_1, \cdots, x_m \mapsto s_m \big]$ and$\tau = \big[ y_1 \mapsto t_1, \cdots, y_n \mapsto t_n \big]$ are two substitutions that are non-overlapping, i.e. such that $\texttt{dom}(\sigma) \cap \texttt{dom}(\tau) = \{\}$ holds,then we define the composition $\sigma\tau$ of $\sigma$ and $\tau$ as follows:$$\sigma\tau := \big[ x_1 \mapsto s_1\tau, \cdots, x_m \mapsto s_m\tau,\; y_1 \mapsto t_1, \cdots, y_n \mapsto t_n \big]$$The function $\texttt{compose}(\sigma, \tau)$ takes two non-overlapping substitutions and computes the composition $\sigma\tau$.<jupyter_code>{'a':1, 'b':2}.items()
def compose(σ, τ):
    Result = { x: apply(s, τ) for (x, s) in σ.items() }
    Result.update(τ)
    return Result
τ = { 'z': s1, 'u': s2 }
σ
τ
compose(σ, τ)<jupyter_output><empty_output><jupyter_text>The function $\texttt{occurs}(x, t)$ checks whether the variable $x$ occurs in the term $t$.<jupyter_code>def occurs(x, t):
    if x == t:
        return True
    if isinstance(t, str): # t must be a variable different from x
        return False
    return any(occurs(x, arg) for arg in t[1:])
t
occurs('u', t)
occurs('x', t)<jupyter_output><empty_output><jupyter_text>The Algorithm of Martelli and Montanari The rules of Martelli and Montanari that can be used to solve a system of syntactical equations are as follows: If $y\in\mathcal{V}$ is a variable that does not occur in the term $t$,     then we perform the following reduction:      $$ \Big\langle E \cup \big\{ y \doteq t \big\}, \sigma \Big\rangle \quad\leadsto \quad          \Big\langle E[y \mapsto t], \sigma\big[ y \mapsto t \big] \Big\rangle      $$       If the variable $y$ occurs in the term $t$, then the system of syntactical equations     $E \cup \big\{ y \doteq t \big\}$ is not solvable:     $$ \Big\langle E \cup \big\{ y \doteq t \big\}, \sigma \Big\rangle\;\leadsto\; \texttt{None} \quad        \mbox{if $x \in \textrm{Var}(t)$ and $y \not=t$.}$$ If $y\in\mathcal{V}$ is a variable and $t$ is no variable, then we use the following rule:     $$ \Big\langle E \cup \big\{ t \doteq y \big\}, \sigma \Big\rangle \quad\leadsto \quad          \Big\langle E \cup \big\{ y \doteq t \big\}, \sigma \Big\rangle.     $$    Trivial syntactical equations of variables can be dropped:     $$ \Big\langle E \cup \big\{ x \doteq x \big\}, \sigma \Big\rangle \quad\leadsto \quad         \Big\langle E, \sigma \Big\rangle.     $$    If $f$ is an $n$-ary function symbol, then we have:      $$ \Big\langle E \cup \big\{ f(s_1,\cdots,s_n) \doteq f(t_1,\cdots,t_n) \big\}, \sigma \Big\rangle          \;\leadsto\;          \Big\langle E \cup \big\{ s_1 \doteq t_1, \cdots, s_n \doteq t_n\}, \sigma \Big\rangle.     $$    The system of syntactical equations $E \cup \big\{ f(s_1,\cdots,s_m) \doteq g(t_1,\cdots,t_n) \big\}$     has no solution if the function symbols $f$ and $g$ are different:     $$ \Big\langle E \cup \big\{ f(s_1,\cdots,s_m) \doteq g(t_1,\cdots,t_n) \big\},      \sigma \Big\rangle \;\leadsto\; \texttt{None} \qquad \mbox{if $f \not= g$}.     $$ Given two terms $s$ and $t$, the function $\texttt{unify}(s, t)$ computes the most general unifier of $s$ and $t$.<jupyter_code>def unify(s, t):
    return solve({('≐', s, t)}, {})<jupyter_output><empty_output><jupyter_text>Given a set of syntactical equations $E$ and a substitution $\sigma$, the function $\texttt{solve}(E, \sigma)$ uses the rules of Martelli and Montanari to solve $E$.<jupyter_code>def solve(E, σ):
    while E != set():
        print(E, σ)
        _, s, t = E.pop()
        if s == t:
            continue
        if isinstance(s, str): # s is a variable
            if occurs(s, t):
                return None
            else:
                E = apply(E, { s: t })
                σ = compose(σ, { s: t })
        elif isinstance(t, str): # t is a variable, but s is not
            E.add(('≐', t, s))
        else:
            f    , g     = s[0]      , t[0]
            sArgs, tArgs = s[1:]     , t[1:]
            m    , n     = len(sArgs), len(tArgs)
            if f != g or m != n:
                return None
            else:
                E |= { ('≐', sArgs[i], tArgs[i]) for i in range(m) }
    return σ
t1 = parseTerm('P(x1,F(x1))')
t2 = parseTerm('P(G(x2),x3)')
μ = unify(t1, t2)
μ<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.16061093247588423, 'fraction_numerical': 0.007395498392282958, 'mean_word_length': 2.5186651583710407, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 25, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '6', 'dir': 'jupyter-structured-clean-dedup', 'id': '278650', 'license': 'MIT', 'n_tokens_mistral': 2287, 'n_tokens_neox': 2210, 'n_words': 762, 'path': 'Python/Unification.ipynb', 'repo_name': 'Sarius5/Logic-1', 'size': '6220'}