Могу ли я перегрузить нотацию для операторов, которые назначены для bool и list?

(ПРИМЕЧАНИЕ: если я могу избавиться от предупреждения, которое я показываю ниже, то я говорю несколько посторонних вещей. В качестве части вопроса я также высказываю некоторые соображения. Думаю, это своего рода вопрос "Почему я не прав?" вот что я скажу?")

Кажется, что 6 символов, используемых для bool операторы должны были быть назначены классам синтаксического типа, и bool создан для этих типов классов. В частности, это:

~, &, |, \<not>, \<and>, \<or>.

Поскольку тип аннотации терминов является частым требованием для операторов HOL, я не думаю, что это было бы большим бременем для использования bool аннотации для этих 6 операторов.

Я хотел бы перегрузить эти 6 символов для других логических операторов. Отсутствие обычных символов для приложения может привести к отсутствию хорошего решения для обозначения.

В следующем примере источника, если я смогу избавиться от предупреждений, тогда проблема будет решена (если я не буду устанавливать ловушку для себя):

definition natOP :: "nat => nat => nat" where
  "natOP x y = x"

definition natlistOP :: "nat list => nat list => nat list" where
  "natlistOP x y = x"

notation
  natOP (infixr "&" 35)    
notation
  natlistOP (infixr "&" 35) 

term "True & False"
term "2 & (2::nat)"  
term "[2] & [(2::nat)]" (*
OUTPUT: Ambiguous input produces 3 parse trees: 
  ...
  Fortunately, only one parse tree is well-formed and type-correct,
  but you may still want to disambiguate your grammar or your input.*)

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

Есть на самом деле и другие символы, которые я тоже хочу, такие как !, используется для list:

term "[1,2,3] ! 1"

Вот приложение, для которого я хочу символы:

Обновить

Основываясь на ответе Брайана Хаффмана, я &и переключить & к классу синтаксического типа. Это сработает или не будет, на самом деле, бинарной логикой, столь разнообразно применимой. Мое общее правило: "Не связывайтесь с Изабель /HOL по умолчанию".

(*|Unnotate; switch to a type class; see someday why this is a bad idea.|*) 

no_notation conj (infixr "&" 35)

class conj = 
  fixes syntactic_type_classes_are_awesome :: "'a => 'a => 'a" (infixr "&" 35)

instantiation bool :: conj
begin
definition syntactic_type_classes_are_awesome_bool :: "bool => bool => bool" 
  where "p & q == conj p q"
instance ..
end

term "True & False" 
value "True & False"
declare[[show_sorts]]
term "p & q" (* "(p::'a::conj) & (q::'a::conj)" :: "'a::conj" *)
Источник

1 ответ

Решение

Вы можете "отменить" специальный синтаксис, используя no_notation команда, например

no_notation conj (infixr "\<and>" 35)

Этот инфиксный оператор доступен для использования с вашими собственными функциями:

notation myconj (infixr "\<and>" 35)

С этого момента, \<and> относится к константе myconj вместо стандартного оператора соединения библиотеки HOL для типа bool, У вас не должно быть предупреждений о неоднозначном синтаксисе. Оригинальный логический оператор HOL все еще доступен по имени (conj), или вы можете дать ему другой синтаксис, если вы хотите с другим notation команда.

Для no_notation Команда для работы, шаблон и исправления должны быть точно такими же, как они были объявлены изначально. Увидеть src/HOL/HOL.thy для деклараций операторов, которые вас интересуют.

Я должен предупредить о потенциальной ловушке: последующие теории слияний могут вернуть первоначальный синтаксис обратно в область действия, снова вызывая неоднозначный синтаксис. Например, скажи свою теорию A.thy импорт Main и объявляет \<and> синтаксис. Тогда твоя теория B.thy импортирует оба A и другая теория библиотеки, скажем Complex_Main, Тогда в теории B, \<and> будет неоднозначным. Чтобы предотвратить это, обязательно поместите все внешние импорты теории в один файл теории, где вы измените синтаксис; тогда сделайте так, чтобы все ваши другие теории импортировали эту.

Источник
Другие вопросы по тегам