Module Instance

instanceOf :: Expr -> Expr -> Bool   

Is the first expression an instance of the second expression?

instanceWith :: Expr -> Expr -> Maybe Subst   

instanceWith e1 e2 tries to compute a substitution sigma such that $e1 = \sigma(e2)$. If e1 is an instance of e2, the function returns Just sigma, if not then Nothing is returned.

Note that instance requires the expressions to share the same structure, i.e., no normalization is considered.

msg :: Expr -> Expr -> (Expr,Subst,Subst)   

msg e e' = (g, sigma, theta) returns the most specific generalization g of e and e' and the substitutions sigma and theta, such that $e = \sigma(g)$, and $e' = \theta(g)$. A generalizer of two terms $e1$, $e2$ is a term $e$, such that $\sigma(e) = e1$ and $theta(e) = e2$ ($e$ generalizes $e1$ and $e2$). Furthermore, there is no other generalization $e'$ of $e1$ and $e2$, such that $e' \neq e$ and $\tau(e) = e'$ ($e$ is most specific). We do not rename the msg because otherwise the substitution may refer to variables locally introduced in the msg.