thy_goal_defn и ключевые слова в Изабель / HOL - PullRequest
Новая
       11

thy_goal_defn и ключевые слова в Изабель / HOL

1 голос
/ 29 сентября 2019

Я пытаюсь понять, как строится математика в Изабель.По какой-то причине во всех руководствах / руководствах скрыты многие детали реализации базовых типов, таких как конструирование натуральных чисел, целых, рациональных и вещественных чисел.Просматривая каталог src / HOL и просматривая файлы .thy, я обнаружил такие блоки кода, как: 

keywords
  "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
  "quotient_type" :: thy_goal_defn and "/" and
  "quotient_definition" :: thy_goal_defn
begin

в Quotient.thy.Здесь используются ключевые слова, так что позже вы можете определить тип как: 

quotient_type rat = "int * int" / partial: "ratrel"

и другие связанные определения.Я не смог понять, как работает функция «ключевые слова».Это не особенно очевидно из кода, и единственная документация, которую я могу найти, находится в Справочном руководстве Изабель / Изар, где написано следующее:

"Спецификация ключевых слов объявляет внешний синтаксис (глава 3), который представлен вэта теория позже (редко встречается в приложениях для конечных пользователей). Необходимо указать как второстепенные ключевые слова, так и основные ключевые слова языка команд Isar, чтобы синтаксический анализ корректных документов работал должным образом. Ключевые слова команды должны быть классифицированы.в соответствии с их структурной ролью в формальном тексте. Примеры можно увидеть в самих источниках Isabelle / HOL, таких как ключевые слова "typedef" :: thy_goal_defn или ключевые слова "datatype" :: thy_defn для определений теоретического уровня с доказательством и без него,соответственно."(стр. 91)

Это поднимает вопрос о том, что такое определение на уровне теории, которое я не смог выяснить.

1 Ответ

2 голосов
/ 29 сентября 2019

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

Грубо говоря, файл теории в Изабель состоит из двух частей:

  1. Заголовок, который может быть проанализированстатически, т.е. без запуска какого-либо пользовательского кода.
  2. Содержимое, где, например, логические определения (типы, константы, ...) и доказательства могут быть в режиме.

Анализ содержимогопроисходит в два этапа:

  1. Сначала разбирается структура команд.Это можно сделать, просмотрев таблицу всех существующих ключевых слов (которые объявлены в заголовке).Существуют различные типы ключевых слов (как указано в руководстве).Ключевые слова команды запускают новый атомный блок в теории.(Следовательно, содержание теории можно рассматривать как последовательность команд.)
  2. Во-вторых, сами команды анализируются с использованием пользовательского кода синтаксического анализа, указанного тем, кто объявил соответствующее ключевое слово.Это будет выполнять любое действие, например, фактически определять тип в теории, когда встречается ключевое слово typedef.

Команды могут быть классифицированы в соответствии с контекстом, в котором они могут появляться.Команды верхнего уровня могут появляться только на верхнем уровне теории.Другие команды могут быть свободно вложены в локальные контексты.Все же другие команды не изменяют теорию, а только выводят диагностический вывод (diag).Обработка теории в Изабель учитывает это, например, при распараллеливании выполнения теории.

Упомянутый вами пример, thy_goal_defn, является ключевым словом, которое добавляет некоторые определения в теорию и также входит в режим доказательства, потому что quotient_type требует доказательств правильности определения.

...