Рассмотрим индуктивный тип, который имеет некоторые рекурсивные вхождения во вложенном, но строго положительном месте. Например, деревья с конечным ветвлением с узлами, использующими общую структуру данных списка для хранения дочерних элементов.
Inductive LTree : Set := Node : list LTree -> LTree.
Наивный способ определения рекурсивной функции над этими деревьями путем рекурсии над деревьями и списками деревьев не работает. Вот пример с size
функцией, которая вычисляет количество узлов.
Fixpoint size (t : LTree) : nat := match t with Node l => 1 + (size_l l) end
with size_l (l : list LTree) : nat := match l with
| nil => 0
| cons h r => size h + size_l r
end.
Это определение неверно сформировано (выдается сообщение об ошибке):
Error:
Recursive definition of size_l is ill-formed.
Recursive call to size has principal argument equal to
"h" instead of "r".
Почему определение плохо сформировано, хотя r
оно явно является подтермой l
? Есть ли способ определить рекурсивные функции в такой структуре данных?
Если вы не владеете синтаксисом Coq: LTree
это индуктивный тип, соответствующий следующей грамматике.
Мы пытаемся определить size
функцию по индукции по деревьям и спискам. В OCaml это будет:
type t = Node of t list
let rec size = function Node l -> 1 + size_l l
and size_l = function [] -> 0
| h::r -> size h + size_l r
источник
Ответы:
Что работает
Если вы вложите определение точки фиксации в списки внутри определения точки фиксации на деревьях, результат будет хорошо напечатан. Это общий принцип, когда у вас есть вложенная рекурсия в индуктивном типе, т.е. когда рекурсия проходит через конструктор типа
list
.Или, если вы предпочитаете писать это более кратко:
(Я понятия не имею, от кого я это услышал в первый раз; это, безусловно, было открыто независимо много раз.)
Предикат общей рекурсии
В более общем смысле вы можете определить «правильный» принцип индукции при включении
LTree
вручную. Автоматически сгенерированный принцип индукцииLTree_rect
опускает гипотезу в списке, потому что генератор принципа индукции понимает только не вложенные строго положительные вхождения индуктивного типа.Давайте добавим гипотезу индукции в списки. Чтобы выполнить его в рекурсивном вызове, мы вызываем принцип индукции списка и передаем его принципу индукции дерева в меньшем дереве внутри списка.
Почему
Ответ на вопрос заключается в точных правилах принятия рекурсивных функций. Эти правила выполняются тонко, поскольку существует тонкий баланс между разрешением сложных случаев (таких как этот, с вложенной рекурсией в типе данных) и несостоятельностью. Coq Справочное руководство вводит язык (исчисление индуктивных конструкций, что является доказательством язык Coq), в основном , с формально точными определениями, но если вы хотите точные правила относительно индукции и коиндукции вам нужно пойти в научно - исследовательских работ, на эту тему Эдуардо Хименес [1].
Начиная с руководства Coq, в нотацииFixfi{f1:A1:=t1;f2:A2:=t2}
Fix
правила у нас есть определение фиксированной точки где:Для того чтобы определение с фиксированной точкой было принято, «если встречается [в ], то… аргумент должен быть синтаксически распознан как структурно меньший, чем [аргумент, переданный в ]» (упрощение, потому что функции имеют единственный аргумент). Здесь мы должны проверить, чтот I е Ifj ti fi
l
t
size
h
l
size_l
r
l
size_l
Причина, по которой
h
он не является структурно меньше, чемl
согласно интерпретатору Coq, мне не ясна. Насколько я понимаю из обсуждений по списку Coq-club [1] [2], это ограничение в интерпретаторе, которое в принципе можно снять, но очень осторожно, чтобы не допустить несоответствия.Ссылки
Cocorico, неопределенный Coq wiki: Взаимная индукция
Список рассылки Coq-Club:
Команда разработчиков Coq. Coq Proof Assistant: Справочное руководство . Версия 8.3 (2010). [ веб ] гл. 4 .
Эдуардо Хименес. Кодификация охраняемых определений с помощью рекурсивных схем . В Types'94: Типы для доказательств и программ , LNCS 996. Springer-Verlag, 1994. doi: 10.1007 / 3-540-60579-7_3 [ Springer ]
Эдуардо Хименес. Структурно-рекурсивные определения в теории типов . В ICALP'98: Материалы 25-го Международного коллоквиума по автоматам, языкам и программированию. Springer-Verlag, 1998. [ PDF ]
источник
Это, очевидно, проблема, специфичная для Coq, поскольку я считаю, что есть более хорошие способы обойти ее с некоторыми другими помощниками по проверке (я смотрю на Agda)
Сначала я думал, что
r
не был признан структурно меньшим, потому что структура только об индуктивном определении, которым в настоящее время занимаетсяFixpoint
: так что это неLTree
подтери, даже если этоlist
подтерма.Но если вы расширите обработку списка, то это сработает:
Или, поскольку вспомогательная функция уже существует в стандартной библиотеке:
Честно говоря, я не уверен, почему они приняты Coq, но я уверен, что они рады.
Существует также решение, которое работает чаще, и не только для списков: определение автономного индуктивного типа. В этом случае вы можете определить свою
size
функцию вручную. (с двумя точками фиксации)Обратите внимание, что если у вас есть проблемы с более сложными индуктивными определениями, вы можете использовать уменьшающий размер аргумент. Это возможно, но громоздко для этой проблемы (и я бы осмелился сказать для большинства проблем)
источник