Помощь Агда

Ответ 1

Контроллер завершения сеанса Agda проверяет только структурную рекурсию (т.е. вызовы, которые происходят на структурно меньших аргументах), и нет способа установить, что определенное отношение (например, _<_) подразумевает, что один из аргументов структурно меньше.

Отступление: Аналогичная проблема возникает при проверке положительности. Рассмотрим стандартный тип данных фиксированной точки:

data μ_ (F : Set → Set) : Set where
  fix : F (μ F) → μ F

Агда отвергает это, потому что F может не быть положительным в своем первом аргументе. Но мы не можем ограничивать μ только положительными функциями типа или показать, что некоторая функция определенного типа положительна.

Как мы обычно показываем, что рекурсивные функции завершаются? Для натуральных чисел это тот факт, что если рекурсивный вызов происходит на строго меньшем числе, мы в конечном итоге должны достигнуть нуля и рекурсия прекратится; для списков одинаковые значения для его длины; для множеств мы могли бы использовать строгое подмножество; и так далее. Обратите внимание, что "строго меньшее число" не работает для целых чисел.

Собственность, которую разделяют все эти отношения, называется обоснованностью. Неформально говоря, отношение обосновано, если у него нет бесконечных нисходящих цепей. Например, < для натуральных чисел является обоснованным, поскольку для любого числа n:

n > n - 1 > ... > 2 > 1 > 0

То есть длина такой цепи ограничена n + 1.

≤ на натуральные числа, однако, не является обоснованным:

n ≥ n ≥ ... ≥ n ≥ ...

И ни один < для целых чисел:

n > n - 1 > ... > 1 > 0 > -1 > ...

Помогает ли это нам? Оказывается, мы можем кодировать, что это значит, чтобы отношение было обоснованным в Agda, а затем использовать его для реализации вашей функции.

Для простоты я собираюсь испечь отношение _<_ к типу данных. Прежде всего, мы должны определить, что означает доступность числа: n доступен, если все m такие, что m < n также доступны. Это, конечно, останавливается на n = 0, потому что нет m, так что m < 0 и это утверждение выполняется тривиально.

data Acc (n : ℕ) : Set where
  acc : (∀ m → m < n → Acc m) → Acc n

Теперь, если мы можем показать, что все натуральные числа доступны, мы показали, что < является обоснованным. Почему это так? Должно быть конечное число конструкторов acc (т.е. Бесконечной нисходящей цепочки), потому что Agda не позволит нам писать бесконечную рекурсию. Теперь может показаться, что мы просто подтолкнули проблему назад на один шаг дальше, но написание доказательства обоснованности на самом деле структурно рекурсивно!

Итак, имея в виду, здесь определение < является обоснованным:

WF : Set
WF = ∀ n → Acc n

И доказательство обоснованности:

<-wf : WF
<-wf n = acc (go n)
  where
  go : ∀ n m → m < n → Acc m
  go zero    m       ()
  go (suc n) zero    _         = acc λ _ ()
  go (suc n) (suc m) (s≤s m<n) = acc λ o o<sm → go n o (trans o<sm m<n)

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

open import Data.Nat
open import Relation.Binary

open DecTotalOrder decTotalOrder
  using (trans)

Далее нам понадобится доказательство того, что ⌊ n /2⌋ ≤ n:

/2-less : ∀ n → ⌊ n /2⌋ ≤ n
/2-less zero          = z≤n
/2-less (suc zero)    = z≤n
/2-less (suc (suc n)) = s≤s (trans (/2-less n) (right _))
  where
  right : ∀ n → n ≤ suc n
  right zero    = z≤n
  right (suc n) = s≤s (right n)

И, наконец, мы можем написать вашу функцию F. Обратите внимание на то, как он становится структурно рекурсивным благодаря acc: рекурсивные вызовы происходят из аргументов с одним отстроенным конструктором acc.

f : ℕ → ℕ
f n = go _ (<-wf n)
  where
  go : ∀ n → Acc n → ℕ
  go zero    _       = 0
  go (suc n) (acc a) = go ⌊ n /2⌋ (a _ (s≤s (/2-less _)))

Теперь работать с acc напрямую не очень приятно. И это, где приходит ответ Доминика. Все это, что я написал здесь, уже было сделано в стандартной библиотеке. Он более общий (тип данных acc на самом деле параметризирован над отношением), и он позволяет вам просто использовать <-rec, не беспокоясь о acc.

