Метод Бове-Капретты (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, который не страдает той же проблемой, поскольку нормализует выражения перед проверкой на завершение, и, следовательно, предлагает подход "леммы инверсии" успешен.)