Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Агда
Стилизованный цыпленок в черных линиях и точках слева от имени «Agda» без засечек, первая буква наклонена вправо.
ПарадигмаФункциональный
РазработаноУльф Норелл; Катарина Кокванд (1.0)
РазработчикУльф Норелл; Катарина Кокванд (1.0)
Впервые появился2007 ; 14 лет назад (1,0 в 1999 г . ; 22 года назад ) ( 2007 ) ( 1999 )
Стабильный выпуск
2.6.1 / 16 марта 2020 г . ; 13 месяцев назад ( 2020-03-16 )
Печатная дисциплинасильный , статический , зависимый , номинальный , явный , предполагаемый
Язык реализацииHaskell
Операционные системыКроссплатформенность
ЛицензияBSD-подобный [1]
Расширения имени файла.agda, .lagda, .lagda.md, .lagda.rst,.lagda.tex
Веб-сайтwiki .portal .chalmers .se / agda
Под влиянием
Coq , эпиграмма , Haskell
Под влиянием
Идрис

Agda - это функциональный язык программирования с зависимой типизацией, первоначально разработанный Ульфом Нореллом из Технологического университета Чалмерса, реализация которого описана в его докторской диссертации. [2] Оригинальная система Agda была разработана в Chalmers Катариной Кокванд в 1999 году. [3] Текущая версия, первоначально известная как Agda 2, представляет собой полностью переписанный язык, который следует рассматривать как новый язык, имеющий общее название и традиции.

Agda также является помощником по проверке, основанным на парадигме предложений как типов , но, в отличие от Coq , не имеет отдельного языка тактик , а доказательства написаны в стиле функционального программирования. В языке есть обычные программные конструкции, такие как типы данных , сопоставление с образцом , записи , let-выражения и модули, а также синтаксис, подобный Haskell . Система имеет интерфейсы Emacs и Atom [4] [5], но также может запускаться в пакетном режиме из командной строки.

Agda основана на единой теории зависимых типов (UTT) Чжаохуэй Луо [6], теории типов, подобной теории типов Мартина-Лёфа .

Agda назван в честь шведской песни «Хонан Агда», написанной Корнелис Вресвик , [7] , который про курица по имени Agda. Это намекает на название Coq .

Особенности [ править ]

Индуктивные типы [ править ]

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

Вот определение чисел Пеано в Агде:

 Данные ℕ :  Установить ,  где  ноль  : ℕ SUC  : ℕ → ℕ

По сути, это означает, что есть два способа создать значение типа ℕ, представляющее натуральное число. Для начала, zeroэто натуральное число, и если nэто натуральное число, то suc n, стоя на преемнику из n, является натуральным числом тоже.

Вот определение отношения «меньше или равно» между двумя натуральными числами:

 данные _≤_ : ℕ → ℕ →  Установить,  где  z≤n  :  { n : ℕ }  → ноль ≤ n s≤s  :  { nm : ℕ }  → n ≤ m → su n ≤ suc m

Первый конструктор z≤nсоответствует аксиоме, согласно которой ноль меньше любого натурального числа или равен ему. Второй конструктор s≤sсоответствует правилу вывода, позволяющему превратить доказательство n ≤ mв доказательство suc n ≤ suc m. [8] Таким образом, значение s≤s {zero} {suc zero} (z≤n {suc zero})является доказательством того, что единица (преемник нуля) меньше или равна двум (преемник единицы). Параметры, указанные в фигурных скобках, могут быть опущены, если они предполагаются.

Зависимо типизированное сопоставление с образцом [ править ]

В теории основных типов принципы индукции и рекурсии используются для доказательства теорем об индуктивных типах . В Agda вместо этого используется сопоставление шаблонов с зависимым типом. Например, сложение натуральных чисел можно определить так:

добавить ноль n = n добавить ( успех ) п = успех ( добавить мн )

Такой способ написания рекурсивных функций / индуктивных доказательств более естественен, чем применение принципов простой индукции. В Agda сопоставление с образцом с зависимым типом является примитивом языка; в базовом языке отсутствуют принципы индукции / рекурсии, на которые переводится сопоставление с образцом.

Метапеременные [ править ]

Одной из отличительных особенностей Agda по сравнению с другими подобными системами, такими как Coq , является сильная зависимость от метапеременных при построении программ. Например, в Agda можно написать такие функции:

 добавить  : ℕ → ℕ → ℕ добавить xy =  ?

?вот метапеременная. При взаимодействии с системой в режиме emacs он покажет ожидаемый тип пользователя и позволит ему уточнить метапеременную, то есть заменить ее более подробным кодом. Эта функция позволяет создавать инкрементные программы аналогично тактическим помощникам по доказательствам, таким как Coq.

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

