Вопросы по теме 'agda'
Различия между Агдой и Идрисом
Я начинаю погружаться в программирование с зависимой типизацией и обнаружил, что языки Agda и Idris наиболее близки к Haskell, поэтому я начал с них.
У меня вопрос: в чем основные различия между ними? Являются ли системы типов одинаково...
22390 просмотров
schedule
10.11.2021
splitAt равноправие в Агде
Как можно доказать это равенство
≡splitAt : {α : Level} {A : Set α} {l₁ l₂ : Nat}
-> (xs₁ : Vec A l₁)
-> (xs₂ : Vec A l₂)
-> (xs₁ , xs₂ , refl) ≡ splitAt l₁ (xs₁ ++ xs₂)
? Базовый случай очевиден...
133 просмотров
schedule
23.10.2021
Как эффективно использовать автоматический поиск доказательств Agda?
При написании доказательств я заметил, что автоматический поиск доказательств Agda часто не находит решений, которые мне кажутся очевидными. К сожалению, создание небольшого примера, иллюстрирующего проблему, кажется трудным, поэтому я пытаюсь вместо...
1292 просмотров
schedule
02.10.2021
Экземпляры функторов и монад, которые проверяют завершение
Это следует за другим вопросом , заданным несколько месяцев назад. Проблема связана с проверкой завершения в Agda с использованием размерных типов.
Вот преамбула:
{-# OPTIONS --sized-types #-}
module Term where
open import Data.Empty...
85 просмотров
schedule
06.10.2021
Как сравнить два комплекта в Агде?
Я хочу написать функцию, которая принимает набор в качестве входных данных, и return true if it is top and false if it is bottom. я пробовал таким образом ..
isTop : Set → Bool
isTop x = if (x eq ⊤) then true
else false
Но я...
416 просмотров
schedule
27.11.2021
Докажите, что m ≤ n - ›k ≤ l -› m + k ≤ n + l в Agda.
Я хочу доказать
{m n k l : ℕ} -> m ≤ n -> k ≤ l -> m + k ≤ n + l
в Агде. Я могу доказать m + k ≤ m + l следующим кодом
add≤ : {m n : ℕ} -> (k : ℕ) -> m ≤ n -> k + m ≤ k + n
add≤ zero exp = exp
add≤ (suc k) exp = s≤s...
131 просмотров
schedule
22.11.2021
Как извлечь второй элемент сигмы в исчислении построений?
Я пытаюсь сделать это следующим образом:
λ (A : *) ->
λ (B : (A -> *)) ->
λ (t : (∀ (r : *) -> (∀ (x : a) -> (B x) -> r)) -> r) ->
(t (B (t A (λ (x : A) -> λ (y : (B x)) -> x)))
(λ (x : A) -> λ (y : (B x))...
317 просмотров
schedule
31.10.2021
Почему мое определение не допускается из-за строгой положительности?
У меня есть два следующих определения, которые приводят к двум различным сообщениям об ошибках. Первое определение отклоняется из-за строгой положительности, а второе - из-за непоследовательности вселенной.
(* non-strictly positive *)
Inductive...
1180 просмотров
schedule
01.11.2021
Что является допустимой сигнатурой типа для упражнения Any-?
#### Exercise `Any-∃`
Show that `Any P xs` is isomorphic to `∃[ x ∈ xs ] P x`.
Не говоря уже о том, что ∃[ x ∈ xs ] P x даже не допустимого синтаксиса - допустимым может быть только Σ[ x ∈ xs ] P x , ни одна из сигнатур типа, которые я...
70 просмотров
schedule
09.09.2021
Понимание неразрешенных метапеременных и желтого выделения в agda
В документации agda я читал, что когда «некоторая метапеременная, отличная от целей, не может быть решена, код будет выделен желтым цветом»
Я пытаюсь понять это в несколько вырожденном случае.
Если я определю обычный тип продукта, то глупая...
106 просмотров
schedule
08.09.2021
Пути и эквивалентности в кубическом agda для конкретного вычислительного поведения
Я работаю в Cubical agda и пытаюсь создать несколько общих утилит для последующих проверок. Одна из них заключается в том, что для любого типа A он «то же самое», что и тип Σ A (\_ -> Top) , где Top - это тип с одним элементом. И вопрос в...
41 просмотров
schedule
17.11.2021
Общее программирование с помощью эффектов
В библиотеке эффектов Idris Effects есть представлен как
||| This type is parameterised by:
||| + The return type of the computation.
||| + The input resource.
||| + The computation to run on the resource given the return value.
Effect : Type...
1740 просмотров
schedule
20.02.2022
Завершение проверки при объединении списков
Agda 2.3.2.1 не видит, что следующая функция завершается:
open import Data.Nat
open import Data.List
open import Relation.Nullary
merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _...
495 просмотров
schedule
03.03.2022
Застрял на доказательстве с неоднородным равенством
У меня есть представление двоичного числа, плюс некоторое преобразование в Nat и обратно:
open import Data.Nat
open import Data.Nat.Properties
open import Function
open import Relation.Binary.PropositionalEquality hiding (trans; cong; subst; sym)...
698 просмотров
schedule
26.02.2022
Регрессия Agda 2.4.0.x при завершении проверки
Следующий код завершения проверяет Agda 2.3.2.2, но не 2.4.0.x:
open import Data.Nat
open import Relation.Binary.PropositionalEquality
+-comm : ∀ a b → a + b ≡ b + a
+-comm zero zero = refl
+-comm zero (suc b) = cong suc (+-comm zero b) -- this...
52 просмотров
schedule
03.03.2022
Простое кодирование категории наборов и функций в Agda
Это очень простой вопрос по Agda и теории категорий. Я хочу закодировать категорию, в которой объекты представляют собой конечные множества, а стрелки - функции между ними. Я использую репозиторий agda / agda-Categories для определения Category ....
124 просмотров
schedule
10.03.2022
Проверка завершения не работает после абстрагирования сайта вызова
Проблема
У меня есть простая коиндуктивная запись с единственным полем типа суммы. Unit дает нам простой тип, с которым можно поиграть.
open import Data.Maybe
open import Data.Sum
data Unit : Set where
unit : Unit
record Stream : Set...
143 просмотров
schedule
12.03.2022
Парное равенство в agda
У меня есть следующий код, который я хочу доказать:
data Pair (A : Set) (B : A → Set) : Set where
pair : (a : A) → (B a) → Pair A B
pairEq : (A : Set) → (B : A → Set) → (a : A) → (b₁ b₂ : B a) → (pair {A} {B} a b₁ ≡ pair {A} {B} a b₂) → b₁ ≡...
112 просмотров
schedule
20.03.2022
Упрощение булевых логических выражений до DNF и CNF (в Haskell)
Я понимаю, что существуют общепринятые алгоритмы приведения заданного булево-логического выражения к КНФ или ДНФ. Я нашел несколько веб-сайтов об этом, но ничего такого, что я мог бы использовать для создания программы на Haskell вокруг этого.
Это...
1696 просмотров
schedule
31.03.2022
Что это за ошибка Agda?
Я впервые пробую Agda и определил тип данных Bool и его основные функции, как говорится во всех руководствах:
data Bool : Set where
true : Bool
false : Bool
not : Bool -> Bool
not true = false
not false = true
etc...
Когда я пытаюсь...
88 просмотров
schedule
31.03.2022
