Предикат Бове-Капретты в опоре - PullRequest
Новая
       70

Предикат Бове-Капретты в опоре

2 голосов
/ 02 августа 2020

Метод Бове-Капретты (http://www.cs.nott.ac.uk/~pszvc/publications/General_Recursion_MSCS_2005.pdf) - изящный трюк для моделирования неструктурно рекурсивных или частичных функций в таких языках, как Agda. Завершающие входы функции характеризуются индуктивным предикатом, и функция переписывается, чтобы принимать предикат в качестве аргумента.

Например, предположим, что мы хотели написать следующее определение логарифма с основанием 2 в Agda (с использованием модуля Data.Nat): 

log2 : ℕ → ℕ
log2 0 = 0
log2 1 = 0
log2 n = suc (log2 ⌊ n /2⌋)

К сожалению, это определение не проходит проверку завершения. Следуя Бове-Капретте, можно было бы определить следующий предикат: 

data Loggable : ℕ → Set where
    log-n≡0 : Loggable 0
    log-n≡1 : Loggable 1
    log-n≡n : ∀ {n} → Loggable ⌊ n /2⌋ → Loggable n

А затем расширить исходное определение, приняв Loggable в качестве дополнительного аргумента: 

log2 : (n : ℕ) → Loggable n → ℕ
log2 0 _ = 0
log2 1 _ = 1
log2 n (log-n≡n p) = suc (log2 ⌊ n /2⌋ p)

Теперь это успешно проходит средство проверки завершения, поскольку предикат Loggable служит аргументом, уменьшающим структуру. Все это работает, как и ожидалось.

Теперь, поскольку предикат используется исключительно для убеждения проверяющего завершения, имеет смысл переместить его в сортировку Prop, поскольку он не должен иметь никакого вычислительного эффекта. В самом деле, изучение нашего нового определения log2 также предполагает это, поскольку предикат не используется для каких-либо разделений регистра, которые еще не были определены другим аргументом.

Вот где проблема. Во-первых, создание Loggable a Prop запрещает разделение регистра, когда мы производим что-то в сортировке Set, как в нашей новой функции log2. Обычным решением этого является введение вспомогательной «леммы об обращении», работающей в sort Prop, которая разрушает предикат и извлекает нужную нам часть. К сожалению, это создает новую проблему - структурное завершение log2 будет нарушено, так как Agda не видит, что результат вызова «леммы инверсии» структурно меньше, чем его вход.

(Примечание что эквивалент этой проблемы может быть написан на Coq, который не страдает той же проблемой, поскольку нормализует выражения перед проверкой на завершение, и, следовательно, предлагает подход "леммы инверсии" успешен.)

1 Ответ

3 голосов
/ 05 августа 2020

В отличие от Prop в Coq (но, как и sProp), юниверс Agda Prop поддерживает несоответствие определения . Это означает, что любые два элемента типа в Prop по определению равны проверке преобразования. С другой стороны, это также означает, что оценка термина никогда не может застрять на аргументе типа в Prop, и, следовательно, эти аргументы не могут использоваться для доказательства завершения. К сожалению, это означает, что метод Бове-Капретты не работает со вселенной Prop Agda.

...