Задача уніфікації другого порядку у загальному випадку є нерозв’язною, хоча для окремої лямбда-алгебри термів другого порядку із одномісними функціональними символами її розв’язність доведено. Стандартний алгоритм уніфікації термів другого порядку має експоненційну складність, а генетичний алгоритм із використанням спеціальних метрик як функцій пристосованості є альтернативним способом ефективного знаходження уніфікатора.