Рассматривается класс основанных на решетках алгебраических структур, описывающих семантику иерархии типов в объектно-ориентированной системе. Исследуются свойства таких структур, включая существование логической редукции. Методология предназначена для верификации и модернизации иерархий типов, важным направлением которой является устранение избыточности кода. Впервые приводятся доказательства полученных результатов.