在Agda中,a的类型forall以这样的方式确定:以下都具有类型Set1(where Set1的类型Set和A类型Set):

Set ? A
A ? Set
Set ? Set

但是,以下类型Set:

A ? A

我明白,如果Set有类型Set,就会有矛盾,但我没有看到,如果上述三个术语中的任何一个有类型Set,我们就会有矛盾.那些可以用来证明是假的吗？它们可以用来表明Set : Set吗？

我有以下两个定义，导致两个不同的错误消息。第一个定义由于严格的正性而被拒绝，第二个定义由于宇宙不一致而被拒绝。

(* non-strictly positive *)
Inductive SwitchNSP (A : Type) : Type :=
| switchNSP : SwitchNSP bool -> SwitchNSP A.

Fail Inductive UseSwitchNSP :=
| useSwitchNSP : SwitchNSP UseSwitchNSP -> UseSwitchNSP.

(* universe inconsistency *)
Inductive SwitchNSPI : Type -> Type :=
| switchNSPI : forall A, SwitchNSPI bool -> SwitchNSPI A.

Fail Inductive UseSwitchNSPI :=
| useSwitchNSPI : SwitchNSPI UseSwitchNSPI -> UseSwitchNSPI.

在gitter上聊天显示，首先检查了Universe（内部）一致性，即第一个定义遵循此检查，但是由于严格的正性问题而失败。

据我了解严格的积极性限制，如果Coq允许非严格的积极性数据类型定义，我可以不使用而构造非终止函数fix（这很糟糕）。

为了使之更加混乱，第一个定义在Agda中被接受，第二个定义给出了严格的正错误。

data Bool : Set where
  True : Bool
  False : Bool …

有谁知道以下任何例子？

1. 关于证明助理(例如Coq)中正则表达式(可能通过反向引用扩展)的证据开发.
2. 关于正则表达式的依赖类型语言(例如Agda)中的程序.

找出造成未解决问题的原因的最佳方法是什么？有没有办法通过扩展所有可解决的周围通配符将所有未解决的元素(以及只有未解决的元素)转换为空洞？

如果没有别的,将未解决的元素更改为一个洞会使关于未解决元的消息消失吗？因为那时我想我可以尝试将每个通配符和每个隐式参数更改为孔,直到消息消失然后找出导致问题的那个...

在Idris 效果库中,效果表示为

||| This type is parameterised by:
||| + The return type of the computation.
||| + The input resource.
||| + The computation to run on the resource given the return value.
Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type

如果我们允许资源成为值并交换前两个参数,我们得到(其余代码在Agda中)

Effect : Set -> Set
Effect R = R -> (A : Set) -> (A -> R) -> Set

拥有一些基本的类型 - 上下文 - 会员机制

data Type : Set …

我是Agda的新手.我正在阅读Ana Bove和Peter Dybjer的论文"工作中的依赖类型".我不理解有限集的讨论(在我的副本中的第15页).

本文定义了一种Fin类型:

data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (succ n)
    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

我一定错过了一些明显的东西.我不明白这个定义是如何工作的.有人可以简单地将定义翻译Fin成日常英语吗？这可能是我需要理解本文的这一部分.

感谢您抽出宝贵时间阅读我的问题.我很感激.

我发现了很多关于使用Agda作为证明系统的有用信息.我发现几乎没有关于使用Agda编写可用程序的信息.我甚至找不到一个用最新版本的Agda编译的"hello world"示例.

所以,

1. 有没有关于Agda作为编程语言的好教程？

2. 是否有其他类似性质的语言(懒惰功能依赖类型)具有更成熟的文档,可以将它们用作编程语言？(我在Coq上找到了很多很棒的文档,但是,再一次,没有"Hello World").

由于_+_-Operation for Nat通常在第一个参数中以递归方式定义,因此对于类型检查器来说,知道这一点显然是非常重要的i + 0 == i.但是,当我在固定大小的向量上编写函数时,我经常遇到这个问题.

一个例子:我如何定义Agda函数

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)

它将第一个n值放在向量的末尾？

因为Haskell中的简单解决方案是

swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])

我在Agda中类似地尝试过这样的:

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {_} {zero} xs          = xs 
swap …

我看到了几个不同的研究小组,至少有一本关于使用Coq设计认证程序的书.关于认证计划的定义是什么,是否有共识？从我所知道的,它真正意味着该程序被证明是完整的并且类型正确.现在,程序的类型可能是非常奇特的东西,例如列表,其中包含非空的证明,排序,所有元素> = 5等等.但是,最终,是一个经过认证的程序,Coq显示的是总计和类型安全的程序,所有有趣的问题归结为最终类型中包含的内容？

编辑1

根据wjedynak的回答,我看了Xavier Leroy的论文"现实编译器的形式验证",它在下面的答案中有所联系.我认为这包含一些很好的信息,但我认为这个研究序列中的信息量更多的信息可以在Sandrine Blazy和Xavier Leroy 的C语言的Clight子集的机械化语义学中找到.这是"形式验证"论文添加优化的语言.在其中,Blazy和Leroy介绍了Clight语言的语法和语义,然后在第5节讨论了这些语义的验证.在第5节中,列出了用于验证编译器的不同策略,这在某种意义上提供了概述创建认证计划的不同策略.这些是:

1. 手动评论
2. 证明语义的属性
3. 验证翻译
4. 测试可执行语义
5. 与备用语义的等价性

在任何情况下,可能会添加一些点,我当然希望听到更多.

回到我关于认证程序定义的原始问题,对我来说仍然有点不清楚.Wjedynak提供了一个答案,但Leroy的工作实际上涉及在Coq中创建编译器,然后在某种意义上证明它.从理论上讲,它现在可以证明C程序的内容,因为我们现在可以进行C-> Coq->证明.从这个意义上讲,似乎就是我们可以做到这一点

1. 用X语言编写程序
2. Coq中的步骤1或其他证明助手工具的程序模型的形式.这可能涉及在Coq中创建编程语言的模型,或者它可能涉及直接创建程序模型(即在Coq中重写程序本身).
3. 证明一些关于模型的属性.也许这是关于价值观的证明.也许它是语句等价性的证明(例如3 = 1 + 2或f(x,y)= f(y,x)之类的东西.)
4. 然后,根据这些证明,调用原始程序认证.

或者,我们可以在校对助手工具中创建程序规范,然后证明规范的属性,而不是程序本身.

无论如何,如果有人有这些定义,我仍然有兴趣听取其他定义.

设置

考虑一种在一类函数符号node 和一类变量上参数化的术语var:

data Term node var
  = VarTerm !var
  | FunTerm !node !(Vector (Term node var))
  deriving (Eq, Ord, Show)

instance Functor (Term node) where
  fmap f (VarTerm var)  = VarTerm (f var)
  fmap f (FunTerm n cs) = FunTerm n (Vector.map (fmap f) cs)

instance Monad (Term node) where
  pure = VarTerm
  join (VarTerm term) = term
  join (FunTerm n cs) = FunTerm n (Vector.map join cs)

这是一个有用的类型,因为我们用开放的术语编码,用Term node Var,关闭术语Term node Void …