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

Question

Я использую математический инструментарий в HOL-Z для выполнения некоторых предикатов Isabelle. в частности, я использую определение частичной функции для определения некоторых отношений в спецификации 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 

, где баланс и Bbalance оба частичные функции (в Z), вида ('a < =>' b) в Изабель, я предполагаю, что он ведет себя хорошо.

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

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

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

Answer 1

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

Руководящей аксиома функции эпсилона гласят:

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

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

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

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

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

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

Bye

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