Понимание практического экзамена об Агде

Question

Я прохожу практический экзамен по языковым фондам программирования с использованием agda, и у меня есть следующий вопрос:

Вам выдается следующая декларация Агды:

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

Предположим, что стандартная библиотека натуральных чисел была импортирована. Ответьте на следующие вопросы:

а) Какого типа ezero?

б) Есть ли условия типа Even 1?

в) Сколько терминов имеют тип Even 2? Перечислить их

d) Опишите одну потенциальную проблему, которая может возникнуть, если мы изменим тип возвращаемого значения esuc на Even (n+2) вместо Even (2+n),

Нам не предоставлено руководство по решению. Вопрос кажется довольно простым, но я не уверен ни в одном из них. Я думаю, что ответ на первые три:

множество

б) нет условий типа даже 1

в) Один член типа Эвен 2

г) не знаю

Ответы на эти вопросы вместе с кратким объяснением будут высоко оценены. Спасибо

Answer 1

Какой тип ezero?

Тип конструктора данных ezero можно прочитать из декларации данных: ezero : Even 0 утверждает, что имеет тип Even 0,

Есть ли условия типа Even 1?

Нет, их нет. Это можно увидеть по разнице в регистре: если бы существовал термин, он начинался бы с одного из двух конструкторов. И поскольку у них есть конкретные индексы доходности, им придется объединиться с 1,

• ezero будет обеспечивать 1 = 0
• esuc будет означать, что есть п, что 1 = 2+ n

Обе эти ситуации невозможны.

Сколько терминов типа Even 2? Перечислить их

Есть ровно одно: esuc ezero, С аргументацией, аналогичной приведенной в предыдущем вопросе, мы можем доказать, что ezero а также esuc (esuc p) (для некоторых p) не будет делать.

Опишите одну потенциальную проблему, которая может возникнуть, если мы изменим тип возвращаемого значения esuc быть Even (n+2) вместо Even (2+n),

Рассмотрим доказательство plus-Even : {m n : N} → Even m → Even n → Even (m + n), Так как (+) определяется индукцией по первому аргументу, вы не сможете сразу применить esuc в случае шага. Вам нужно будет использовать переписывание, чтобы реорганизовать тип цели из Even ((m +2) + n) (или же Even (m + (n +2)) в зависимости от того, по какому аргументу Even ((m + n) +2) заранее.