Значение Изабель КОНСТ (по отношению к THE) - PullRequest
Новая
       13

Значение Изабель КОНСТ (по отношению к THE)

1 голос
/ 02 октября 2019

Что означает CONST в Изабель / Чистый? В HOL.thy у нас есть следующие блоки кода: 

translations "∃!x. P" ⇌ "CONST Ex1 (λx. P)"

translations "THE x. P" ⇌ "CONST The (λx. P)"

translations
  "_Let (_binds b bs) e"  ⇌ "_Let b (_Let bs e)"
  "let x = a in e"        ⇌ "CONST Let a (λx. e)"

Я пытался понять, что означает «THE», и нашел это в HOL.thy. «THE» объясняется несколько здесь , но я не совсем понимаю, что происходит в принципе, так как предположим, что P :: 'a ==> a' ==> bool 

definition test :: "'a ==> 'a" where
"test y = (THE x. (P x y))"

Как "test y" может быть типа "'a", если не существует x st P xy? Каким-то образом это должно быть скрыто в CONST и The (что я также не совсем понимаю, так как это просто дано аксиоматически как нечто типа "('a ==> bool) ==>' a" без каких-либо свойств).

Возможно, самое главное, где есть ссылка на все это ?? Его нет в справочном руководстве по Изабель / Изаре, учебном пособии по Изабель HOL, в PDF-документе о реализации Изабель / Изаре, в комментариях к файлам теории или в любом другом месте, которое мне удалось найти.

...