Try and compare the two. There are some places where unification does not work.
Given a non-terminating process on some certificate, if we replace some terms in the certificate with variables, we get failure. How can it be?! There should be more options now! The only answer I can think of now is that more abstraction causes the unification to fail.
Try and compare the two. There are some places where unification does not work.
Given a non-terminating process on some certificate, if we replace some terms in the certificate with variables, we get failure. How can it be?! There should be more options now! The only answer I can think of now is that more abstraction causes the unification to fail.