работа элементов в наборе в Изабель

Question

В моей недавней работе ， речь идет об алгебраической семантике. Я хочу выразить новую операцию элементов в наборе в Изабель, и эти элементы очень сложны.Эта операция является расширением двоичной операции.и эта бинарная операция легко завершилась по локали.такие как: a⊕b = c

locale Probjia = Prob + Prep + fixes probjiao :: "'b ⇒ 'b ⇒ 'b" (infixl "⊕" 90)

НО, я не знаю, как выразить эту операцию элементов в наборе.Советы: я не знаю, сколько элементов в этом наборе.

Надеюсь, ⊕A, A = {a, b, c, d, ......}, затем ⊕A = a⊕b⊕c⊕d ......

Кто-нибудь может дать мне несколько советов?или какой-то пример, который я могу выучить сам.Мой английский не очень хороший, надеюсь выразить четко.

Answer 1

Операция коммутативного моноида может быть увеличена до конечных наборов с использованием оператора F в локали comm_monoid_set.Вам нужен моноид такой, чтобы пустой набор мог быть представлен как нейтральный элемент.Я рекомендую вам посмотреть, как определены предопределенные функции sum и prod (введите term "sum" и и Ctrl-Click на sum, чтобы перейти к определению).В вашем случае, вы, вероятно, захотите объявить отношение подцены:

context Probjia begin
sublocale probjiao: comm_monoid_set probjiao neutral_element_for_probjiao
  defines Probjiao = probjiao.F

, где neutral_element_for_probjiao - нейтральный элемент для вашей операции.После того, как вы закончили доказательство, Probjiao - это поднятая версия вашего оператора.