Основы Изабель/HOL

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

1) Почему Isabelle/HOL не допускают функции, которые не заканчиваются? Многие другие языки, такие как Haskell, допускают неограничивающие функции.

2) Какие символы являются искусством метаязыка Изабеллы? Я прочитал, что есть символы в метаязыке для универсальной квантификации (/\) и для импликации (==>). Однако эти символы имеют свой аналог на языке объектного уровня (∀ и -->). Я понимаю, что --> - это функция уровня объекта типа bool => bool => bool. Однако как определяются ∀ и ∃? Являются ли они логическими функциями уровня объекта? Если это так, они не являются вычислимыми (учитывая бесконечные области). Я заметил, что я могу писать логические функции в темах ∀ и ∃, но они не являются вычислимыми. Итак, что такое ∀ и ∃? Являются ли они частью уровня объекта? Если да, то как они определены?

3) Являются ли теоремы Изабеллы просто булевыми выражениями? Тогда булевы являются частью метаязыка?

4) Насколько я знаю, Isabelle - строгий язык программирования. Как я могу использовать бесконечные объекты? Скажем, бесконечные списки. Возможно ли это в Isabelle/HOL?

Извините, если эти вопросы очень просты. Кажется, я не нашел хорошего учебника по метатеории Изабель. Мне бы очень хотелось, чтобы кто-нибудь мог порекомендовать мне хороший учебник по этим темам.

Большое спасибо.

Ответ 1

1) Вы можете определить функции без конца (то есть частичные) в Isabelle (см. Руководство по пакету функций (раздел 8)). Однако частичные функции сложнее рассуждать, потому что всякий раз, когда вы хотите использовать свои уравнения определения (правила psimps, которые заменяют правила simps нормальной функции), вы должны показать, что функция завершается на этом конкретный ввод.

В общем, такие вещи, как неопределенность и не-окончание, всегда логичны в логике - рассмотрим, например, определение функции f x = f x + 1. Если бы мы приняли это как уравнение на ℤ (целые числа), мы могли бы вычесть f x с обеих сторон и получить 0 = 1. В Haskell эта проблема "решается, говоря, что это не уравнение на ℤ, а скорее ℤ ∪ ⊥ (целые числа плюс нижнее) и функция без конца f оценивается как ⊥, а" ⊥ + 1 = ⊥, так что все работает отлично.

Однако, если каждое отдельное выражение в вашей логике может потенциально оценить ⊥ вместо "правильного" значения, рассуждение в этой логике станет очень утомительным. Вот почему Isabelle/HOL решает ограничить себя полными функциями; такие вещи, как пристрастность, должны быть эмулированы такими вещами, как undefined (это произвольное значение, о котором вы ничего не знаете) или типы опций.

2) Я не специалист по Isabelle/Pure (мета логика), но наиболее важные символы определенно

⋀ (универсальный мета-квантификатор)
⟹ (мета-импликация)
≡ (meta равенство)
&&& (метасоединение, определенное в терминах ⟹)
Pure.term, Pure.prop, Pure.type, Pure.dummy_pattern, Pure.sort_constraint, которые выполняют некоторые внутренние внутренние функции, о которых я мало что знаю.

Информацию об этом можно найти в справочном руководстве Isabelle/Isar > в разделе 2.1 и, возможно, в других местах руководства.

Все остальное (включая ∀ и ∃, которые действительно работают с булевыми выражениями) определяется в логике объекта (обычно HOL). Вы можете найти определения, а именно аксиоматизации, в ~~/src/HOL/HOL.thy (где ~~ обозначает корневой каталог Isabelle):

All_def:      "All P     ≡ (P = (λx. True))"
Ex_def:       "Ex P      ≡ ∀Q. (∀x. P x ⟶ Q) ⟶ Q"

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

3) Теоремы Изабель являются сложным типом данных (см. ~~/src/Pure/thm.ML), содержащим много информации, но наиболее важной частью, конечно же, является предложение. Предложение есть что-то от Изабель/Чисто, которое на самом деле имеет только предложения и функции. (и itself и dummy, но вы можете их игнорировать).

Предложения не являются булевыми - на самом деле даже не существует способа утверждать, что предложение не выполняется в Isabelle/Pure.

HOL затем определяет (или, скорее, аксиоматизирует) булевы, а также аксиоматизирует принуждение от булевых к предложениям: Trueprop :: bool ⇒ prop

4) Isabelle - это не язык программирования, и кроме того, тотальность не означает, что вы должны ограничивать себя конечными структурами. Даже на общем языке программирования вы можете иметь бесконечные списки. (см. Идрис codata)

Изабелла - это теоретический прорыв, и логически бесконечные объекты могут обрабатываться путем аксиоматизации их, а затем рассуждения о них с использованием аксиом и правил, которые у вас есть.

Например, HOL предполагает существование бесконечного типа и определяет натуральные числа на этом. Это уже дает вам доступ к функциям nat ⇒ 'a, которые по сути являются бесконечными списками.

