Интернет магазин китайских планшетных компьютеров

Компьютеры - Coq - Язык

• Пользователь может вводить собственные аксиомы
• Основан на предикативном исчислениииндуктивных конструкций, что означает:
  • Все возможности исчисления конструкций:
  • Кумулятивная иерархия универсумов, состоящая из Prop, Set и множества Type, индексированного натуральными числами
  • Prop импредикативный, Set и Type предикативные
  • Индуктивные или алгебраические типы данных
  • Коиндуктивные типы данных
  • Возможно задать только общерекурсивные функции, то есть такие функции, вычисление которых останавливается, то есть не зацикливается. В Coq можно записать функцию Аккермана. Остановка рекурсии по индуктивным типам данных гарантируется синтаксической проверкой определения функции, называемой «guarded by destructors». Остановка функций, которые используют сопоставление по образцу коиндуктивных типов, гарантируется условием «guarded by contructors». Список литературы можно найти в , «Fixpoint definitions» и «Coinductive types».
  • Неявное приведение типов, или наследование
• Автоматический вывод типов
• Вывод значений аргументов из типов. Например, тип второго аргумента или результата функции f зависит от значения первого аргумента. Тогда значение первого аргумента можно вывести из типа второго аргумента или результата соответственно. Символ подчёркивания на месте аргумента указывает, что аргумент должен быть выведен автоматически. Если аргумент объявлен как неявный, его вообще можно опускать после имени функции. Coq может автоматически обнаруживать аргументы, которые имеет смысл объявить неявными
• Тактики можно писать на:
  • Языке программирования ML
  • Специальном языке для тактик Ltac
  • Coq, используя тактику quote
• Имеет обширный набор примитивных тактик и меньший набор развитых тактик для специфических теорий
• Тактики группы setoid для имитации фактормножеств: задаётся отношение эквивалентности; функции, сохраняющие это отношение; далее можно подставлять в термах эквивалентные значения
• Интегрированы классы типов а-ля-Haskell.
• Program и Russel для создания верифицированных программ из неверифицированных