Взяв более пристальный взгляд, мы на самом деле довольно близки к общему решению. Посмотрим, что получим, когда мы параметризируем отношение. Для простоты я не имею дело с полиморфизмом Вселенной.

Отношение на A - это просто функция, принимающая два A и возвращающая Set (мы можем назвать бинарный предикат):

Rel : Set → Set₁
Rel A = A → A → Set

Мы можем легко обобщить acc, изменив hardcoded _<_ : ℕ → ℕ → Set на произвольное отношение по некоторому типу A:

data Acc {A} (_<_ : Rel A) (x : A) : Set where
  acc : (∀ y → y < x → Acc _<_ y) → Acc _<_ x

Соответственно определяется определение обоснованности:

WellFounded : ∀ {A} → Rel A → Set
WellFounded _<_ = ∀ x → Acc _<_ x

Теперь, поскольку acc является индуктивным типом данных, как и любой другой, мы должны иметь возможность написать его выпрямитель. Для индуктивных типов это сводка (так же, как foldr является выпрямителем для списков) - мы говорим выпрямителю, что делать с каждым случаем конструктора, а выпрямитель применяет это ко всей структуре.

В этом случае мы просто отлично справимся с простым вариантом:

foldAccSimple : ∀ {A} {_<_ : Rel A} {R : Set} →
                (∀ x → (∀ y → y < x → R) → R) →
                ∀ z → Acc _<_ z → R
foldAccSimple {R = R} acc′ = go
  where
  go : ∀ z → Acc _ z → R
  go z (acc a) = acc′ z λ y y<z → go y (a y y<z)

Если мы знаем, что _<_ является обоснованным, мы можем полностью пропустить аргумент Acc _<_ z, поэтому напишите небольшую удобную оболочку:

recSimple : ∀ {A} {_<_ : Rel A} → WellFounded _<_ → {R : Set} →
            (∀ x → (∀ y → y < x → R) → R) →
            A → R
recSimple wf acc′ z = foldAccSimple acc′ z (wf z)

И наконец:

<-wf : WellFounded _<_
<-wf = {- same definition -}

<-rec = recSimple <-wf

f : ℕ → ℕ
f = <-rec go
  where
  go : ∀ n → (∀ m → m < n → ℕ) → ℕ
  go zero    _ = 0
  go (suc n) r = r ⌊ n /2⌋ (s≤s (/2-less _))

И действительно, это выглядит (и работает) почти так же, как в стандартной библиотеке!

Здесь полностью зависимая версия в случае, если вам интересно:

foldAcc : ∀ {A} {_<_ : Rel A} (P : A → Set) →
          (∀ x → (∀ y → y < x → P y) → P x) →
          ∀ z → Acc _<_ z → P z
foldAcc P acc′ = go
  where
  go : ∀ z → Acc _ z → P z
  go _ (acc a) = acc′ _ λ _ y<z → go _ (a _ y<z)

rec : ∀ {A} {_<_ : Rel A} → WellFounded _<_ →
      (P : A → Set) → (∀ x → (∀ y → y < x → P y) → P x) →
      ∀ z → P z
rec wf P acc′ z = foldAcc P acc′ _ (wf z)

Ответ 2

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

Идея здесь в том, что проблема заключается в невозможности увидеть, что n / 2 является как-то "частью" n. Структурная рекурсия хочет разбить вещь на ее непосредственные части, но способ, которым n / 2 является "частью" n, заключается в том, что мы отбрасываем все остальные suc. Но это не очевидно, сколько из них нужно сбросить, мы должны осмотреться и попытаться разобраться. Что было бы неплохо, если бы у нас был тип, у которого были конструкторы для "multiple" suc s.

Чтобы сделать проблему несколько более интересной, пусть вместо этого попытается определить функцию, которая ведет себя как

f : ℕ → ℕ
f 0 = 0
f (suc n) = 1 + (f (n / 2))

т.е. должно быть, что

f n = ⌈ log₂ (n + 1) ⌉

Теперь, естественно, вышеприведенное определение не будет работать, по тем же причинам ваш f не будет. Но пусть делает вид, что это так, и пусть исследует "путь" , так сказать, что аргумент будет проходить через натуральные числа. Предположим, что мы смотрим на n = 8:

f 8 = 1 + f 4 = 1 + 1 + f 2 = 1 + 1 + 1 + f 1 = 1 + 1 + 1 + 1 + f 0 = 1 + 1 + 1 + 1 + 0 = 4

