В формализации Изабель я представляю отношения бинарными предикатами.Я хотел бы иметь операторы, которые выполняют типичные операции отношения, такие как составление и инверсия, используя это представление.
В документе «Что в основном» упоминаются только такие операторы для представления множествами пар.В начале Relation теория говорит: «Отношения - как наборы пар и двоичные предикаты».Тем не менее, я не мог найти большую поддержку для представления двоичных предикатов в этой теории.Все, что я нашел, было несколько лемм с загадочным атрибутом pred_set_conv.
Существует ли обширная поддержка отношений, представленных двоичными предикатами?В частности, определены ли операторы для операций общего отношения?Где эти вещи задокументированы?