使用函数编码属性有什么缺点？

Question

在Agda中,通常有两种方法来改进集合.一种是简单地编写一个函数来检查属性是否成立,并提升.例如:

has_true : List Bool -> Bool 
has_true (true ? xs) = true
has_true (false ? xs) = has_true xs
has_true [] = false

Truthy : List Bool -> Set
Truthy list = T (has_true list)

这里Truthy list证明了布尔列表至少有一个真元素.另一种方法是直接编码该属性,作为归纳类型:

data Truthy : List Bool -> Set where
  Here  : (x : Bool) -> (x ? true) -> (xs : List Bool) -> Truthy (x ? xs)
  There : (x : Bool) -> (xs : List Bool) -> Truthy xs -> Truthy (x ? xs)

在这里,Truthy list也证明了同样的事情.

我相信我之前已经阅读过比较,但我不记得了.那些不同的款式有名字吗？使用一种风格而不是另一种风格有什么优点和缺点？还有第三种选择吗？

Answer 1

到目前为止,您列出了两种定义谓词的方法:

1. A -> Bool 功能.
2. 归纳谓词.

我还要补充一点:

3. A -> Set功能.也可称为"递归定义"或"由大消除定义".

第三个版本在Agda中如下:

open import Data.Bool
open import Data.Unit
open import Data.Empty
open import Data.List

hastrue : List Bool ? Set
hastrue []           = ?   -- empty type
hastrue (false ? bs) = hastrue bs
hastrue (true ? bs)  = ?   -- unit type

首先,让我们谈谈使用这三个选项可以表示什么类型的谓词.这是一个ASCII表.*是一个通配符代表是/否.

                    | P : A -> Set | P : A -> Bool | data P : A -> Set |
|-------------------|--------------|---------------|-------------------|
| Proof irrelevant  | *            | yes           | *                 |
| Structural        | yes          | yes           | *                 |
| Strictly positive | *            | N/A           | yes               |
| Decidable         | *            | yes           | *                 |

证明不相关意味着所有证据P x都是平等的.在Bool情况下,证明通常是一些p : P x ? true,或p : IsTrue (P x)用IsTrue = ? b ? if b then ? else ?,并在这两种情况下,所有的证据都是平等的确实.我们可能会也可能不希望谓词无关紧要.

结构意味着P x只能使用A结构上小于的元素来定义x.函数总是结构化的,所以如果某些谓词不是,那么它只能被归纳定义.

严格肯定意味着P不能递归地出现在函数箭头的左侧.非严格正面谓词不是可归定的.证明相关的非严格正谓词的一个例子是函数类型代码的解释:

data Ty : Set where
  top : Ty
  fun : Ty ? Ty ? Ty

?_? : Ty ? Set
? top     ? = ?
? fun A B ? = ? A ? ? ? B ?  -- you can't put this in "data"

可判定性是不言自明的; A -> Bool函数必然是可判定的,这使得它们不适用于不可判断或不能轻易地作为结构Bool函数写出的谓词.可判定性的优点是被排除在中间推理之外,Bool如果没有假设或额外的可判定性证明,则无法使用非谓词定义.

第二,关于Agda/Idris的实际影响.

• 您可以对归纳谓词的证明进行依赖模式匹配.使用递归和布尔谓词,您必须A首先对值进行模式匹配,以使谓词见证计算.有时这会使归纳谓词变得方便,例如,您可以使用包含10个构造函数的枚举类型,并且您希望谓词仅保留在一个构造函数中.归纳定义的谓词只允许您匹配真实案例,而其他版本则要求您始终匹配所有案例.

• 另一方面,只要知道A元素具有给定形状,布尔和递归谓词就会自动计算.这可以在Agda中使用,以便在没有策略或实例的情况下自动填写样张.例如,具有类型的孔或隐式参数hastrue xs可以通过对的eta规则和单元类型来解决,只要xs是具有已知包含true前缀的列表表达式.这类似于布尔谓词.