Программирование в чистой теории типов требует множества утомительных и повторяющихся доказательств. Хотя в Agda нет отдельного языка тактик, можно запрограммировать полезные тактики внутри самой Agda. Обычно это работает путем написания функции Agda, которая, возможно, возвращает доказательство некоторого интересующего свойства. Затем тактика создается путем запуска этой функции во время проверки типов, например, с использованием следующих вспомогательных определений:

 data Maybe ( A :  Set )  :  Установить,  где  Just  : A → Maybe A Nothing  : Maybe A data isJust { A :  Set }  : Возможно A →  Установить,  где  auto  :  ∀  { x }  → isJust ( Просто x ) Тактика  :  ∀  { A :  Set }  ( x : Maybe A )  → isJust x → A Тактика Ничего () Тактика ( Просто x ) auto = x

Для функции, check-even : (n : ℕ) → Maybe (Even n)которая вводит число и, при необходимости, возвращает доказательство его четности, тактика может быть построена следующим образом:

 тактика проверки четности  :  { n : ℕ }  → isJust ( проверка четности n )  → четность n check-even-tactic { n }  = Тактика ( чек-даже n ) лемма0  : Даже ноль lemma0 = автоматическая проверка четности лемма 2  : Even ( success ( success zero )) лемма 2 = проверка- четность -тактика авто

Фактическое доказательство каждой леммы будет автоматически построено во время проверки типов. Если тактика не удалась, проверка типов не удастся.

Кроме того, для написания более сложных тактик Agda поддерживает автоматизацию через отражение . Механизм отражения позволяет заключать фрагменты программы в кавычки или извлекать их из абстрактного синтаксического дерева. Способ использования отражения аналогичен тому, как работает Template Haskell. [9]

Другой механизм для автоматизации проверки - это действие поиска доказательства в режиме emacs. Он перечисляет возможные условия подтверждения (ограниченный 5 секундами), и, если один из терминов соответствует спецификации, он будет помещен в мета-переменную, в которой вызывается действие. Это действие принимает подсказки, например, какие теоремы и из каких модулей можно использовать, может ли действие использовать сопоставление с образцом и т. Д. [10]

Проверка прекращения [ править ]

Agda - это тотальный язык , т. Е. Каждая программа в нем должна завершаться, и все возможные шаблоны должны быть сопоставлены. Без этой функции логика языка становится непоследовательной, и становится возможным доказывать произвольные утверждения. Для проверки прерывания Agda использует метод проверки прерывания плодов. [11]

Стандартная библиотека [ править ]

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

Юникод [ править ]

Одна из наиболее заметных особенностей Agda - это сильная зависимость от Unicode в исходном коде программы. Стандартный режим emacs использует ярлыки для ввода, например, \Sigmaдля Σ.

Бэкэнды [ править ]

Есть два бэкэнда компилятора, MAlonzo для Haskell и один для JavaScript .

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

  • Coq
  • HOL (помощник проверки)
  • Идрис (язык программирования)
  • Изабель (помощник по пруфу)

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

  1. ^ Файл лицензии Agda
  2. ^ Ульф Норелл. К практическому языку программирования, основанному на теории зависимых типов. Кандидатская диссертация. Технологический университет Чалмерса, 2007 г. [1]
  3. ^ «Agda: интерактивный редактор доказательств» . Архивировано из оригинала на 2011-10-08 . Проверено 20 октября 2014 .
  4. ^ Кокванд, Катарина; Синек, Дэн; Такеяма, Макото. Интерфейс Emacs для поддержки создания доказательств и программ, ориентированных на типы (PDF) . European Joint Conferences on Theory and Practice of Software 2005. Архивировано из оригинала (PDF) 22.07.2011.
  5. ^ "agda-mode на Атоме" . Проверено 7 апреля 2017 года .
  6. ↑ Ло, Чжаохуэй. Вычисления и рассуждения: теория типов для информатики . Oxford University Press, Inc., 1994.
  7. ^ "[Agda] происхождение" Agda "? (Список рассылки Agda)" . Дата обращения 24 октября 2020 .
  8. ^ "Nat из стандартной библиотеки Agda" . Проверено 20 июля 2014 .
  9. ^ Van Der Уолт, Пол и Wouter Swierstra. «Инженерное доказательство отражением в Агде». В реализации и применении функциональных языков , стр. 157-173. Springer Berlin Heidelberg, 2013. [2]
  10. ^ Kokke, Pepijn и Wouter Swierstra. «Авто в Агде».
  11. ↑ Абель, Андреас. «плод - Завершение проверки простых функциональных программ». Отчет лаборатории программирования 474 (1998). [3]

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

  • Официальный веб-сайт
  • Зависимо типизированное программирование в Agda , Ульф Норелл
  • Краткий обзор Агды , написанный Аной Бове, Питером Дибджером и Ульфом Нореллом
  • Знакомство с Agda , плейлистом на YouTube из пяти частей от Дэниела Пиблза
  • Жесткое [мета] введение в зависимые типы в Agda
  • Учебное пособие по Agda: «Изучите программирование в Agda без теоретической подготовки»