Описание тега coinduction
3
ответа
Являются ли списки индуктивными или индуктивными в Хаскеле?
Так что в последнее время я читаю о коиндукции, и теперь мне интересно: списки на Haskell индуктивны или коиндуктивны? Я также слышал, что Хаскелл не различает их, но если да, то как они делают это формально? Списки определяются индуктивно, data [a]…
04 окт '16 в 14:09
1
ответ
Доказательство законов функторов потока
Я писал что-то похожее на поток. Я могу доказать каждый закон функтора, но не могу найти способ доказать, что он тотальный: module Stream import Classes.Verified %default total codata MyStream a = MkStream a (MyStream a) mapStream : (a -> b) ->…
26 май '15 в 02:49
1
ответ
Проверка завершения рекурсивного вызова функции в agda
Следующий код отлично подходит для Haskell: dh :: Int -> Int -> (Int, Int) dh d q = (2^d, q^d) a = dh 2 (fst b) b = dh 3 (fst a) Подобный код в Agda не будет компилироваться (проверка завершения не пройдена): infixl 9 _^_ _^_ : ℕ → ℕ → ℕ x ^ z…
06 июн '15 в 23:25
1
ответ
Трудно понять коиндукцию Агды
Я пытаюсь кодировать функциональную семантику для языка IMP с параллельным упреждающим планированием, как представлено в разделе 4 следующей статьи. Я использую Agda 2.5.2 и стандартную библиотеку 0.13. Кроме того, весь код доступен в следующем разд…
05 фев '17 в 13:50
1
ответ
Взаимная рекурсия в primcofix
Когда я пишу codatatype inftree = node nat inftree inftree primcorec one :: inftree and two :: inftree where "one = node 1 one two" | "two = node 2 one two" я получил "inftree" не является взаимо-действующим ядром с "inftree" и не является вложенным…
21 апр '17 в 17:18
2
ответа
Коиндукция и зависимые типы
Я пытаюсь написать функцию Coq, которая принимает Stream и предикат и возвращается, как list, самый длинный префикс потока, для которого выполняется свойство. Вот что у меня есть: Require Import List Streams. Require Import Lt. Import ListNotations.…
15 июл '13 в 15:23
1
ответ
Почему я не могу определить следующую CoFixpoint?
Я использую: $ coqtop -v The Coq Proof Assistant, version 8.4pl5 (February 2015) compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1 Я определил следующее CoInductive тип, stream: $ coqtop Welcome to Coq 8.4pl5 (February 2015) Coq < CoInductive st…
04 май '15 в 06:04
1
ответ
Coinduction на Coq, несоответствие типов
Я пробовал коиндуктивные типы и решил определить коиндуктивные версии натуральных чисел и векторов (списки с их размером в типе). Я определил их и бесконечное число так: CoInductive conat : Set := | cozero : conat | cosuc : conat -> conat. CoIndu…
13 окт '17 в 23:28
1
ответ
Доказательство принципа коиндукции для ко-натуральных чисел
Я должен признать, что я не очень хорош в коиндукции. Я пытаюсь показать принцип бисимуляции для ко-натуральных чисел, но я застрял на паре (симметричных) случаев. CoInductive conat := | cozero : conat | cosucc : conat -> conat. CoInductive conat…
10 июл '17 в 12:42
1
ответ
Как создать функцию enumFromTo на Morte?
Morte был разработан, чтобы служить промежуточным языком для супероптимизирующих функциональных программ. Чтобы сохранить строгую нормализацию, она не имеет прямой рекурсии, поэтому индуктивные типы, такие как списки, представлены в виде складок, а…
20 фев '15 в 23:56
1
ответ
Вычислить бесконечное дерево из корневых путей, используя модальность задержки
Это вариант " Вычислить (бесконечное) дерево из оператора с фиксированной точкой, используя модальность задержки ". Настройки. Мы изучаем язык бинарных деревьев, дополненный возможностью ссылаться на произвольные другие узлы в дереве путем от корня:…
16 июн '16 в 20:38
1
ответ
Является ли равенство разрешимым на любом типе коиндуктивности?
Это мой первый пост, извиняюсь, если я допустил ошибки. Я подозреваю, что в Coq коиндуктивные типы, такие как Stream, не имеют разрешимого равенства. То есть, учитывая два потока s и t, невозможно определить, является ли s=t или ~(s=t). Я подозреваю…
18 июн '15 в 08:10
2
ответа
Как доказать sset (цикл xs) = установить xs
При работе с типом данных бесконечного потока Изабель мне нужна эта, очевидно, истинная лемма, но я не могу понять, как это доказать (поскольку я еще не очень хорошо разбираюсь в коиндукции). Как мне доказать это? lemma sset_cycle[simp]: "xs ≠ [] ⟹ …
19 май '16 в 10:08
1
ответ
Как эффективно преобразовать индуктивный тип в коиндуктивный тип (без рекурсии)?
> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-} Любой индуктивный тип определяется так > newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r} > induction = flip flipinduct induction имеет тип (f a ->…
06 дек '15 в 22:20
1
ответ
Доказательство коиндуктивного свойства (лексическое упорядочение транзитивно) в Coq
Я пытаюсь доказать первый пример в "Практической коиндукции" в Coq. Первый пример - доказать, что лексикографическое упорядочение бесконечных потоков целых чисел транзитивно. Я не смог сформулировать доказательства, чтобы обойти условие Охраняемости…
19 мар '15 в 00:16
0
ответов
Нужны ли типы, которые не являются ни индуктивными, ни коиндуктивными для написания реальных программ?
Или просто иногда слишком сложно доказать, что тип является коиндуктивным? Я говорю о языке программирования, который является полным, что означает, что он не завершен по Тьюрингу, и рекурсия все хорошо обоснована, а corecursion - все продуктивно. П…
09 ноя '16 в 16:22
1
ответ
Ltac вызов "Cofix" не удалось. Ошибка: все методы должны конструировать элементы в коиндуктивных типах
Require Import Streams. CoFixpoint map {X Y : Type} (f : X -> Y) (s : Stream X) : Stream Y := Cons (f (hd s)) (map f (tl s)). CoFixpoint interleave {X : Type} (s : Stream X * Stream X) : Stream X := Cons (hd (fst s)) (Cons (hd (snd s)) (interleav…
18 июн '17 в 04:04
0
ответов
Агда: как сделать неразрывную IO (getLine) без (устаревшей?) Коиндукции в стиле ∞?
В этом вопросе о том, как это сделать getLine в Агде основной ответ предлагает использовать монаду частичности, чтобы справиться с возможным прекращением работы с результирующей Costring. С другой стороны, в версии 2.5.3 страница руководства по Coin…
24 окт '17 в 19:49
2
ответа
Доказательство равенства в коиндуктивных ленивых списках в Coq
Я экспериментирую с типами Coq Coinductive. Я использую ленивый тип списка из книги Coq'Art (раздел 13.1.4): Set Implicit Arguments. CoInductive LList (A:Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. Implicit Arguments LNil…
05 окт '16 в 19:53
3
ответа
Определение отношения равенства для бесконечных деревьев
В coq я могу определить отношения равенства для коиндуктивных типов, чьи компоненты являются парами: Section Pairs. Variable (A:Type). CoInductive Stream := cons : (A * Stream) -> Stream. CoInductive Stream_eq : Stream -> Stream -> Prop := …
26 окт '18 в 12:21