Частичные функции по сравнению с недоопределенными полными функциями

Предположим, у меня есть набор A ⊆ nat. Я хочу смоделировать в Изабель функцию f : A ⇒ Y. Я мог бы использовать либо:

  1. частичная функция, то есть функция типа nat ⇒ Y option или
  2. общая функция, т. е. функция типа nat ⇒ Y, которая не указана для входных данных, не входящих в A.

Интересно, какой вариант "лучше". Я вижу пару факторов:

  • Подход «частичной функции» лучше, потому что проще сравнивать частичные функции на равенство. То есть, если я хочу посмотреть, равна ли f другой функции, g : A ⇒ Y, я просто говорю f = g. Чтобы сравнить неполные общие функции f и g, я должен был бы сказать ∀x ∈ A. f x = g x.

  • Подход с «недостаточной общей функцией» лучше, потому что мне не нужно постоянно возиться с конструированием/деконструкцией option типов. Например, если f является недоопределенной общей функцией, а x ∈ A, то я могу просто сказать f x, но если f является частичной функцией, я должен сказать (the ∘ f) x. С другой стороны, сложнее выполнять композицию функций на частичных функциях, чем на общих функциях.

В качестве конкретного примера, относящегося к этому вопросу, рассмотрим следующую попытку формализации простых графов.

type_synonym node = nat
record 'a graph = 
  V :: "node set"
  E :: "(node × node) set"
  label :: "node ⇒ 'a"

Граф состоит из набора узлов, отношения ребер между ними и label для каждого узла. Нас интересует только метка узлов, находящихся в V. Итак, должно ли label быть частичной функцией node ⇒ 'a option с dom label = V, или это должна быть просто общая функция, которая не указана вне V?


isabelle
person John Wickerson    schedule 14.03.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Это, вероятно, дело вкуса, а также может зависеть от того, какое использование вы имеете в виду, поэтому я просто дам вам свой личный вкус, который будет вариантом 2. общая функция. Причина в том, что я думаю, что ограниченная количественная оценка в обоих подходах в любом случае будет неизбежной. Я думаю, что при подходе 1 вы обнаружите, что самый простой способ справиться с Option — это ограничить область (ограниченное количественное определение), о которой вы рассуждаете. Что касается примера с графом, теоремы о графах всегда говорят что-то подобное для всех узлов в V. Но, как я уже сказал, это, вероятно, дело вкуса.

person Bryan Olivier    schedule 14.03.2013
comment
Спасибо Брайан. Тогда я буду защищать подход с частичными функциями... Если label является частичным, то эквивалентность графов G и H - это просто обычное равенство терминов, G=H. Но если label является тотальным, то эквивалентность становится более сложной, и, следовательно, о ней гораздо труднее рассуждать. - person John Wickerson; 14.03.2013
comment
В связи с этим возникает вопрос: насколько важно равенство терминов для графов? Может быть, два изоморфных графа более интересны. - person chris; 15.03.2013
comment
Действительно, поэтому нам все равно понадобится сложная эквивалентность. Я предполагаю, что это недостаток того, что я использую графики в качестве иллюстративного примера. - person John Wickerson; 15.03.2013