Substitution tree

Substitution tree – metoda indeksowania termów polegająca na trzymaniu w każdym termie podstawienia, które należy wykonać na węźle rodzicu żeby uzyskać dany term.

W substitution tree inaczej traktowane są zmienne zewnętrzne (czyli po prostu pewne symbole) oraz zmienne wewnętrzne (służące wyłącznie do opisywania części wspólnych drzew).

Przykład dla $g(b),$ $f(a,g(b))$ i $f(b,g(b)){:}$

$x$ i $y$ są tu zmiennymi wewnętrznymi.

W substitution tree ma miejsce o wiele więcej współdzielenia niż w drzewie dyskryminacyjnym, jest więc ono pamięciowo o wiele bardziej wydajne. Wciąż jednak $g(b)$ jest dzielone jedynie pomiędzy niektórymi wystąpieniami.