поэтому "путь" равен 8 -> 4 -> 2 -> 1 -> 0. Как насчет, скажем, 11?

f 11 = 1 + f 5 = 1 + 1 + f 2 = ... = 4

поэтому "путь" равен 11 -> 5 -> 2 -> 1 -> 0.

Ну, естественно, что здесь происходит то, что на каждом шаге мы либо делим на 2, либо вычитаем один, и разделим на 2. Каждое натуральное число, большее 0, может быть разложено однозначно таким образом. Если он четный, разделите на два и продолжайте, если он нечетный, вычтите один и разделите на два и продолжайте.

Итак, теперь мы можем точно видеть, как должен выглядеть наш тип данных. Нам нужен тип с конструктором, который означает "в два раза больше suc", а другой означает "в два раза больше suc плюс один", а также, конечно, конструктор, который означает "zero suc s":

data Decomp : ℕ → Set where
  zero : Decomp zero
  2*_ : ∀ {n} → Decomp n → Decomp (n * 2)
  2*_+1 : ∀ {n} → Decomp n → Decomp (suc (n * 2))

Теперь мы можем определить функцию, которая разбивает натуральное число на соответствующий ему Decomp:

decomp : (n : ℕ) → Decomp n
decomp zero = zero
decomp (suc n) = decomp n +1

Это помогает определить +1 для Decomp s:

_+1 : {n : ℕ} → Decomp n → Decomp (suc n)
zero +1 = 2* zero +1
(2* d) +1 = 2* d +1
(2* d +1) +1 = 2* (d +1)

Учитывая a Decomp, мы можем разложить его на натуральное число, которое игнорирует различия между 2*_ и 2*_+1:

