For this assignment you will implement unification of terms. This will require creating a type of terms, and implementing an algorithm that performs unification.
Implement this program in Astarte as a package that exports the term type and the unification function.
A term is a tree. Each internal vertex has a label that is a symbol and a list of subterms. Each leaf contains a value. For this assignment the term type should be parameterized. Type Term(T) holds terms whose leaves have type T. For example, a value of type Term(Boolean) might look as follows.
apple
/ \
banana true
|
orange
/ | \
true false true
A term can also contain variables. A variable has a name that is a symbol, and two variables with the same name are considered the same variable. A variable stands for a term, and is always a leaf of a tree when present. A tree with variables might look as follows.
apple
/ \
banana Y
|
orange
/ | \
true false X
So there are three kinds of terms: leaves, nonleaves and variables. Define the term type to have three constructors.
You will need to provide the constructors so that somebody can build terms. Make them as shown in the following table.
| constructor | type | what it builds |
|---|---|---|
| vr | String -> Term(`a) | vr(s) is a variable whose name is s. |
| lf | `a -> Term(`a) | lf(x) is a leaf holding value x |
| tm | (String, [Term(`a)]) -> Term(`a) | tm(r,[a,b,c]) is a term whose root label is r and whose subterms are a, b and c. |
A substitution is a list of pairs (X,V) where X is the name of a variable and V is the term that X is replaced by. You can use the assoc function to find the term that is bound to a variable.
Define a function unify(A,B) that takes two terms A and B and attempts to unify them by finding a substitution that makes them the same. If unification is possible, then unify(A,B) should return a pair (R,S) where S is a substitution that is a principal unifier of A and B, and R is the result of performing substitution S on A or B. (The result must be the same in both cases.)
Sometimes you will find yourself unifying two leaves together. Two leaves can only be unified if they hold the same value. So just do an equality test. Because you need to perform these equality tests, the type of thing in a leaf must be one that supports equality tests.
Create a new exception called UnifyX. If A and B cannot be unified, then unify(A,B) should fail with exception UnifyX.
Your unification algorith must use the occur check. It should not be possible to unify a variable X with a term T that contains X, unless T is exactly X.
Think carefully about the cases that are needed. Make your program simple and readable. Provide clear comments describing each function. Provide documentation for your unify function.
Your package should look as follows. Notice that unify is only defined for terms of type Term(T) where T supports an equality test. (Variable EQ`a can only stand for types that support operation ==.) The type term, however, can be more general.
Package unify
Export
Import "logic/symbol".
Extension
Expect{noEqual} species Term(`a).
%Extension
Exception unifyX "terms could not be unified".
Expect
unify : (Term(EQ`a), Term(EQ`a)) -> (Term(EQ`a), [(Symbol, Term(EQ`a))])
%" ... (describe unify)
;
vr : String -> Term(`a)
%" ... (describe vr)
;
lf : `a -> Term(`a)
%" ... (describe lf)
;
tm : (String, [Term(`a)]) -> Term(`a)
%" ... (describe tm)
%Expect
Implementation
Extension
Species{noEqual} Term(`a) =
...
%Species
%Extension
... (here is where the implemention of type Term, function unify and
... any helper functions should be put.
%Package