Описание тега agda
Agda - это полностью функциональный язык программирования с зависимой типизацией и помощник по проверке.
1
ответ
Лучший способ написать конструкторы как функции в Agda
У меня есть список data List (X : Set) : Set where <> : List X _,_ : X -> List X -> List X определение равенства data _==_ {l}{X : Set l}(x : X) : X -> Set l where refl : x == x и конгруэнтность cong : forall {k l}{X : Set k}{Y : Set …
23 ноя '14 в 19:41
1
ответ
Какие размеры в Агде?
Какие размеры в Агде? Я пытался прочитать статью о MiniAgda, но не смог продолжить из-за следующих моментов: Почему типы данных являются общими для их размера? Насколько я знаю, размер - это глубина дерева индукции. Почему типы данных ковариантны от…
02 ноя '16 в 15:27
1
ответ
Завершение проверки замены через (монадическое) соединение и fmap
Я использую типоразмеры и имею функцию подстановки для типизированных терминов, которая проверяет завершение, если я даю определение напрямую, а не если я делаю его через (монадное) соединение и fmap. {-# OPTIONS --sized-types #-} module Subst where…
27 фев '14 в 07:44
1
ответ
Агда: Вектор Членство в Stdlib? (А как научить стдлиб вообще)
Я имею дело со строками в Агде, и у меня есть их вектор. Мне нужно проверить, встречается ли данная строка в векторе (как часть проверки, является ли переменная свободной или связанной в выражении, в теории PL, которую я делаю wprk). Я все еще пытаю…
06 мар '17 в 19:05
1
ответ
Экземпляры функтора и монады, которые проверяют завершение
Это следует за другим вопросом от нескольких месяцев назад. Проблема связана с проверкой завершения в Agda с использованием типоразмеров. Вот преамбула: {-# OPTIONS --sized-types #-} module Term where open import Data.Empty open import Function open…
12 авг '14 в 07:23
1
ответ
Как доказать, что существует рациональное, которое в агде меньше рационального?
Я хочу доказать, что существует рациональное, которое меньше рационального. например.. v : ℚ v = + 1 ÷ 2 thm : (Σ[ x ∈ ℚ ] (x Data.Rational.≤ v)) thm = ? Что писать во второй строке?? И в чем смысл x ∈ ℚ, даст ли он элемент из ℚ или что. И где он оп…
16 июн '15 в 08:50
1
ответ
Застрял на простом доказательстве равенства
Я пытаюсь реализовать некоторые матричные операции и доказательства вокруг них в Агде. Код включает в себя что-то около следующих определений: open import Algebra open import Data.Nat hiding (_+_ ; _*_) open import Data.Vec open import Relation.Bina…
03 сен '16 в 00:34
3
ответа
Логика высказываний и доказательства
Я пытаюсь доказать приведенный ниже случай для домашнего задания, и я работал над ним часами, но все же не повезло. r) -> p -> q -> r"> Любые предложения или комментарии относительно того, что я делаю неправильно?
17 фев '16 в 03:21
2
ответа
Как определить оператора деления в Агде?
Я хочу разделить два натуральных числа. Я сделал функцию, как это _/_ : N -> N -> frac m / one = m / one (suc m) / n = ?? I dont know what to write here. Пожалуйста помоги.
18 фев '15 в 10:54
1
ответ
Доказывая Агде, что мы говорим об одном и том же
Я пытаюсь доказать противоречие, но сталкиваюсь с проблемой, пытающейся доказать Agda, что тип домена сигмы, возвращаемый <>-wt-inv та же сигма, что и в предыдущем доказательстве. Я ожидаю, что доказательство uniq-типа должно помочь мне там, н…
07 апр '15 в 19:13
1
ответ
Доказательство конкатенации языка ассоциативно в Агде
Я новичок в языке Agda, и я работаю над формальными языками, используя Agda. У меня есть некоторые проблемы, когда доказательство объединения языков является ассоциативным. Доказательство будет выделено желтым цветом, так как Agda не смогла найти сл…
23 апр '17 в 16:22
2
ответа
Установка agda не удалась при дублировании объявлений экземпляров
Я пытаюсь дать Агде шанс, но не могу его установить. Я запускаю GHC 7.8.3 в песочнице Кабала. Failed to install Agda-2.4.0.1 Build log ( /Users/jsnavely/project/agda/.cabal-sandbox/logs/Agda-2.4.0.1.log ): [1 of 1] Compiling Main ( /var/folders/dh/c…
25 июл '14 в 21:07
2
ответа
Программы agda обязательно заканчиваются?
В нескольких местах было указано, что все программы agda завершаются. Однако я могу построить такую функцию: stall : ∀ n → ℕ stall 0 = 0 stall x = stall x Подсветка синтаксиса, кажется, не нравится, но нет ошибок компиляции. Вычисление нормальной …
12 авг '13 в 03:02
1
ответ
Небезопасный принудительный и более эффективный код Agda (-ftrust-me-im-agda)
В списке рассылки Agda Конор МакБрайд спросил: Есть ли способ получить операции, как предполагаемый trustFromJust :: Maybe x -> x который на самом деле не проверяет на справедливость и идет не так (в смысле Милнера), если ничего не кормит? Agda м…
03 окт '10 в 23:44
1
ответ
Знакомство с Lift и Setω, а также с появлением переменных в выражениях
В предыдущем вопросе у меня были типы для игрушечного языка data Type : Set where Nat : Type Prp : Type Я думал о том, чтобы интерпретировать их, используя несвязанный союзType → Set ⊎ Set₁, но подъем уровня мышления был бы лучшим и помог получить ⟦…
30 мар '16 в 18:22
1
ответ
Есть ли какой-нибудь нетривиальный код, который использует Data.Maybe.Is-just?
Стандартная библиотека Agda предоставляет тип данных Maybe в сопровождении с видом Any, Тогда есть свойство Is-just определяется с помощью Any, Мне было трудно работать с этим типом, так как стандартная библиотека не предоставляет никаких инструмент…
17 июн '15 в 06:58
1
ответ
Представление индуктивных типов
Я реализовал лямбда-исчисление с зависимой типизацией в духе этой статьи: http://www.andres-loeh.de/LambdaPi/LambdaPi.pdf Исчисление, работает, и я экспериментировал с ним и расширил несколько вещей: много вселенных, жестко закодированная индукция а…
12 мар '14 в 02:28
2
ответа
Библиотека категорий для Agda?
Существуют ли "рекомендуемые" библиотеки, которые обеспечивают удобную формализацию базовой теории категорий в Agda? Стандартная библиотека Agda, кажется, предоставляет очень мало в этом отношении. Я ищу что-то с низким барьером для входа, подобно т…
04 сен '14 в 07:49
1
ответ
Несоответствие уровня в Агде
Некоторые входы: module error where open import Data.Nat as ℕ open import Level open import Data.Vec open import Data.Vec.N-ary Эта функция создает тип функции из вектора типов и типа результата: N-Ary-from-Vec : {α γ : Level} {l : ℕ} -> Vec (Set…
26 янв '14 в 13:12
2
ответа
Проверка завершения на unionWith
У меня проблема с проверкой завершения, очень похожая на описанную в этом вопросе, а также на отчет об ошибке Agda / запрос функции. Проблема заключается в том, чтобы убедить компилятор в следующем unionWith завершается. Используя функцию комбиниров…
19 янв '14 в 11:54