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

Question

Я использую математический инструментарий в 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) в Изабель, я предполагаю, что она ведет себя нормально.

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

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

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

Answer 1

Ваше правило 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 и Изабель, где выразительная сила эпсилон-термов дает значительные практические преимущества.

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

до свидания

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