coinduction

1La chaleur

1Répondre

Définir une 'tête' pour un flux de type coinductif dans Coq (sans appariement de formes)

1) Je crois qu'il est possible d'utiliser des types inductifs sans appariement de formes. (en utilisant _rec, _rect, _ind seulement). C'est opaque, compliqué, mais possible. 2) Est-il possible d'utili

0La chaleur

1Répondre

appel

corecursive inattendue Ce (coupé out) de définition de la fonction corecursive Isabelle primcorec tree :: "'form fset ⇒ 'vertex ⇒ 'preform ⇒ (('form fset × 'form), ('rule × 'preform) NatRule) dtree" w

2La chaleur

1Répondre

principes CoInductive correspondant à la famille * de _rect des fonctions

Définition d'un nouveau type foo me donne un principe de récursion foo_rect, qui résumés avec élégance sur fix. Pourrait-on définir un équivalent coinducteur (abstraction supérieure à cofix) en "retou

2La chaleur

1Répondre

L'appel Ltac à "cofix" a échoué. Erreur: Toutes les méthodes doivent construire des éléments dans les types CoInductive

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) : Stre

6La chaleur

1Répondre

Problème de compréhension de la Coinduction d'Agda

J'essaie de coder une sémantique fonctionnelle pour le langage IMP avec une planification préemptive parallèle comme présenté dans la section 4 du paper suivant. J'utilise Agda 2.5.2 et la bibliothèqu

2La chaleur

1Répondre

Coinduction sur Coq, type mismatch

J'ai essayé des types coinductifs et j'ai décidé de définir des versions coinductives des nombres naturels et des vecteurs (listes avec leur taille dans le type). Je les ai définis et le nombre infini

1La chaleur

1Répondre

Prouver un principe de coinduction pour les nombres co-naturels

Je dois admettre que je ne suis pas très bon en coinduction. J'essaie de montrer un principe de bisimulation sur les nombres co-naturels, mais je suis coincé sur une paire de cas (symétriques). CoIndu

3La chaleur

1Répondre

Prouver une propriété co-inductive (l'ordre lexical est transitif) dans Coq

J'essaye de prouver le premier exemple dans "Practical Coinduction" dans Coq. Le premier exemple est de prouver que l'ordre lexicographique sur les flux infinis d'entiers est transitif. Je n'ai pas ét

2La chaleur

1Répondre

Calcul de l'arborescence infinie à partir de chemins enracinés à l'aide de la modalité de délai

Ceci est une variante de "Compute an (infinite) tree from fixpoint operator using delay modality". Le paramètre. Nous étudions un langage d'arbres binaires, augmentée avec la possibilité de se référer

2La chaleur

1Répondre

Laissez-lier les résultats intermédiaires dans monade IO

Dans ce contexte: open import IO open import Data.String open import Data.Unit open import Coinduction postulate A : Set f : String → A g₁ g₂ : A → String disons que je veux mett