flatten : {n : ℕ} → Decomp n → ℕ
flatten zero = zero
flatten (2* p) = suc (flatten p)
flatten (2* p +1 = suc (flatten p)

И теперь тривиально определить f:

f : ℕ → ℕ
f n = flatten (decomp n)

Это с радостью проходит проверку завершения без проблем, потому что мы никогда не возвращаемся к проблемному n / 2. Вместо этого мы преобразуем число в формат, который непосредственно представляет его путь через числовое пространство структурно рекурсивным способом.

Изменить Мне только недавно показалось, что Decomp представляет собой малозначное представление двоичных чисел. 2*_ означает "добавить 0 к концу/сдвигу влево 1 бит", а 2*_+1 "добавить 1 к концу/сдвигу влево 1 бит и добавить один". Таким образом, приведенный выше код действительно показывает, что двоичные числа структурно рекурсивны, делятся на 2, что они должны быть! Мне кажется, это намного легче понять, но я не хочу менять то, что я написал, поэтому мы могли бы вместо этого переименовать здесь: Decomp ~ > Binary, 2*_ ~ > _,zero, 2*_+1 ~ > _,one, Decomp ~ > natToBin, flatten ~ > countBits.

Ответ 3

После принятия ответа Витуса я обнаружил другой способ достижения цели, заключающейся в том, что функция заканчивается в Agda, а именно, используя "размерные типы". Я предоставляю свой ответ здесь, потому что это кажется приемлемым, а также для критики любых слабых сторон этого ответа.

Описанные типы описаны: http://arxiv.org/pdf/1012.4896.pdf

Они реализованы в Agda, а не только MiniAgda; см. здесь: http://www2.tcs.ifi.lmu.de/~abel/talkAIM2008Sendai.pdf.

Идея состоит в том, чтобы увеличить тип данных с размером, который позволяет typechecker более легко доказать завершение. Размер определяется в стандартной библиотеке.

open import Size

Мы определяем натуральные числа размера:

data Nat : {i : Size} \to Set where
    zero : {i : Size} \to Nat {\up i} 
    succ : {i : Size} \to Nat {i} \to Nat {\up i}

Далее мы определяем предшественник и вычитание (monus):

pred : {i : Size} → Nat {i} → Nat {i}
pred .{↑ i} (zero {i}) = zero {i}
pred .{↑ i} (succ {i} n) = n 

sub : {i : Size} → Nat {i} → Nat {∞} → Nat {i}
sub .{↑ i} (zero {i}) n = zero {i}
sub .{↑ i} (succ {i} m) zero = succ {i} m
sub .{↑ i} (succ {i} m) (succ n) = sub {i} m n

Теперь мы можем определить деление по алгоритму Евклида:

div : {i : Size} → Nat {i} → Nat → Nat {i}
div .{↑ i} (zero {i}) n = zero {i}
div .{↑ i} (succ {i} m) n = succ {i} (div {i} (sub {i} m n) n)

data ⊥ : Set where
record ⊤ : Set where
notZero :  Nat → Set
notZero zero = ⊥
notZero _ = ⊤

Дадим деление для ненулевых знаменателей. Если знаменатель отличен от нуля, то он имеет вид b + 1. Затем мы делаем divPos a (b + 1) = div a b Поскольку div a b возвращает потолок (a/(b + 1)).

divPos : {i : Size} → Nat {i} → (m : Nat) → (notZero m) → Nat {i}
divPos a (succ b) p = div a b
divPos a zero ()

В качестве вспомогательного:

div2 : {i : Size} → Nat {i} → Nat {i}
div2 n = divPos n (succ (succ zero)) (record {})

Теперь мы можем определить метод деления и завоевания для вычисления n-го числа Фибоначчи.

fibd : {i : Size} → Nat {i} → Nat
fibd zero = zero
fibd (succ zero) = succ zero
fibd (succ (succ zero)) = succ zero
fibd (succ n) with even (succ n)
fibd .{↑ i}  (succ {i} n) | true = 
  let
    -- When m=n+1, the input, is even, we set k = m/2
    -- Note, ceil(m/2) = ceil(n/2)
    k = div2 {i} n
    fib[k-1] = fibd {i} (pred {i} k)
    fib[k] = fibd {i} k
    fib[k+1] =  fib[k-1] + fib[k]
  in
    (fib[k+1] * fib[k]) + (fib[k] * fib[k-1])
fibd .{↑ i} (succ {i} n) | false = 
  let
    -- When m=n+1, the input, is odd, we set k = n/2 = (m-1)/2.
    k = div2 {i} n
    fib[k-1] = fibd {i} (pred {i} k)
    fib[k] = fibd {i} k
    fib[k+1] = fib[k-1] + fib[k]
  in
    (fib[k+1] * fib[k+1]) + (fib[k] * fib[k])

Ответ 4

Вы не можете сделать это напрямую: проверка окончания сеанса Agda учитывает только рекурсию ok на синтаксически меньших аргументах. Тем не менее, стандартная библиотека Agda предоставляет несколько модулей для подтверждения завершения с использованием обоснованного порядка между аргументами функций. Стандартный порядок на натуральных числах такой порядок и может быть использован здесь.

Используя код в Induction. *, вы можете написать свою функцию следующим образом:

open import Data.Nat
open import Induction.WellFounded
open import Induction.Nat

s≤′s : ∀ {n m} → n ≤′ m → suc n ≤′ suc m
s≤′s ≤′-refl = ≤′-refl
s≤′s (≤′-step lt) = ≤′-step (s≤′s lt)

proof : ∀ n → ⌊ n /2⌋ ≤′ n
proof 0 = ≤′-refl
proof 1 = ≤′-step (proof zero)
proof (suc (suc n)) = ≤′-step (s≤′s (proof n))

f : ℕ → ℕ
f = <-rec (λ _ → ℕ) helper
  where
    helper : (n : ℕ) → (∀ y → y <′ n → ℕ) → ℕ
    helper 0 rec = 0
    helper (suc n) rec = rec ⌊ n /2⌋ (s≤′s (proof n))

Я нашел статью с некоторым объяснением здесь. Но там могут быть лучшие ссылки.

Ответ 5

Подобный вопрос появился в рассылке Agda несколько недель назад, и консенсус, казалось, заключался в том, чтобы вставить элемент Data.Nat в Data.Bin, а затем использовать структурную рекурсию в этом представлении, которая хорошо подходит для задания под рукой.

Здесь вы можете найти целую цепочку: http://comments.gmane.org/gmane.comp.lang.agda/5690

Ответ 6

Вы можете избежать использования обоснованной рекурсии. Скажем, вам нужна функция, которая применяет ⌊_/2⌋ к числу, пока не достигнет 0, и соберет результаты. С помощью {-# TERMINATING #-} прагмы это можно определить следующим образом:

{-# TERMINATING #-}
⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s 0 = []
⌊_/2⌋s n = n ∷ ⌊ ⌊ n /2⌋ /2⌋s

Второе предложение эквивалентно

⌊_/2⌋s n = n ∷ ⌊ n ∸ (n ∸ ⌊ n /2⌋) /2⌋s

Можно сделать структурную рекурсивность ⌊_/2⌋s путем вложения этой подстановки:

⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s = go 0 where
  go : ℕ -> ℕ -> List ℕ
  go  _       0      = []
  go  0      (suc n) = suc n ∷ go (n ∸ ⌈ n /2⌉) n
  go (suc i) (suc n) = go i n

go (n ∸ ⌈ n /2⌉) n является упрощенной версией go (suc n ∸ ⌊ suc n /2⌋ ∸ 1) n

Некоторые тесты:

test-5 : ⌊ 5 /2⌋s ≡ 5 ∷ 2 ∷ 1 ∷ []
test-5 = refl

test-25 : ⌊ 25 /2⌋s ≡ 25 ∷ 12 ∷ 6 ∷ 3 ∷ 1 ∷ []
test-25 = refl

Теперь скажем, что вам нужна функция, которая применяет ⌊_/2⌋ к числу, пока не достигнет 0, и суммирует результаты. Это просто

⌊_/2⌋sum : ℕ -> ℕ
⌊ n /2⌋sum = go ⌊ n /2⌋s where
  go : List ℕ -> ℕ
  go  []      = 0
  go (n ∷ ns) = n + go ns

Итак, мы можем просто запустить нашу рекурсию в списке, который содержит значения, созданные функцией ⌊_/2⌋s.

Более сжатая версия

⌊ n /2⌋sum = foldr _+_ 0 ⌊ n /2⌋s

И вернемся к основам.

open import Function
open import Relation.Nullary
open import Relation.Binary
open import Induction.WellFounded
open import Induction.Nat

calls : ∀ {a b ℓ} {A : Set a} {_<_ : Rel A ℓ} {guarded : A -> Set b}
      -> (f : A -> A)
      -> Well-founded _<_
      -> (∀ {x} -> guarded x -> f x < x)
      -> (∀ x -> Dec (guarded x))
      -> A
      -> List A
calls {A = A} {_<_} f wf smaller dec-guarded x = go (wf x) where
  go : ∀ {x} -> Acc _<_ x -> List A
  go {x} (acc r) with dec-guarded x
  ... | no  _ = []
  ... | yes g = x ∷ go (r (f x) (smaller g))

Эта функция выполняет ту же функцию, что и функция ⌊_/2⌋s, т.е. создает значения для рекурсивных вызовов, но для любой функции, удовлетворяющей определенным условиям.

Посмотрите на определение go. Если x не guarded, верните []. В противном случае добавьте x и вызовите go на f x (мы могли бы написать go {x = f x} ...), который структурно меньше.

Мы можем переопределить ⌊_/2⌋s в терминах calls:

⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s = calls {guarded = ?} ⌊_/2⌋ ? ? ?

⌊ n /2⌋s возвращает [], только когда n равен 0, поэтому guarded = λ n -> n > 0.

Наше обоснованное отношение основано на _<′_ и определено в модуле Induction.Nat как <-well-founded.

Итак, мы имеем

⌊_/2⌋s = calls {guarded = λ n -> n > 0} ⌊_/2⌋ <-well-founded {!!} {!!}

Тип следующего отверстия {x : ℕ} → x > 0 → ⌊ x /2⌋ <′ x

Нетрудно доказать это предложение:

open import Data.Nat.Properties

suc-⌊/2⌋-≤′ : ∀ n -> ⌊ suc n /2⌋ ≤′ n
suc-⌊/2⌋-≤′  0      = ≤′-refl
suc-⌊/2⌋-≤′ (suc n) = s≤′s (⌊n/2⌋≤′n n)

>0-⌊/2⌋-<′ : ∀ {n} -> n > 0 -> ⌊ n /2⌋ <′ n
>0-⌊/2⌋-<′ {suc n} (s≤s z≤n) = s≤′s (suc-⌊/2⌋-≤′ n)

Тип последнего отверстия (x : ℕ) → Dec (x > 0), мы можем заполнить его _≤?_ 1.

И последнее определение

⌊_/2⌋s : ℕ -> List ℕ
⌊_/2⌋s = calls ⌊_/2⌋ <-well-founded >0-⌊/2⌋-<′ (_≤?_ 1)

Теперь вы можете записаться в список, созданный ⌊_/2⌋s, без каких-либо проблем с завершением.