Twelf: Логический фреймворк LF для формализации теории языков программирования.
Twelf
Twelf: логическое программирование и теория языков. Реализация логической основы LF от CMU. Объявление типов, констант и определение натуральных чисел.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Twelf — это реализация логической структуры LF, разработанная Фрэнком Пфеннингом и Карстеном Шюрманном в Университете Карнеги — Меллона. Она используется для логического программирования и формализации теории языков программирования.
Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University. It is used for logic programming and for the formalization of programming language theory.
Введение
В самом простом виде программа Twelf (называемая "подписью") представляет собой коллекцию деклараций семейств типов (отношений) и констант, которые принадлежат этим семействам типов. Например, ниже приведено стандартное определение натуральных чисел, где `z` обозначает ноль, а `s` – оператор следования. `nat : type. z : nat. s : nat > nat`. Здесь `nat` – это тип, а `z` и `s` – константные термы. Поскольку Twelf – зависимо типизированная система, типы могут быть индексированы термами, что позволяет определять более интересные семейства типов. Вот определение сложения:
At its simplest, a Twelf program (called a "signature") is a collection of declarations of type families (relations) and constants that inhabit those type families. For example, the following is the standard definition of the natural numbers, with standing for zero and the successor operator. nat : type. z : nat. s : nat > nat. Here is a type, and and are constant terms. As a dependently typed system, types can be indexed by terms, which allows the definition of more interesting type families. Here is a definition of addition:
`plus : nat > nat > nat > type. plus zero : {M:nat} plus M z M.`
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 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`. Этот рекурсивный вызов осуществляется через подцель, вводимую с помощью `<`. Стрелка `>` может быть понята оперативно как `:-` в Prolog, или как логическое следование ("если `M + N = P`, то `M + (s N) = (s P)`"), или, наиболее точно с точки зрения теории типов, как тип константы `plus` ("при задании терма типа `nat > nat > nat`, возвращает терм типа `type`"). Twelf поддерживает реконструкцию типов и неявные параметры, поэтому на практике обычно не нужно явно указывать `{M:nat}` (и т.д.) над определением. Эти простые примеры не демонстрируют возможности LF высшего порядка и не показывают его возможности проверки теорем. Обратитесь к дистрибутиву Twelf для ознакомления с включенными примерами.
The type family is read as a relation between three natural numbers , and , such that We then give the constants that define the relation: the constant indicates that The quantifier can be read as "for all of type ". The constant defines the case for when the second argument is the successor of some other number (see pattern matching). The result is the successor of , where is the sum of and This recursive call is made via the subgoal , introduced with The arrow can be understood operationally as Prolog's , or as logical implication ("if M + N = P, then M + (s N) = (s P)"), or most faithfully to the type theory, as the type of the constant ("when given a term of type , return a term of type "). Twelf features type reconstruction and supports implicit parameters, so in practice, one usually does not need to explicitly write (etc.) above. These simple examples do not display LF's higher order features, nor any of its theorem checking capabilities. See the Twelf distribution for its included examples.
Применение
Двенадцать используется несколькими различными способами.
Twelf is used in several different ways.
Логическое программирование
Двенадцать подписей могут быть выполнены посредством процедуры поиска. Его ядро сложнее, чем у Prolog, поскольку оно является языком высшего порядка с зависимой типизацией, но ограничено чистыми операторами: в нем отсутствует оператор "cut" и другие экстралогические операторы (например, для выполнения операций ввода-вывода), которые часто встречаются в реализациях Prolog, что может снизить его пригодность для практических задач логического программирования. Некоторые применения правила "cut" в Prolog можно реализовать, объявив определенные операторы принадлежащими к детерминированным семействам типов, что позволяет избежать повторных вычислений. Кроме того, как и в λProlog, Twelf обобщает предложения Хорна до наследственных формул Харропа, что обеспечивает логически обоснованные операционные концепции генерации новых имен и расширения базы данных предложений с учетом области видимости.
Twelf signatures can be executed via a search procedure. Its core is more sophisticated than Prolog, since it is higher order and dependently typed, but it is restricted to pure operators: there is no cut or other extralogical operators (such as ones for performing I/O) as are often found in Prolog implementations, which may make it less well suited for practical logic programming applications. Some uses of Prolog's cut rule can be obtained by declaring that certain operators belong to deterministic type families, which avoids recalculation. Also, like λProlog, Twelf generalizes Horn clauses to hereditary Harrop formulas, which allow for logically well founded operational notions of fresh name generation and scoped extension of the clause database.
Формализация математики
Сегодня Twelf используется главным образом как система для формализации математики, особенно метатеории языков программирования. В связи с этим, он тесно связан с Coq и Isabelle/HOL/HOL Light. Однако, в отличие от этих систем, доказательства в Twelf обычно разрабатываются вручную. Несмотря на это, для тех областей задач, в которых Twelf особенно силен, доказательства часто получаются короче и проще в разработке, чем в автоматизированных системах общего назначения. Встроенное в Twelf понятие связывания и подстановки облегчает кодирование языков программирования и логик, большинство из которых используют связывание и подстановку, которые часто можно непосредственно закодировать с помощью синтаксиса высшего порядка (HOAS), где связующие мета-языка представляют связующие объектного уровня. Таким образом, стандартные теоремы, такие как сохраняющая тип подстановка и альфа-преобразование, предоставляются "из коробки". Twelf использовался для формализации многих различных логик и языков программирования (примеры включены в дистрибутив). Среди крупных проектов — доказательство безопасности для Standard ML, фундаментальная типизированная система ассемблера от CMU и фундаментальная система доказательства корректности кода от Принстона.
Twelf is mainly used today as a system for formalizing mathematics, especially the metatheory of programming languages. As such, it is closely related to Coq and Isabelle/HOL/HOL Light. However, unlike those systems, Twelf proofs are typically developed by hand. Despite this, for the problem domains at which it excels, Twelf proofs are often shorter and easier to develop than in the automated, general purpose systems. Twelf's built in notion of binding and substitution facilitates the encoding of programming languages and logics, most of which make use of binding and substitution, which can often be directly encoded through higher order abstract syntax (HOAS), where the meta language's binders represent the object level binders. Thus standard theorems such as type preserving substitution and alpha conversion come "for free". Twelf has been used to formalize many different logics and programming languages (examples are included with the distribution). Among the larger projects are a proof of safety for Standard ML, a foundational typed assembly language system from CMU, and a foundational proof carrying code system from Princeton.
Реализация
Twelf написан на Standard ML, и бинарные файлы доступны для Linux и Windows. Он активно разрабатывается, преимущественно в Университете Карнеги — Меллона.
Twelf is written in Standard ML, and binaries are available for Linux and Windows. , it is under active development, mostly at Carnegie Mellon University.