нужно определение в Изабель, чтобы показать, что две частичные функции никогда не производят одинаковый результат

Я использую математический инструментарий HOL-Z для выполнения некоторых предикатов Изабель. в частности, я использую частичное определение функции для определения некоторых отношений в спецификации Z, которую я пишу, где я конвертирую схему в операторы спецификации, чтобы я мог генерировать простые предикаты HOL.

определения из набора инструментов HOL-Z

type_synonym      ('a,'b) lts = "('a*'b) set"     (infixr "<=>" 20)

  prodZ       ::"['a set,'b set] => ('a <=> 'b) "        ("_ %x _"  [81,80] 80)
"a %x b"        == "a <*> b"

rel           ::"['a set, 'b set] => ('a <=> 'b) set"    ("_ <--> _"   [54,53] 53)
rel_def       : "A <--> B    == Pow (A %x B)"

partial_func  ::"['a set,'b set] => ('a <=> 'b) set"     ("_ -|-> _"   [54,53] 53)
partial_func_def  : "S -|-> R    == 
    {f. f:(S <--> R) & (! x y1 y2. (x,y1):f & (x,y2):f  --> (y1=y2))}"

rel_appl      :: "['a<=>'b,'a] => 'b"    ("_ %^ _"  [90,91] 90)
rel_appl_def  :  "R %^ x       == (@y. (x,y) : R)"

Когда я пишу в предикате следующее:

FORALL x. balance %^ x = Bbalance %^ x

где balance и Bbalance являются частичными функциями (в Z) формы ('a ‹=>' b) в Isabelle, я полагаю, что это нормально.

Как я могу определить другую функцию, в которой я говорю, что две частичные функции полностью не пересекаются для всех 'x'. Я имею в виду, что относительное применение одного и того же значения к двум частичным функциям «баланс» и «Bbalance» НИКОГДА не дает одно и то же значение. что-то типа...

FORALL x. balance %^ x \noteq Bbalance %^ x

извините за плохое объяснение. мы узнаем через советы специалистов :).


theorem-proving theorem master-theorem isabelle z-notation
person Shiyam    schedule 28.01.2015    source источник

Ответы (1)


arrow_upward
1
arrow_downward

В вашем правиле rel_appl_def используется функция epsilon. Согласно Стэнфордской энциклопедии философии (SEP) (*) в его лекции в Гамбурге в 1921 (1922), Гильберт впервые представил идею использования функций выбора для работы с принципом исключенного третьего в формальной арифметической системе.

Основная аксиома функции эпсилон гласит:

 (A x) --> (A (@ A))

В классической логике из-за ex falso quodlibet, если (A x) терпит неудачу, (@ A) может принимать любую интерпретацию. Это означает, что ваше правило rel_appl_def дает любое значение, когда вы указываете аргумент x, который не находится в домене dom R.

Так что, вероятно, то, что вы хотите использовать в качестве равенства, будет следующей логической функцией (^) для двух частичных функций:

 f ^ g = (dom f = dom g) & (!x. x : dom f --> f %^ x = g %^ x)

То, что я не могу понять, когда пишет SEP, второе, возможно, более актуальное в настоящее время, - это использование эпсилон-оператора в системах доказательства теорем HOL и Isabelle, где выразительная сила эпсилон-терминов дает значительные практические преимущества.

На практике я видел гораздо более простую трактовку частичных функций, а именно использование типа option. Таким образом, частичная функция f просто принадлежит типу A => B. Но когда вы не можете изменить типы в своем проекте, вероятно, разумнее будет искать равенство, которое соответствует вашим требованиям, приведенное выше определение может быть кандидатом.

Пока

(*)
Исчисление Эпсилон, Джереми Авигад и Ричард Зак
Впервые опубликовано 3 мая 2002 г .; существенная редакция, среда, 27 ноября 2013 г.
http://plato.stanford.edu/entries/epsilon-calculus/

person Mostowski Collapse    schedule 29.01.2015
comment
Я просто заметил, что, скорее всего, Изабель позволит вам доказать (f ^ g) ‹-› (f = g), а Изабель также даст вам (! X. X: f = x: g) ‹-› (f = г). Но я не вижу больших шансов для (! X. (F% ^ x) = (g% ^ x)) ‹-› (f = g). - person Mostowski Collapse; 30.01.2015
comment
Так же, как боковой узел: в новой версии Isabelle также есть директива partial_function, см. Также здесь: stackoverflow.com/questions/25280566/ Но в настоящее время я не знаю базовый механизм и будет ли он состоять из другой жизнеспособной альтернативы. - person Mostowski Collapse; 30.01.2015