Вопросы по теме 'agda'
Строго позитивно в Агде
Я пытаюсь закодировать некоторую денотационную семантику в Agda на основе программы, которую я написал на Haskell.
data Value = FunVal (Value -> Value)
| PriVal Int
| ConVal Id [Value]
| Error String
В...
3574 просмотров
schedule
24.09.2023
Агда, логическое предложение
В предисловии обратите внимание, что это для задания. Вопрос по первому вопросу уже задан. Итак, у нас есть тип данных:
data BoolProp : ??? where
ptrue : BoolProp true
pfalse : BoolProp false
pand : (P Q : Bool) -> (BoolProp P) ->...
496 просмотров
schedule
03.01.2023
Agda: функция запуска для примера стека Конора
На ICFP 2012 Конор МакБрайд выступил с программным докладом «Агда-любопытно?».
В нем была реализована небольшая стековая машина.
Видео находится на YouTube: http://www.youtube.com/watch?v=XGyJ519RY6Y
Код также находится в сети:...
617 просмотров
schedule
10.06.2023
Схемы рекурсии в Agda
Излишне говорить, что стандартная конструкция в Haskell
newtype Fix f = Fix { getFix :: f (Fix f) }
cata :: (Functor f) => (f a -> a) -> Fix f -> a
cata f = f . fmap (cata f) . getFix
это здорово и очень полезно.
Пытаюсь...
1058 просмотров
schedule
10.10.2022
Иерархия типов в Agda
Я пытаюсь понять, как иерархии типов работают в Agda.
Предполагая, что я определяю тип набора X:
X : Set
а затем приступить к построению индуктивного типа
data Y : X -> Set where
Какой тип X -> Set ? Это набор или тип?...
945 просмотров
schedule
07.06.2022
неразрешенные мета-данные при определении записи в Agda
Рассмотрим следующий код:
module UnresolvedMeta where
record Test (M : Set) : Set1 where
field
_≈_ : M -> M -> Set
_⊕_ : M -> M -> M
assoc⊕ : ∀ {r s t} -> ((r ⊕ s) ⊕ t) ≈ (r ⊕ (s ⊕ t))
data ℕ : Set where...
179 просмотров
schedule
19.02.2023
Как определить одноэлементный набор?
Предположим, у меня есть значение x : A , и я хочу определить набор, содержащий только x .
Вот что я пробовал:
open import Data.Product
open import Relation.Binary.PropositionalEquality
-- Singleton x is the set that only contains x. Its...
706 просмотров
schedule
08.08.2023
Завершение проверки функции по дереву
Мне трудно убедить Agda выполнить проверку завершения функции fmap ниже и аналогичных функций, определенных рекурсивно в структуре Trie . Trie - это дерево , домен которого является Type , тип уровня объекта, состоящий из единицы, продуктов...
181 просмотров
schedule
18.05.2023
Ошибка типа Agda
Я новичок в Agda и пытаюсь определить константу prod типа: Z → (Z → ((Z → Set) → Set))
Теперь я написал следующий код Agda:
data Prod (X : Set) : ℕ → X where
prod : ℕ → (ℕ → ((ℕ → X) → X))
Когда я проверяю тип, agda выдает следующее...
371 просмотров
schedule
03.05.2022
Недостаточно оцененный контекст внутри предложения `with`
Я застрял на следующем доказательстве.
module Temp where
open import Data.Empty
open import Data.Fin hiding (compare)
open import Data.Nat hiding (compare); open import Data.Nat.Properties
open import Function
open import Level...
48 просмотров
schedule
10.04.2022
Разница между параметрами типа и индексами?
Я новичок в зависимых типах, и меня смущает разница между ними. Кажется, люди обычно говорят, что тип параметризуется другим типом и индексируется некоторым значением . Но разве нет различия между типами и терминами в языке с зависимой...
3134 просмотров
schedule
26.09.2022
Понимание синтаксиса Agda
Используя следующее в качестве примера
postulate DNE : {A : Set} → ¬ (¬ A) → A
data ∨ (A B : Set) : Set where
inl : A → A ∨ B
inr : B → A ∨ B
-- Use double negation to prove exclude middle
classical-2 : {A : Set} → A ∨ ¬ A
classical-2 = λ...
754 просмотров
schedule
16.04.2022
Как работать с потоком в agda?
Я написал потоковый тип данных и одну головную операцию в Agda. Теперь я хочу проверить правильность работы головки.
Итак, я принимаю свой входной поток как 1 :: 2 :: 3 ::. . . Но agda не принимает это как поток.
Итак, мой вопрос в том, как...
295 просмотров
schedule
05.02.2023
Проблемы с индексами типов данных, в которых используется конкатенация списков
У меня возникла неприятная проблема с формализацией теоремы, которая использует тип данных, у которого есть некоторые конструкторы, индексы которых имеют конкатенацию списков. Когда я пытаюсь использовать режим emacs для разделения регистра, Agda...
383 просмотров
schedule
22.04.2023
Неожиданный уровень вселенной
Вот определение, подобное тому, что в Data.List.All :
open import Data.Vec
data All {α π} {A : Set α} (P : A -> Set π) : ∀ {n} -> Vec A n -> Set π where
[]ₐ : All P []
_∷ₐ_ : ∀ {n x} {xs : Vec A n} -> P x -> All P xs ->...
81 просмотров
schedule
04.01.2023
Как пронумеровать элементы списка по `Fin`s за линейное время?
Мы можем перечислить элементы списка следующим образом:
-- enumerate-ℕ = zip [0..]
enumerate-ℕ : ∀ {α} {A : Set α} -> List A -> List (ℕ × A)
enumerate-ℕ = go 0 where
go : ∀ {α} {A : Set α} -> ℕ -> List A -> List (ℕ × A)
go n []...
517 просмотров
schedule
24.07.2022
Зачем нужны контейнеры?
(В качестве оправдания: заголовок имитирует заголовок Зачем нам нужны монады? )
Существуют контейнеры (и проиндексированные ) (и хазохистские ) и описания . Но контейнеры проблемны , и, судя по моему небольшому опыту, мне труднее думать с...
1301 просмотров
schedule
12.05.2023
Как установить agda-mode на OSX El Capitan?
Пытаюсь установить agda-mode на OSX. Я следовал официальному руководству (пробовал и несколько других), но, похоже, не могу заставить его работать.
При загрузке Emacs / Aquamacs я получаю следующую ошибку:
Warning (initialization): An error...
483 просмотров
schedule
02.04.2024
Равенство по зависимым типам записей
Некоторое время я ломал голову над этой проблемой: у меня есть типы записей с зависимыми полями, и я хочу доказать равенство при преобразованиях записей. Я попытался выразить суть моей проблемы в небольшом примере. Рассмотрим следующий тип записи...
447 просмотров
schedule
20.04.2022
Можно ли создать представление общих АТД на уровне типов?
Используя кодировку Черча, можно представить любой произвольный алгебраический тип данных без использования встроенной системы АТД. Например, Nat можно представить (пример в Идрисе) как:
-- Original type
data Nat : Type where
natSucc : Nat...
231 просмотров
schedule
12.12.2023
