标签: coinduction

所以我最近一直在阅读有关coinduction的内容,现在我想知道:Haskell列出了归纳还是共同？我也听说Haskell没有区分这两者,但如果是这样的话,他们怎么这样做呢？

列表是归纳定义的data [a] = [] | a : [a],但可以共同使用,ones = a:ones.我们可以创建无限列表.然而,我们可以创建有限列表.他们是哪一个？

相关的是Idris,其中类型List a严格地是归纳类型,因此仅是有限列表.它的定义类似于Haskell中的方式.然而,Stream a是一种共同类型,建模无限列表.它被定义为(或者更确切地说,定义相当于)codata Stream a = a :: (Stream a).创建无限List或有限Stream是不可能的.但是,当我写出定义时

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

我得到了我对Haskell列表的期望,即我可以创建有限和无限结构.

所以让我把它们归结为几个核心问题:

1. Haskell不区分归纳和共感类型吗？如果是这样,那是什么形式化？如果没有,那么哪个是[a]？

2. HList是coinductive吗？如果是这样,coinductive类型如何包含有限值？

3. 如果我们定义data HList' a = L (List a) | R (Stream a)怎么办？会考虑什么和/或仅对它有用HList？

> {-# LANGUAGE DeriveFunctor, Rank2Types, ExistentialQuantification #-}

任何归纳类型都是这样定义的

> newtype Ind f = Ind {flipinduct :: forall r. (f r -> r) -> r}
> induction = flip flipinduct

induction有类型(f a -> a) -> Ind f -> a.这种称为共同诱导的概念是双重的.

> data CoInd f = forall r. Coinduction (r -> f r) r
> coinduction = Coinduction

coinduction有类型(a -> f a) -> a -> CoInd f.注意如何induction和coinduction是双重的.作为归纳和coinductive数据类型的示例,请查看此仿函数.

> data StringF rec = Nil …

（免责声明：我不是 100% 确定 codatatype 是如何工作的，特别是在不涉及终端代数时）。

考虑“类型类别”，类似于Hask，但进行了适合讨论的任何调整。在这样的类别中，据说（1）初始代数定义数据类型，（2）终端代数定义协数据类型。

我正在努力说服自己相信（2）。

考虑函子T(t) = 1 + a * t。我同意初始T代数是明确定义的并且确实定义了[a]， 的列表a。根据定义，初始的T-algebra 是一个类型X和一个函数f :: 1+a*X -> X，这样对于任何其他类型Y和函数g :: 1+a*Y -> Y，都存在一个m :: X -> Y这样的函数m . f = g . T(m)（其中.表示 Haskell 中的函数组合运算符）。通过f解释为列表构造函数、g初始值和阶跃函数以及T(m)递归操作，该方程本质上断言了m给定任何初始值和 中定义的任何阶跃函数的函数的唯一存在性g，这需要一个底层的良好-fold与基础类型（. 列表）一起表现a。

例如，g …

我了解如何在 Haskell 中定义同构流和异构流。

-- Type-invariant streams.
data InvStream a where
   (:::) :: a -> InvStream a -> InvStream a

-- Heterogeneous Streams.
data HStream :: InvStream * -> * where
   HCons :: x -> HStream xs -> HStream (x '::: xs)

我们如何将恒定流定义为异构流的特殊情况？如果我尝试定义常量类型流的类型族，则会收到“归约堆栈溢出”错误。我想这与类型检查算法不够懒惰并试图计算整个Constant a类型流有关。

type family Constant (a :: *) :: InvStream * where
  Constant a = a '::: Constant a

constantStream :: a -> HStream (Constant a)
constantStream x =  HCons x (constantStream x)

有什么方法可以解决这个问题并定义恒定的异构流吗？我应该尝试其他类似的结构吗？

在Prolog中,统一X = [1|X]是一种获得无限列表的理智方式吗？SWI-Prolog没有任何问题,但GNU Prolog只是挂起.

我知道在大多数情况下我可以替换列表

one(1).
one(X) :- one(X).

但我的问题是明确是否可以X = [1|X], member(Y, X), Y = 1在"理智"的Prolog实现中使用该表达式.

我正在尝试使用并行抢占式调度来编写IMP语言的功能语义,如下文第4部分所述.

我正在使用Agda 2.5.2和标准库0.13.此外,整个代码可以通过以下要点获得.

首先,我将所讨论语言的语法定义为归纳类型.

  data Exp (n : ?) : Set where
    $_  : ? ? Exp n
    Var : Fin n ? Exp n
    _?_ : Exp n ? Exp n ? Exp n

  data Stmt (n : ?) : Set where
    skip : Stmt n
    _?_ : Fin n ? Exp n ? Stmt n
    _?_ : Stmt n ? Stmt n ? Stmt n
    iif_then_else_ : Exp n ? Stmt n ? Stmt …

我一直在写类似Stream的东西.我能够证明每个算子法,但我无法找到证明它总数的方法:

module Stream

import Classes.Verified

%default total

codata MyStream a = MkStream a (MyStream a)

mapStream : (a -> b) -> MyStream a -> MyStream b
mapStream f (MkStream a s) = MkStream (f a) (mapStream f s)

streamFunctorComposition : (s : MyStream a) -> (f : a -> b) -> (g : b -> c) -> mapStream (\x => g (f x)) s = mapStream g (mapStream f s)
streamFunctorComposition (MkStream x y) f g =
  let inductiveHypothesis = …

这是我的第一篇文章,如果我犯了错误就道歉.

我怀疑,在Coq中,像Stream这样的共同类型没有可判定的平等.也就是说,给定两个流s和t,不可能识别s = t或〜(s = t).我怀疑Coq中的所有共同类型都是如此.

快速谷歌和搜索堆栈交换不会透露任何确认.谁能证实这一点或纠正我？

我正在尝试CoNat从Jesper Cockx 和 Andreas Abel 的这篇论文中得到的定义：

open import Data.Bool
open import Relation.Binary.PropositionalEquality

record CoNat : Set where
  coinductive
  field iszero : Bool
        pred : .(iszero ? false) -> CoNat

open CoNat public

我定义zero和plus：

zero : CoNat
iszero zero = true
pred zero ()

plus : CoNat -> CoNat -> CoNat
iszero (plus m n)                                  = iszero m ? iszero n
pred (plus m n) _ with iszero m | inspect iszero m …

我正在通过https://agda.readthedocs.io/en/v2.6.0.1/language/coinduction.html研究共导和共模式。我以为我理解文章代码，所以我决定研究以下命题。

cons-uncons-id : ? {A} (xs : Stream A) ? cons (uncons xs) ? xs

我以为这个命题和文章问题非常相似，也可以证明，但我不能很好地证明。 这是我写的代码。

我认为它可以改进，cons-uncons-id (tl xs)因为它的类型与 merge-split-id 非常相似，但 Agda 不接受它。

这是我自己想到的一个问题，所以我认为这是真的，但当然存在误解的可能性。然而，非利弊和利弊会恢复原状是很自然的。

如果你应该能够证明它而不会被误解，请告诉我你如何证明它。

你能解释一下为什么不能像merge-split-id一样证明吗？

问候，谢谢！