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

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

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

A -> Bool 函数。
归纳谓词。

我再补充一个：

A -> Set 函数。也可以称为 "recursively defined" 或 "defined by large elimination".

第三个版本在 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

首先，让我们用三个选项来谈谈表示什么样的谓词table。这是一个 ASCII table。 * 是代表 yes/no 的通配符。

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

Proof irrelevance 表示 P x 的所有证明都是相等的。在 Bool 的情况下，证明通常是一些 p : P x ≡ true，或 p : IsTrue (P x) 和 IsTrue = λ b → if b then ⊤ else ⊥，并且在这两种情况下所有证明确实是相等的。我们可能希望也可能不希望谓词无关紧要。

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

严格正数表示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"

Decidable 是不言自明的； A -> Bool 函数必然是可判定的，这使得它们不适用于 table 不可判定或不能轻易写成结构 Bool 函数的谓词。可判定性的优点是排除了中间推理，这对于没有假设或额外的可判定性证明的非Bool谓词定义是不可能的。

其次，关于 Agda/Idris 中的实际后果。

您可以对归纳谓词的证明进行依赖模式匹配。对于递归和布尔谓词，您必须首先对 A 值进行模式匹配，以使谓词见证计算。有时这使得归纳谓词很方便，例如您可能有一个具有 10 个构造函数的枚举类型，并且您希望一个谓词只包含一个构造函数。归纳定义的谓词让您只匹配真实情况，而其他版本要求您始终匹配所有情况。
另一方面，只要您知道 A 元素具有给定的形状，布尔和递归谓词就会自动计算。这可以在 Agda 中使用，使类型推断自动填充证明，无需策略或实例。例如，只要 xs 是一个包含已知 true 前缀的列表表达式，类型为 hastrue xs 的空洞或隐式参数就可以通过对和单元类型的 eta 规则来解决。这与布尔谓词类似。

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

What are the drawbacks of encoding properties using functions?

agda