Вы также можете определить бесконечные списки и другие бесконечные структуры данных как codatatypes с пакетом (co-) datatype, который основан на ограниченных естественных функторах.

Ответ 2

Позвольте мне добавить несколько вопросов к двум вашим вопросам.

1) Почему Isabelle/HOL не допускают функции, которые не заканчиваются? Многие другие языки, такие как Haskell, допускают неограничивающие функции.

Короче: Isabelle/HOL не требует завершения, а тотальность (т.е. для каждого входа функции) есть функции. Тотальность не означает, что функция фактически заканчивается, когда она транскрибируется (функциональным) языком программирования или даже что она вообще вычислима.

Поэтому разговор о завершении несколько вводит в заблуждение, хотя его поощряет тот факт, что пакет функций Isabelle/HOL использует ключевое слово termination для доказательства некоторого свойства P, о котором я должен будет сказать немного больше ниже.

С одной стороны, термин "прекращение" может казаться более интуитивным для более широкой аудитории. С другой стороны, более точное описание P было бы обоснованностью графика вызова функции.

Не поймите меня неправильно, termination не очень плохое имя для свойства P, это даже оправдано тем фактом, что многие методы, которые реализованы в пакете функций, очень близки к методам завершения из (например, принцип изменения размера, пары зависимостей, лексикографические заказы и т.д.).

Я просто говорю, что это может ввести в заблуждение. Ответ на этот вопрос также касается вопроса 4 ОП.

4) Насколько я знаю, Isabelle - строгий язык программирования. Как я могу использовать бесконечные объекты? Скажем, бесконечные списки. Возможно ли это в Isabelle/HOL?

Isabelle/HOL - это не язык программирования, и в нем нет какой-либо стратегии оценки (мы могли бы сказать: у нее есть любая стратегия оценки, которая вам нравится).

И вот почему окончание слова вводит в заблуждение (барабанный ролл): если нет стратегии оценки, и у нас есть прекращение функции f, люди могут ожидать, что f прекратит независимость от используемой стратегии. Но это не так. A termination доказательство a function скорее гарантирует, что f четко определен. Даже если f вычислимо, доказательство P просто гарантирует, что существует стратегия оценки, для которой f завершается.

(В стороне: то, что я называю "стратегией" здесь, обычно зависит от так называемых cong-правил (т.е. правил конгруэнтности) в Isabelle/HOL.)

В качестве примера тривиально доказать, что функция (см. раздел 10.1 "Правила конгруэнтности и порядок оценки в документации пакета функций" ):

fun f' :: "nat ⇒ bool"
where
  "f' n ⟷ f' (n - 1) ∨ n = 0"

завершается (в смысле, определяемом termination) после добавления cong-правила:

lemma [fundef_cong]:
  "Q = Q' ⟹ (¬ Q' ⟹ P = P') ⟹ (P ∨ Q) = (P' ∨ Q')"
by auto

Что, по сути, означает, что логическое - или должно быть "оценено" справа налево. Однако, если вы пишете ту же функцию, например. в OCaml это вызывает переполнение стека...

Ответ 3

РЕДАКТИРОВАТЬ: этот ответ не совсем правильный, ознакомьтесь с комментарием Ларса ниже.

К сожалению, у меня недостаточно репутации, чтобы опубликовать это как комментарий, так что вот мой ответ (пожалуйста, имейте в виду, что я не эксперт в Изабель, но у меня также были подобные вопросы один раз):

1) Идея состоит в том, чтобы доказать утверждения об определенных функциях. Я не уверен, насколько вы знакомы с Теорией вычислимости, но думайте о проблеме с остановкой и о том, что из нее возникают основные проблемы (например, проблема принятия). Представьте, что вы определяете функцию, которую вы не можете доказать, что она завершается. Как вы могли бы тогда доказать, что он возвращает число 42 при вводе "ABC", и он не идет в бесконечном цикле?

Если вместо этого вы ограничиваете себя завершающими функциями, вы можете доказать гораздо больше о них, по сути дела делая компромисс (или, по крайней мере, так я это вижу).

Эти идеи проистекают из конструктивизма и интуитивизма, и я рекомендую вам ознакомиться с очень интересной лекционной серией Роберта Харпера: https://www.youtube.com/watch?v=9SnefrwBIDc&list=PLGCr8P_YncjXRzdGq2SjKv5F2J8HUFeqN по теории типов

Следует особо отметить часть отсутствия закона исключенного среднего: http://youtu.be/3JHTb6b1to8?t=15m34s

2) См. ответ Мануэля.

3,4) Снова см. ответ Мануэля с учетом интуиционистской логики: "фундаментальная сущность не является логической, а скорее доказательством того, что что-то истинно".

Для меня потребовалось много времени, чтобы приспособиться к этому способу мышления, и я все еще не уверен, что понимаю. Я думаю, что ключевым является то, чтобы понять, что это более или менее совершенно другой способ мышления.