$($a$)$ Consider the $-$term $t=vw(xy*vx).$

i$.$ Write $t$ in full, inserting all the missing parentheses and $\text{'}$s$.$

ii$.$ List the free variables and bound variables of $t.$

$[10$ marks$]$

$($b$)$ Give the $-$reduction graph of the $-$term $(xy*x)(II)I,$ where $I=x*x.$

Underline all redexes in the graph.

$[15$ marks$]$

$($c$)$ Define and explain the term disagreement set as used in the unification

algorithm as part of the algorithm for type reconstruction. Include in your

answer an example to illustrate the concept.

$[10$ marks$]$

$($d$)$ Build a type derivation to find the type of $x*(y.y)x.$

$[15$ marks$]$