Agda


Agda
Agda
Класс языка:

функциональный, доказыватель теорем[en]

Автор(ы):

Ульф Норелл

Релиз:

2.3.2 (12 ноября 2012)

Типизация данных:

статическая, строгая, зависимая

Испытал влияние:

Haskell, Coq, Epigram (англ.)русск.

Сайт:

Agda wiki

Agda — чистый функциональный язык программирования с зависимыми типами, то есть типами, которые могут быть индексированы значениями другого типа. Теоретической основой Agda служит интуиционистская теория типов Мартин-Лёфа (англ.), которая расширена набором конструкций, полезных для практического программирования.

Agda также является системой автоматического доказательства. Логические высказывания записываются как типы, а доказательствами являются программы соответствующего типа.

Agda поддерживает индуктивные типы данных, сопоставление с образцом (гибко использующее наличие зависимых типов), систему параметризованных модулей, проверку завершаемости программ (англ.)русск., миксфиксный синтаксис для операторов. Поддержка неявных аргументов приводит к существенному упрощению программирования с зависимыми типами. Для программ на Agda характерно широкое использование Юникода.

В стандартную реализацию Agda входит расширение редактора Emacs, позволяющее осуществлять инкрементальное построение программ. Система проверки типов языка дает программисту полезную информацию о ещё не написанных частях программы.

Конкретный синтаксис языка Agda весьма близок к синтаксису Haskell, на котором система Agda и реализована.

Примеры

Натуральные числа и их сложение

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat
_+_ : Nat -> Nat -> Nat
zero  + m = m
suc n + m = suc (n + m)

Пример зависимого типа: список, в типе которого хранится натуральное число — его длина

data Vec (A : Set) : Nat -> Set where
  []   : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

Безопасная функция вычисления головы списка, не позволяющая выполнять эту операцию над пустым списком (нулевой длины):

head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
head (x :: xs) = x

Ссылки



Wikimedia Foundation. 2010.

Смотреть что такое "Agda" в других словарях:

  • agda — àgda ž <G mn ágdā/ ī> DEFINICIJA reg. 1. ukuhani šećer 2. bombon od ukuhanog, topljenog šećera; karamela ETIMOLOGIJA tur. aǧda ← arap. ̔aqīd: spojen, vezan …   Hrvatski jezični portal

  • Agda — may refer to * A minor character from The Hitchhiker s Guide to the Galaxy * The Agda (theorem prover) …   Wikipedia

  • ağda — is., Ar. ˁaḳīde 1) Kaynatılarak çok koyu ve yapışkan bir macun durumuna getirilen pekmez veya limonlu şeker eriyiği 2) Şekerle yapılan ürünlerin hazırlanması veya beklemesi sırasında şekerin ulaştığı koyuluk Atasözü, Deyim ve Birleşik Fiiller… …   Çağatay Osmanlı Sözlük

  • AGDA — abbr. Automated Grants Documentation System …   Dictionary of abbreviations

  • AĞDA — Bir kapta karıştırılıp pişirilerek koyulaşmış ve lüzucet kazanmış her nevi şeker vesaire …   Yeni Lügat Türkçe Sözlük

  • ağda — pekmeze un katılarak elde edilen tatlı …   Beypazari ağzindan sözcükler

  • Agda (theorem prover) — Agda is a theorem prover, i.e. a computer program that can check mathematical proofs. More specifically, it is an interactive system for developing constructive proofs in a variant of Per Martin Löf s Type Theory. It can also be seen as a… …   Wikipedia

  • Agda Michelsdotter — Agda Michelsdotter, known as Liten Agda and Olof Tyste , (fl. c. 1523 1526), was couple in a legend which was to have happened in Sweden in c. 1523 27, during the very first years of king Gustav Vasa (1523 1560) and the last years of Catholic… …   Wikipedia

  • Agda Persdotter — or Agda i Porten, (d. after 1565), was a Swedish woman, main royal mistress of King Eric XIV of Sweden during his time as a Crown Prince and during the first years of his reign 1560 1565. Biography Agda Persdotter is believed to have been the… …   Wikipedia

  • Agda Lund Bed & Breakfast — (Чивик,Швеция) Категория отеля: Адрес: Kiviks stora väg 59, 27721 Чивик, Швеция …   Каталог отелей


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.