Каковы недостатки свойств кодирования с использованием функций?

Question

В Агде кажется, что часто есть два способа улучшить набор. Один из них - просто написать функцию, которая проверяет, сохраняется ли свойство, и поднимать. Например:

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 функций. Может также называться «рекурсивно определенным» или «определенным большим исключением».

Третья версия в Агде:

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, без постулатов или дополнительных доказательств разрешимости.

Во-вторых, о практических последствиях в Агде / Идрисе .

• Вы можете сделать зависимое сопоставление с образцом на основе доказательств индуктивных предикатов. С рекурсивными и булевыми предикатами вы должны сначала сопоставить шаблон по значениям A, чтобы свидетели-предикаты вычислялись. Иногда это делает индуктивные предикаты удобными, например, у вас может быть тип перечисления с 10 конструкторами, и вы хотите, чтобы предикат содержал только один конструктор. Индуктивно определенный предикат позволяет вам сопоставлять только истинный случай, в то время как другие версии требуют, чтобы вы соответствовали всем случаям все время.

• С другой стороны, логические и рекурсивные предикаты вычисляются автоматически, как только вы узнаете, что элемент A имеет заданную форму. Это можно использовать в Agda, чтобы сделать вывод типа заполнять доказательства автоматически, без тактики или случаев. Например, дырочный или неявный аргумент с типом hastrue xs может быть решен с помощью правил eta для пар и типа модуля, когда xs является выражением списка с известным true-содержащим префиксом. Это работает аналогично логическим предикатам.