如何使具有前提的 Adga 函数工作

Question

我想让自然数的减法起作用。然而，函数的参数有一个前提，即 a 中的所有 a， b 在 N 中;a>= b. 所以我做了一些相关的函数：

data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
data _NotLessThan_ : (n m : ℕ) → Set where
ZERO : zero NotLessThan zero
SUC_ZERO : ∀ n → (suc n) NotLessThan zero
STEP : ∀ m n → m NotLessThan n → (suc m) NotLessThan (suc n)
sub : (m n : ℕ) →  (a : m NotLessThan n) → ℕ
sub zero (suc n) () -- zero - n can't return
sub zero zero _ = zero
sub (suc m) zero _ = (suc m)
sub (suc x) (suc y) a = sub x y (x NotLessThan y)

但是，我收到错误：

Set !=< x NotLessThan y of type Set₁
when checking that the expression x NotLessThan y has type
x NotLessThan y

我发现该类型x NotLessThan y，因为我除外。是否有任何类型错误？如何调试这种类型错误或如何声明一个函数来跳过类型检测错误？

Answer 1

表达式(x NotLessThan y)不是类型(x NotLessThan y)。NotLessThan是类型集(索引集)的数据定义。您可以使用已定义的三个构造函数构造NotLessThan的元素。在这种情况下，您必须在a上模式补丁，以获得适当的构造函数和所需类型的元素。所以最后一种情况是

sub (suc x) (suc y) (STEP _ _ a) = sub x y a

Answer 2

简而言之

代码片段中存在类型不兼容，即(x NotLessThan y)是一个类型，而不是类型(x NotLessThan y)的值，您必须提供该值才能使函数类型正确。以下代码片段更正了此问题：

sub : (m n : ℕ) →  (a : m NotLessThan n) → ℕ
sub .zero .zero ZERO = zero
sub .(suc n) .zero SUC n ZERO = suc n
sub .(suc m) .(suc n) (STEP m n a) = sub m n a

在长

这是代码中的主要问题，但也有一些不准确之处阻止了您编写正确的代码。具体如下：

• 您的数据类型名称_NotLessThan_可以有所改进，以更好地匹配数学概念(并匹配您将在标准库中找到的内容)。

• 构造函数通常不使用大写字母书写。

• 您提供了两个具有相同用途的构造函数ZERO和SUC_ZERO，也就是说，任何自然数都大于或等于零。这些可以分解。

• 第二个构造函数SUC_ZERO包含一个下划线，Agda 会将其解释为放置此构造函数的参数的位置。我觉得这不是故意的，在这种情况下，您绝对应该避免在构造函数名称中使用下划线。

• 在你的函数中，sub你对两个自然变量进行了大小写拆分，尽管第三个参数(a大于b的证明)已经包含了计算发生的必要信息。相反，此参数上的模式匹配也将避免任何空情况。

考虑这些注释会导致数据类型的以下定义：

data _≤_ : ℕ → ℕ → Set where
z≤s : ∀ {a} → zero ≤ a
s≤s : ∀ {a b} → a ≤ b → suc a ≤ suc b

从这种数据类型中，子函数然后非常自然地编写：

sub' : ∀ a b → b ≤ a → ℕ
sub' a .zero z≤s = a
sub' ._ ._ (s≤s p) = sub' _ _ p

请注意，在此代码段中，下划线(以及定义左侧的点)用于标记其值可由 Agda 推断的参数，这使得证明足以计算减法的事实可见。

为了走得更远

让 Agda 单独计算证明而不是在您想要进行减法时提供证明可能会很有趣。为了做到这一点，你的数据类型必须被证明是可判定的，这意味着，给定两个自然数a和b，必须编写一个函数来计算a ≤ b证明或否定它。这需要几个步骤，第一个是逻辑 false(空类型)的定义：

data ⊥ : Set where

根据此数据类型，可以定义逻辑否定：

¬ : Set → Set
¬ A = A → ⊥

我们现在可以定义可判定类型的类型(粗略地说，它可以被证明为真或假)：

data Dec (A : Set) : Set where
yes : A → Dec A
no : ¬ A → Dec A

然后，我们可以证明对于任何输入，关于此定义，较小或相等的数据类型是可判定的：

_≤?_ : ∀ a b → Dec (a ≤ b)
zero ≤? b = yes z≤s
suc a ≤? zero = no (λ ())
suc a ≤? suc b with a ≤? b
suc a ≤? suc b | yes p = yes (s≤s p)
suc a ≤? suc b | no ¬p = no λ {(s≤s q) → ¬p q}

为了封装减法的错误情况，我们需要 may monad，它要么是 and 错误情况，要么是一个值：

data Maybe (A : Set) : Set where
nothing : Maybe A
just : A → Maybe A

最后，我们可以写一个减法，取两个自然数，检查是否满足减法的要求，如果满足，则返回错误，并在可能的情况下计算：

_-M_ : (a b : ℕ) → Maybe ℕ
a -M b with b ≤? a
a -M b | yes p = just (sub' a b p)
a -M b | no _ = nothing

作为失败的一个例子，这里有一个不合理的减法：

error : Maybe ℕ
error = suc (suc (zero)) -M (suc (suc (suc (suc (suc (suc zero))))))

以下是阿格达在评估error时给出的内容：

nothing

作为成功的一个例子，这里有一个合理的减法：

success : Maybe ℕ
success = (suc (suc (suc (suc (suc (suc zero)))))) -M suc (suc (zero))

以下是阿格达在评估success时给出的内容：

just (suc (suc (suc (suc zero))))

请注意，所有这些量(直到 may 数据类型的定义)都可以在标准库中找到，并且在呈现它们时我故意省略了宇宙级别。