Описание тега totality
1
ответ
Какие размеры в Агде?
Какие размеры в Агде? Я пытался прочитать статью о MiniAgda, но не смог продолжить из-за следующих моментов: Почему типы данных являются общими для их размера? Насколько я знаю, размер - это глубина дерева индукции. Почему типы данных ковариантны от…
02 ноя '16 в 15:27
0
ответов
Проверка целостности с косвенными взаимно рекурсивными типами данных в Idris
Я работаю с абстрактным синтаксическим деревом, где я хотел бы дать связующим их собственный тип. Это, кажется, вызывает проблемы для проверки целостности Идриса... С типичной референцией Tree Идрис прекрасно справляется с проверкой целостности. dat…
09 дек '18 в 18:15
1
ответ
Coq не может вычислить обоснованную функцию на Z, но она работает на nat
Я пишу (для себя) объяснение того, как сделать обоснованную рекурсию в Coq. (см., например, книгу Coq'Art, глава 15.2). Сначала я сделал пример функции на основе nat и это работало нормально, но потом я сделал это снова для Zи когда я использую Comp…
25 май '17 в 17:47
0
ответов
Странное поведение сопоставления с образцом в Идрисе
Я наткнулся на то, что кажется странным для Идриса. Я использую Emacs 25.3 на Ubuntu 17.04 и Idris 1.0. Рассмотрим следующий модуль: module Strange %default total fun : Int -> Int -> Int fun 0 0 = 0 fun 0 n = 10 fun n 0 = 20 Когда я загружаю э…
16 дек '17 в 14:57
1
ответ
Ошибка: невозможно угадать уменьшение аргумента исправления. Coq
I have the following definition for terms : Require Import Coq.Arith.Arith. Require Import Coq.Lists.List. Require Import Coq.Strings.String. Import ListNotations. Definition VarIndex:Type := nat. Inductive Term : Type := |Var : VarIndex -> Term …
21 май '17 в 13:24
1
ответ
Coq не может вычислить обоснованные, определенные с помощью Fix, но может, если определено с помощью программы Fixpoint
В качестве упражнения для понимания рекурсии по обоснованному отношению я решил реализовать расширенный евклидов алгоритм. Расширенный евклидов алгоритм работает с целыми числами, поэтому мне нужны некоторые обоснованные отношения с целыми числами. …
15 апр '18 в 20:47
1
ответ
В чем разница между точкой фиксации программы и функцией в Coq?
Кажется, они служат схожим целям. Единственное различие, которое я заметил, заключается в том, что пока Program Fixpoint примет сложную меру, как {measure (length l1 + length l2) }, Function кажется, отвергнуть это и позволит только {measure length …
17 июн '17 в 15:24
3
ответа
Ошибка в определении Аккермана в Coq
Я пытаюсь определить функцию Ackermann-Peters в Coq, и я получаю сообщение об ошибке, которое я не понимаю. Как видите, я собираю аргументы a, b Аккермана в паре ab; Я предоставляю порядок, определяющий функцию порядка для аргументов. Тогда я исполь…
24 апр '12 в 05:53
2
ответа
Лучшая практика Coq: взаимная рекурсия, структурно уменьшается только одна функция
Рассмотрим следующее игрушечное представление для нетипизированного лямбда-исчисления: Require Import String. Open Scope string_scope. Inductive term : Set := | Var : string -> term | Abs : string -> term -> term | App : term -> term -&g…
28 июн '17 в 02:42
0
ответов
Использование комбинаторов парсера Text.Parser и Inf
Далее используется грамматика из файла contrib.Parser test : Grammar t b a -> Grammar t b a test p = do a <- p pure a К сожалению, это приводит к ошибке компилятора: type mismatch between _ -> Grammar tok False _ and delayed Infinite b (a -…
03 янв '18 в 09:55
2
ответа
Является ли эта рекурсивная функция неполной или компилятор просто не может это доказать? Как переписать это как общее?
Когда представлен следующий код: module TotalityOrWhat %default total data Instruction = Jump Nat | Return Char | Error parse : List Char -> Instruction parse ('j' :: '1' :: _) = Jump 1 parse ('j' :: '2' :: _) = Jump 2 parse ('j' :: '3' :: _) = J…
20 авг '16 в 16:00
1
ответ
Почему эта функция вешает REPL?
В главе 9 " Разработка через тестирование с помощью Idris" представлен следующий тип данных и removeElem функция. import Data.Vect data MyElem : a -> Vect k a -> Type where MyHere : MyElem x (x :: xs) MyThere : (later : MyElem x xs) -> MyEl…
21 июн '17 в 00:26
1
ответ
Взаимная рекурсивная функция и проверка завершения в Coq
РЕДАКТИРОВАТЬ Require Import Bool List ZArith. Variable A: Type. Inductive error := | Todo. Inductive result (A : Type) : Type := Ok : A -> result A | Ko : error -> result A. Variable bool_of_result : result A -> bool. Variable rules : Type…
08 ноя '12 в 09:31
1
ответ
Идрис: проверка целостности завершается неудачно при попытке повторно реализовать из Integer для Nat
У меня есть следующий код: module Test data Nat' = S' Nat' | Z' Num Nat' where x * y = ?hole x + y = ?hole fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1)) Я получаю сообщение об ошибке о последней строке: Test.idr:6:5: Prelude.Inte…
12 май '17 в 08:53
2
ответа
Не могу определить завершение
Функция для определения, является ли набор подмножеством другого: Fixpoint subset (s1:bag) (s2:bag) : bool := match s1 with | nil => true | h :: t => match (beq_nat (count h s1) (count h s2)) with | true => subset (remove_all h t) (remove_a…
16 янв '18 в 20:12
2
ответа
Научите coq проверять завершение
Coq, в отличие от многих других, принимает необязательный явный параметр, который может использоваться для указания убывающей структуры определения точки фиксации. Из спецификации Галлина, 1.3.4, Fixpoint ident params {struct ident0 } : type0 := ter…
09 янв '18 в 17:40
1
ответ
Ограничения Fixpoint в Coq?
Я дурачусь с Coq. В частности, я пытаюсь реализовать сортировку слиянием, а затем доказать, что она работает. Моя попытка реализации была: Fixpoint sort ls := match ls with | nil => nil | cons x nil => cons x nil | xs => let (left, right) :…
10 дек '12 в 04:15
0
ответов
Делаете strIndex в быстром поиске?
Я работаю над версией алгоритма быстрого поиска строки в Idris и придумала это: quickSearch : (needle : String) -> (haystack : String) -> {auto lengths : (length needle) `LTE` (length haystack)} -> Maybe Nat quickSearch needle haystack = le…
08 авг '17 в 22:54
1
ответ
Coq simple для программы Fixpoint
Есть ли что-то вроде тактики simpl за Program Fixpoints? В частности, как можно доказать следующее тривиальное утверждение? Program Fixpoint bla (n:nat) {measure n} := match n with | 0 => 0 | S n' => S (bla n') end. Lemma obvious: forall n, bl…
31 мар '16 в 09:22
1
ответ
Нахождение обоснованного отношения, чтобы доказать завершение функции, которая в какой-то момент перестает убывать
Предположим, у нас есть: Require Import ZArith Program. Program Fixpoint range (from to : Z) {measure f R} : list := if from <? to then from :: range (from + 1) to else []. Я хотел бы убедить Coq, что это заканчивается - я попытался измерить разм…
05 янв '18 в 21:17