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

Я работаю над теорией, в которой я довольно активно использую экстенсиональные функции, определенные в теории Funcset. Мне нужно работать с функциями, оценивающими функции, где и функция, и значения являются экстенсиональными. Очень досадно, что некоторые из моих лемм терпят неудачу, потому что функция undefined не отображает все в undefined. Итак, цель

undefined x = undefined

не доказуемо. Я могу обойти это, используя ограничения, но без них было бы намного элегантнее. Безопасно ли добавлять новую аксиому:

axiomatization where 
  undefined_at [simp]: "undefined x = undefined"

? Меня это беспокоит, потому что

1) Я не уверен, стоит ли возиться с такой логикой.

2) После того, как я добавлю эту аксиому, для таких целей, как "undefined \ in A", придирание выдает ошибку: Limit reached: too many nested axioms (256).

3) На первый взгляд столь же невинная аксиома

axiomatization where 
  at_undefined [simp]: "f undefined = undefined"

создает странные цели вроде «P ==> undefined».


isabelle
person Dávid Kertész    schedule 07.07.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Константа undefined на самом деле не моделирует математическое понятие undefined. Скорее это означает отсутствие указания, как я объяснил в тема в списке рассылки Изабель.

Еще в 2008 году, undefined фактически было указано с аксиомой undefined x = undefined, т. е. функция undefined отображает все в undefined. Вскоре люди поняли, что это не то, что undefined должно представлять, потому что это ограничивало функцию undefined постоянной функцией, которая вообще не является произвольной функцией. Добавление этой аксиомы не делает HOL несостоятельным, но сильно ограничивает универсальность доказанного, потому что undefined часто используется пакетами Изабель.

Однако другая аксиома at_undefined ведет к противоречиям. Как указано, это означает, что каждая функция f должна быть идентификатором для неопределенного значения undefined. Рассмотрим тип bool логических значений. undefined должен быть либо True, либо False. Итак, если вы возьмете отрицание для f, тогда аксиома требует ~ True = True или ~ False = False. Очевидно, это несовместимо со спецификацией op ~, поэтому аксиома несовместима.

person Andreas Lochbihler    schedule 07.07.2015
comment
Спасибо, ваш ответ был очень полезным. Приятно знать, что undefined_at безопасно и разумно добавлять, но слишком специфичен для некоторых приложений. Я собираюсь определить новую undefined (я хочу назвать ее nothing) с более сильной аксиомой и буду использовать ее там, где мне нужно. - person Dávid Kertész; 08.07.2015
comment
Собственно, вам и не нужны аксиомы. Определите класс типа class nothing = fixes nothing и создайте его для нужных вам типов. Для типа функции используйте instantiation "fun" :: (type, nothing) nothing begin definition "nothing x = nothing" instance .. end. Если создание экземпляров всех типов слишком громоздко, вы также можете использовать неограниченную перегрузку, что также безопасно. consts nothing :: 'a overloading f == "nothing :: ('a ⇒ 'b)" begin definition nothing_fun_def: "f (x :: 'a) = (nothing :: 'b)" end В обоих подходах вы можете добавить больше уравнений для других типов позже. - person Andreas Lochbihler; 08.07.2015