Двенадцать

Twelf — это реализация логической структуры LF, разработанной Фрэнком Пфеннингом и Карстеном Шюрманном в Университете Карнеги-Меллон . ^[1] Он используется для логического программирования и для формализации теории языков программирования .

Введение [ править ]

В самом простом виде программа Twelf (называемая «сигнатурой») представляет собой набор объявлений семейств типов (отношений) и констант, населяющих эти семейства типов. Например, следующее является стандартным определением натуральных чисел: z обозначающий ноль и s оператор-преемник.

nat : type.

z : nat.
s : nat -> nat.

Здесь nat это тип, и z и s являются постоянными условиями. В качестве зависимо типизированной системы типы могут индексироваться по терминам, что позволяет определять более интересные семейства типов. Вот определение сложения:

plus : nat -> nat -> nat -> type.

plus_zero : {M:nat} plus M z M.

plus_succ : {M:nat} {N:nat} {P:nat}
            plus M (s N) (s P)
         <- plus M N P.

Типовое семейство plus читается как отношение между тремя натуральными числами M, N и P, такой, что M + N = P. Затем мы даем константы, которые определяют соотношение: константа plus_zero указывает на то, что M + 0 = M. Квантор {M:nat} можно прочитать как «для всех M типа nat".

Константа plus_succ определяет случай, когда второй аргумент является преемником какого-либо другого числа N (см. сопоставление с образцом ). Результатом является преемник P, где P это сумма M и N. Этот рекурсивный вызов выполняется через подцель plus M N P, представленный с <-. Стрелку можно понимать функционально как символ Пролога. :-, или как логическое следствие («если M + N = P, то M + (s N) = (s P)»), или, наиболее точно по теории типов, как тип константы plus_succ («когда задан термин типа plus M N P, вернуть термин типа plus M (s N) (s P)").

Twelf поддерживает реконструкцию типов и поддерживает неявные параметры, поэтому на практике обычно нет необходимости явно записывать {M:nat} (и т. д.) выше.

Эти простые примеры не демонстрируют ни функции LF высшего порядка, ни какие-либо его возможности проверки теорем. См. примеры дистрибутива Twelf.

Использует [ править ]

Twelf используется по-разному.

Логическое программирование [ править ]

Двенадцать подписей могут быть выполнены с помощью процедуры поиска. Его ядро более сложное, чем у Пролога , поскольку оно имеет более высокий порядок и имеет зависимую типизацию, но оно ограничено чистыми операторами: здесь нет оператора Cut или других экстралогических операторов (например, для выполнения ввода-вывода ), которые часто встречаются в Прологе. реализации, что может сделать его менее подходящим для практических приложений логического программирования. Некоторые варианты использования правила отсечения Пролога можно получить, объявив, что определенные операторы принадлежат к детерминированным семействам типов, что позволяет избежать пересчета. Кроме того, как и λProlog , Twelf обобщает предложения Хорна до наследственных формул Харропа , которые допускают логически обоснованные рабочие понятия генерации новых имен и масштабируемого расширения базы данных предложений.

Формализация математики [ править ]

Twelf сегодня в основном используется как система формализации математики, особенно метатеории языков программирования . Таким образом, он тесно связан с Coq и Isabelle / HOL / HOL Light . Однако, в отличие от этих систем, доказательства Twelf обычно разрабатываются вручную. Несмотря на это, для проблемных областей, в которых он превосходен, доказательства Twelf часто короче и их легче разрабатывать, чем в автоматизированных системах общего назначения.

Встроенное в Twelf понятие связывания и замены облегчает кодирование языков программирования и логики, большинство из которых используют связывание и замену, которые часто могут быть напрямую закодированы с помощью абстрактного синтаксиса более высокого порядка (HOAS), где связыватели метаязыка представляют связующие на уровне объекта. Таким образом, стандартные теоремы, такие как подстановка с сохранением типа и альфа-преобразование, предоставляются «бесплатно».

Twelf использовался для формализации множества различных логик и языков программирования (примеры включены в дистрибутив). Среди более крупных проектов — доказательство безопасности Standard ML , ^[2] базовая система типизированного ассемблера от CMU, ^[3] и фундаментальную кодовую систему доказательств из Принстона.

Реализация [ править ]

Twelf написан на стандартном ML, доступны двоичные файлы для Linux и Windows. По состоянию на 2006 год ^[update], он находится в стадии активной разработки, в основном в Университете Карнеги-Меллон.

См. также [ править ]

Список помощников по проверке

Ссылки [ править ]

^ Пфеннинг, Фрэнк; Карстен Шюрманн (июль 1999 г.). Описание системы: Twelf - металогическая основа дедуктивных систем (PDF) . Материалы 16-й Международной конференции по автоматизированному дедукции (CADE-16) . Проверено 8 мая 2019 г.
^ Ли, Дэниел; Карл Крэри; Роберт Харпер (январь 2007 г.). На пути к механизированной метатеории стандартного машинного обучения (PDF) . Материалы симпозиума 2007 года по принципам языков программирования . Ницца , Франция . Проверено 8 февраля 2007 г.
^ Крери, Карл (2003). На пути к базовому типизированному ассемблеру (PDF) . Материалы симпозиума 2003 года по принципам языков программирования . Проверено 8 февраля 2007 г.

Внешние ссылки [ править ]

Официальный сайт , Вики

[1] Пфеннинг, Фрэнк; Карстен Шюрманн (июль 1999 г.). Описание системы: Twelf - металогическая основа дедуктивных систем (PDF) . Материалы 16-й Международной конференции по автоматизированному дедукции (CADE-16) . Проверено 8 мая 2019 г.

[2] Ли, Дэниел; Карл Крэри; Роберт Харпер (январь 2007 г.). На пути к механизированной метатеории стандартного машинного обучения (PDF) . Материалы симпозиума 2007 года по принципам языков программирования . Ницца , Франция . Проверено 8 февраля 2007 г.

[3] Крери, Карл (2003). На пути к базовому типизированному ассемблеру (PDF) . Материалы симпозиума 2003 года по принципам языков программирования . Проверено 8 февраля 2007 г.

[1]

[2]

[3]