4
ответа
доказательства о регулярных выражениях
Кто-либо знает какие-либо примеры следующего? Разработки доказательства о регулярных выражениях (возможно расширенный с помощью обратных ссылок) в помощниках доказательства (таких как Coq). Программы в зависимо введенном...
вопрос задан: 8 June 2009 13:03
1
ответ
Вызов функции в Агде
У меня есть этот код, который в основном является hello world, с функцией добавления, он компилирует и запускает и выводит «Hello, world 5!»: Открыть импорт данных Common.IO ℕ: установить где ноль: ℕ suc: ℕ → ...
вопрос задан: 26 March 2019 15:38
1
ответ
Как соединить строки в Agda
Я пытаюсь соединить строки на языке agda. Мой код до сих пор это открытый импорт Common.IO открытый импорт Common.String f: String → String f x = x main = putStrLn (f "Привет, мир!") Как я ...
вопрос задан: 3 March 2019 13:16
1
ответ
Agda, ключевое слово `with` и` refl` [duplicate]
TL; DR того, что я хочу: f с g f | constructor1 val = {!!} В контексте этой цели, как я могу получить что-то типа g ≡ constructor1 val? У меня есть следующее определение равенства: data _≡ ...
вопрос задан: 27 December 2014 13:45
1
ответ
Как выучить agda
Я пытаюсь выучить agda. Однако у меня возникла проблема. Все руководства, которые я нашел на вики-сайте agda, слишком сложны для меня и охватывают различные аспекты программирования. После параллельного чтения 3 ...
вопрос задан: 26 February 2012 18:20
1
ответ
Показ (голова. init), = направляются в Agda
Я пытаюсь доказать простую лемму в Agda, который я думаю, верно. Если вектор имеет больше чем два элемента, брать его голову после взятия init совпадает со взятием его головы сразу. Я...
вопрос задан: 10 August 2010 16:09
1
ответ
“Строго положительный” в Agda
Я пытаюсь закодировать некоторую денотационную семантику в Agda на основе программы, которую я записал в Haskell. значение данных = FunVal (Значение-> Значение) | Интервал PriVal | идентификатор ConVal [Значение]...
вопрос задан: 6 April 2010 07:44
0
ответов
Конгруэнтность для гетерогенного равенства
Я пытаюсь использовать гетерогенное равенство, чтобы доказать утверждения, включающие этот индексированный тип данных: data Counter: ℕ → Set where cut: (ij: ℕ) → Counter (Suc i + j) I was возможность писать свои доказательства, используя ...
вопрос задан: 28 September 2019 17:02
0
ответов
Различия между Agda и Idris
Я начинаю погружаться в программирование с зависимой типизацией и обнаружил, что языки Agda и Idris наиболее близки к Haskell, поэтому я начал с этого. Мой вопрос: в чем заключаются основные различия ...
вопрос задан: 2 August 2017 11:25
0
ответов
Общее программирование через эффекты
В библиотеке «Эффекты Идриса» эффекты представлены в виде ||| Этот тип параметризуется с помощью: ||| + Возвращаемый тип вычисления. ||| + Входной ресурс. ||| + Вычисления для запуска на ...
вопрос задан: 22 January 2016 05:06
0
ответов
Agda как язык программирования [закрыто]
Я нашел много полезной информации об использовании Agda в качестве системы доказательств. Я практически не нашел информации об использовании Agda для написания полезных программ. Я даже не могу найти пример "hello world", который...
вопрос задан: 10 May 2014 21:21
0
ответов
С чего начать с программирования зависимого типа? [закрыто]
Существует учебное пособие по Idris, учебное пособие по Agda и множество других статей по стилю учебного пособия и вводный материал с бесконечными ссылками на вещи, которые еще предстоит изучить. Я ползаю в середине ...
вопрос задан: 20 January 2013 14:53
0
ответов
Что такое комбинаторно-логический эквивалент интуиционистской теории типов?
Недавно я закончил университетский курс, посвященный Haskell и Agda (, функциональному языку программирования с зависимой типизацией ), и мне было интересно, можно ли заменить лямбда-исчисление в этих...
вопрос задан: 11 July 2012 08:41
0
ответов
Преобразование кода Haskell в код Agda
Мы должны преобразовать этот тип данных haskell в код Agda: data TRUE
данные ЛОЖЬ
данные BoolProp :: * -> * где
PTrue :: BoolProp TRUE
PFalse :: BoolProp FALSE
PAnd :: BoolProp a -> BoolProp b -&...
вопрос задан: 19 May 2012 13:33
0
ответов
Как избежать постулата экстенсиональности при определении неунарных функций над частными типами
Я пытаюсь определить функции с более чем одним аргументом над частными типами. Используя каррирование, я могу свести проблему к определению функций над точечным произведением setoid: module Foo where ...
вопрос задан: 13 May 2012 12:52
0
ответов
Установка Agda на Windows 7
У меня проблемы с запуском Agda на моем компьютере с Windows 7 64 -бит. Я попытался запустить следующие команды :cabal install agda и исполняемый файл cabal install agda -, которые обе работают, но я все еще не могу...
вопрос задан: 30 April 2012 05:10
0
ответов
Выяснение, какие метасы не решены в программе Agda.
Какой лучший способ узнать, что вызывает нерешенные метастазы? Есть ли способ превратить все нерешенные мета (и только нерешенные) в дыры, расширяя все окружающие подстановочные знаки, которые ...
вопрос задан: 27 April 2012 07:26
0
ответов
≡ -Рассуждение и & #39;с& #39; Patterns
Я доказывал некоторые свойства filter и map, все шло неплохо, пока я не наткнулся на это свойство :filter p (map f xs )≡ map f (filter (p ∘ f )xs ). Вот часть кода, которая...
вопрос задан: 25 April 2012 16:40
0
ответов
Прекращение структурной индукции
Я не могу заставить программу проверки завершения Agda принимать функции, определенные с помощью структурной индукции. Я создал следующий, как мне кажется, самый простой пример, демонстрирующий эту проблему.
Следующее ...
вопрос задан: 5 February 2012 04:30
0
ответов
Параметризованные индуктивные типы в Agda
Я только что читаю «Зависимые типы в действии». Во введении к параметризованным типам автор упоминает, что в этом объявлении список данных (A: Set): Set where []: List A _ :: _: A → List A → ...
вопрос задан: 22 January 2012 17:04
0
ответов
Определение конечных множеств в Agda
Я новичок в Agda. Я читаю статью «Зависимые типы в действии» Аны Бове и Питера Дайбьера. Я не понимаю обсуждения конечных множеств (на странице 15 в моем экземпляре). В статье дается определение Fin ...
вопрос задан: 26 August 2011 18:34
0
ответов
Небезопасное принуждение и более эффективный код Agda (-ftrust-me-im-agda)
В списке рассылки Agda Конор МакБрайд спросил: есть ли способ получить такие операции, как предполагаемое доверие? -> x, который на самом деле не проверяет Just and Goes ...
вопрос задан: 4 October 2010 04:14