programming-languages - 了解 Agda 模拟考试

Question

我正在使用 agda 进行编程语言基础练习考试，其中有以下问题:

您将获得以下 Agda 声明:

data Even : N → Set where
 ezero : Even 0
 esuc : { n : N }  → Even n  → Even (2+ n)

假设已经导入自然数标准库。回答以下问题:

a)ezero 的类型是什么？

b)是否有偶数1类型的项？

c) 有多少项属于 Even 2 类型？列出它们

d)描述如果我们将 esuc 的返回类型更改为 Even (n+2) 而不是 Even (2+n) 时可能出现的一个潜在问题.

我们没有提供解决方案手册。这个问题似乎很基本，但我不确定其中任何一个。我认为前三个问题的答案是:

a) 设置

b) 没有 Even 1 类型的项

c) Even 2 类型的一项

d) 不知道

如果能回答这些问题并附上简短的解释，我们将不胜感激。谢谢

Answer 1

What is the type of ezero?

数据构造函数 ezero 的类型可以从数据声明中读取:ezero : Even 0 表明它的类型为 Even 0 .

Are there any terms of type Even 1?

不，没有。这可以通过大小写区别来看出:如果有一个术语，那么它将以两个构造函数之一开头。由于它们具有特定的返回索引，因此它们必须与 1 统一。

• ezero 将强制执行 1 = 0
• esuc 表示存在一个 n 使得 1 = 2+ n

这两种情况都是不可能的。

How many terms are of type Even 2? List them

只有一个:esuc ezero。通过与上一问题类似的推理，我们可以证明 ezero 和 esuc (esuc p) (对于某些 p)获胜不这样做。

Describe one potential problem that might occur if we change the return type of esuc to be Even (n+2) instead of Even (2+n).

考虑证明plus-Even : {m n : N} → Even m → Even n → Even (m + n)。由于 (+) 是通过第一个参数的归纳来定义的，因此您无法在步骤情况中立即应用 esuc。您将需要使用重写来重新组织 Even ((m +2) + n) 的目标类型(或 Even (m + (n +2)) code> 取决于您对哪个参数执行归纳) 到 Even ((m + n) +2) 事先。