Fixpoint / fix разрешает только рекурсивные вызовы с синтаксически меньшим аргументом .
Fixpoint example (n : nat) :=
... (* There must be a match on [n] somewhere *)
... match n with
| O => base_case (* no recursive call allowed *)
| S m =>
... (example m)
(* We can only call [example] on [m], or some even smaller value obtained by matching on [m] *)
end ...
В частности, нельзя делать рекурсивный вызов значения, полученного с помощью некоторой произвольной функции (в данном случае div и sub в copy2 a ((i-1) / 2)).
Вот три варианта:
Выберите другое представление натуральных чисел, чтобы сопоставление с образцом на нем естественно разложилось на различные ветви желаемого определения (базовый случай (ноль), четный, нечетный).
Используйте тот факт, что глубина рекурсии на самом деле ограничена n, поэтому мы можем использовать n в качестве "топлива", которое, как мы знаем, на самом деле не будет исчерпано до того, как мы закончим.
Хитро извлеките подтерму убывающего аргумента, чтобы сделать рекурсивный вызов. Это решение является менее общим и надежным, чем предыдущие; это гораздо сложнее бороться с проверкой завершения.
Альтернативное представление
У нас есть три случая: ноль, чет и нечет. К счастью, стандартная библиотека имеет тип с почти такой же структурой, positive:
Inductive positive := (* p > 0 *)
| xH (* 1 *)
| xI (p : positive) (* 2p + 1 *)
| xO (p : positive) (* 2p *)
.
Указав тип positive с дополнительным нулем, получим N:
Inductive N :=
| N0 (* 0 *)
| Npos (p : positive) (* p > 0 *)
.
Существует также функция преобразования N.of_nat : nat -> N, хотя было бы также неплохо использовать N везде вместо nat, если преобразования становятся слишком раздражающими.
Окончательное определение начинается с анализа случая на N, и дело, раскрывающее число positive, обрабатывается с точкой fix, где базовый случай равен 1 вместо 0. Мы должны сдвинуть некоторые детали , поскольку четный случай равен 2p вместо 2p + 2, поэтому вместо пары деревьев размером (i + 1, i) мы должны выполнить (i-1, i). Но в целом рекурсивные случаи все еще естественно соответствуют неформальной спецификации:
Require Import NArith PArith.
Parameter V : Type.
Inductive BraunTree : Type :=
| E : BraunTree
| T: V -> BraunTree -> BraunTree -> BraunTree.
Definition copy (x : V) (n : N) : BraunTree :=
match n with
| N0 => E
| Npos p =>
let
(* copy2 a i : a tree of (i-1) copies of a, and another of i copies of a *)
fix copy2 (a : V) (i : positive) : (BraunTree * BraunTree) :=
match i with
| xH => (* i = 1 *)
(E, T a E E)
| xI p => (* i = 2p + 1 *)
let (s,t) := copy2 a p in
((T a t s),(T a t t))
| xO p => (* i = 2p *)
let (s,t) := copy2 a p in
((T a s s),(T a t s))
end
in
match copy2 x p with
|(_,snd) => snd
end
end.
Достаточно топлива
Мы добавляем топливо к fix в качестве убывающего аргумента. Мы можем только закончить, если n = i = 0, поэтому мы знаем, каков будет результат.
(* note: This doesn't need to be a Fixpoint *)
Definition copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (n : nat) (i : nat) : (BraunTree * BraunTree) :=
match n with
| O => (T a E E,E)
| S n' =>
match i with
| O => (T a E E,E)
| _ =>
if Nat.odd i then
let m := div2 ((i - 1) / 2) in
let (s,t) := copy2 a n' m in
((T a s t),(T a t t))
else
let m := div2 ((i - 2) / 2) in
let (s,t) := copy2 a n' m in
((T a s s),(T a s t))
end
end
in
match copy2 x n n with
|(_,snd) => snd
end.
Это хорошо работает, когда:
- мы можем вычислить количество необходимого топлива;
- и есть предсказуемый ответ, когда у нас кончится топливо.
Если какое-либо из этих предположений не выполняется, нам нужно засорить наш код с помощью option.
вложенная рекурсия
Как упоминалось ранее, Coq имеет строгие правила об уменьшении аргументов. Обычное объяснение состоит в том, что мы можем сделать рекурсивный вызов только для подтермы, полученной путем сопоставления с образцом для убывающего аргумента (или транзитивно, одного из его подтермов).
Одним из очевидных ограничений является то, что, поскольку условие является синтаксическим (т. Е. Coq смотрит на определение, чтобы отследить происхождение убывающего аргумента), аргумент n может только уменьшаться не более чем на постоянную (постоянную по отношению к n), поскольку в определении только конечное число match. В частности, нет способа сделать рекурсивный вызов результата деления на два, поскольку это представляет уменьшение на n/2, линейное значение в n.
К лучшему или к худшему, критерий завершения Coq на самом деле немного умнее, чем этот: можно передать убывающий аргумент во вложенную точку фиксации, и через него будет отслеживаться отношение «подтермы».
Безбилетное деление
И действительно, деление Пеано nat может быть определено таким образом, что Coq может сказать, что результат представляет собой подтерму дивиденда:
Definition div2 (n : nat) :=
let fix d2 (n1 : nat) (n2 : nat) {struct n1} :=
match n2 with
| S (S n2') =>
match n1 with
| O => n1
| S n1' => d2 n1' n2'
end
| _ => n1
end
in d2 n n.
Идея состоит в том, чтобы написать fix -точку из двух аргументов (что-то вроде решения для топлива), которые начинаются с равенства (d2 n n), и мы удаляем два S конструкторов из один (n2) из них на каждый один S, который мы удаляем из другого (n1). Важные детали:
Во всех непериодических случаях мы возвращаем n1 (и , а не 0 в любом случае), что гарантированно будет подтермой самого верхнего n .
И функция должна уменьшаться в n1 (термин, который мы возвращаем), а не n2 (Coq отслеживает только подтермы убывающих аргументов).
Все это гарантирует, что div2 n является подтермой n (а не строгим подтермом (или надлежащим подтермом ), поскольку n может быть O).
Это имеет сходство с предыдущим решением на основе топлива, но здесь аргумент уменьшения намного важнее, чем просто устройство для обмана проверщика типов.
Этот метод является вариантом программирование без минусов .(Обратите внимание, что ограничения не совсем такие же, как обсуждаемые в литературе, например, когда основное внимание уделяется избеганию выделения памяти , а не обеспечению завершения структурной обоснованностью.)
Вывод: определение copy
Получив div2, мы можем определить copy с несколькими настройками, чтобы получить i-1 и i-2 как правильные подтермы из i, опять же путем сопоставления с образцом.Ниже i' и i'' являются правильными подтермами i (визуальным осмотром), а div2 i' и div2 i'' являются подтермами i' и i'' (по определению div2).По транзитивности они являются правильными подтермами i, поэтому проверка завершения принимает.
Definition copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) :=
match i with
| 0 => (T a E E,E)
| S i' => (* i' = i-1 *)
if Nat.odd i then
let m := div2 i' in
let (s,t) := copy2 a m in
((T a s t),(T a t t))
else
match i' with
| O => (* Unreachable *) (E, E)
| S i'' => (* i'' = i-2 *)
let m := div2 i'' in
let (s,t) := copy2 a m in
((T a s s),(T a s t))
end
end
in
match copy2 x n with
|(_,snd) => snd
end.