Agn*_*yay 2 type-theory theorem-proving agda
显然,Agda中有一些功能称为积极性检查,即使type-in-type启用也可以显然保持系统声音.
我很想知道这是什么,但是Agda手册没有回答这个问题,只解释了如何关闭它.
在午餐桌上,我无意中听到这是关于类型理论的极性,但这就是我所知道的.我没有在网上找到任何解释这个概念的东西以及为什么它有助于保持稳健性.任何可理解的解释将不胜感激.
首先,我必须澄清一个误解:当启用type-in-type时,积极性检查不能保证健全.因此,数据类型必须同时满足积极性检查和宇宙检查以保持稳健性.
现在,为了解释积极性检查,让我们首先看一下我们不进行积极性检查的反例:
-- the empty type
data ? : Set where
-- a non-positive type
data Bad : Set where
bad : (Bad ? ?) ? Bad
假设允许这种数据类型,那么你可以很容易地证明?:
bad-is-false : Bad ? ?
bad-is-false (bad f) = f (bad f)
bad-is-true : Bad
bad-is-true = bad bad-is-false
boom : ?
boom = bad-is-false bad-is-true
根据Curry-Howard的对应,Bad的定义说:Bad是真的,当且仅当Bad是假的.因此,它导致不一致并不奇怪.
积极性检查排除数据类型,例如Bad.通常,(严格)积极性标准表示c数据类型的每个构造函数都D应该具有表单的类型
c : (x1 : A1)(x2 : A2) ... (xn : An) ? D xs
其中每个参数的类型艾要么非递归(即,它不参照D)或形式的(y1 : B1)(y2 : B2) ... (ym : Bm) ? D ys,其中每个Bj不参考D.
Bad不满足此标准,因为构造函数的参数bad具有类型Bad ? ?,它既不是两个允许的形式.
这个名字的积极性检查"来(如类型理论很多事情要做)从范畴论,积极endofunctor的具体概念.满足积极性标准的数据类型的每个定义都是类型类别上的正向endofunctor.这意味着我们可以构造该endofunctor 的初始代数,它可以在构造类型理论模型(用于证明稳健性)时用于建模数据类型.