Рекурсивные определения над индуктивным типом с вложенными компонентами

21

Рассмотрим индуктивный тип, который имеет некоторые рекурсивные вхождения во вложенном, но строго положительном месте. Например, деревья с конечным ветвлением с узлами, использующими общую структуру данных списка для хранения дочерних элементов.

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это индуктивный тип, соответствующий следующей грамматике.

LTree::=|list(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
Жиль "ТАК - перестань быть злым"
источник
Это по теме? Я не уверен; давайте обсудим это на Мете .
Жиль "ТАК - перестать быть злым"
Можете ли вы добавить эквивалентные определения функций в что-то менее Coqy и более математику? У меня проблемы с пониманием синтаксиса.
Рафаэль
1
@ Рафаэль, я пробовал, сейчас лучше? Честно говоря, этот вопрос довольно специфичен для Coq.
Жиль "ТАК ... перестать быть злым"

Ответы:

14

Что работает

Если вы вложите определение точки фиксации в списки внутри определения точки фиксации на деревьях, результат будет хорошо напечатан. Это общий принцип, когда у вас есть вложенная рекурсия в индуктивном типе, т.е. когда рекурсия проходит через конструктор типа list.

Fixpoint size (t : LTree) : nat :=
  let size_l := (fix size_l (l : list LTree) : nat :=
                  match l with
                    | nil => 0
                    | h::r => size h + size_l r
                  end) in
  match t with Node l =>
    1 + size_l l
  end.

Или, если вы предпочитаете писать это более кратко:

Fixpoint size (t : LTree) : nat :=
  match t with Node l =>
    1 + (fix size_l (l : list LTree) : nat :=
          match l with
            | nil => 0
            | h::r => size h + size_l r
          end) l
  end.

(Я понятия не имею, от кого я это услышал в первый раз; это, безусловно, было открыто независимо много раз.)

Предикат общей рекурсии

В более общем смысле вы можете определить «правильный» принцип индукции при включении LTreeвручную. Автоматически сгенерированный принцип индукции LTree_rectопускает гипотезу в списке, потому что генератор принципа индукции понимает только не вложенные строго положительные вхождения индуктивного типа.

LTree_rect = 
fun (P : LTree -> Type) (f : forall l : list LTree, P (Node l)) (l : LTree) =>
match l as l0 return (P l0) with
| Node x => f x
end
     : forall P : LTree -> Type,
       (forall l : list LTree, P (Node l)) -> forall l : LTree, P l

Давайте добавим гипотезу индукции в списки. Чтобы выполнить его в рекурсивном вызове, мы вызываем принцип индукции списка и передаем его принципу индукции дерева в меньшем дереве внутри списка.

Fixpoint LTree_rect_nest (P : LTree -> Type) (Q : list LTree -> Type)
                         (f : forall l, Q l -> P (Node l))
                         (g : Q nil) (h : forall t l, P t -> Q l -> Q (cons t l))
                         (t : LTree) :=
  match t as t0 return (P t0) with
    | Node l => f l (list_rect Q g (fun u r => h u r (LTree_rect_nest P Q f g h u)) l)
  end.

Почему

Ответ на вопрос заключается в точных правилах принятия рекурсивных функций. Эти правила выполняются тонко, поскольку существует тонкий баланс между разрешением сложных случаев (таких как этот, с вложенной рекурсией в типе данных) и несостоятельностью. Coq Справочное руководство вводит язык (исчисление индуктивных конструкций, что является доказательством язык Coq), в основном , с формально точными определениями, но если вы хотите точные правила относительно индукции и коиндукции вам нужно пойти в научно - исследовательских работ, на эту тему Эдуардо Хименес [1].

Начиная с руководства Coq, в нотации Fixправила у нас есть определение фиксированной точки где:Fixfi{f1:A1:=t1;f2:A2:=t2}

Γ1=(x:LTree)A1=natt1=case(x,LTree,λy.g1(f2y))Γ2=(l:listLTree)A2=natt2=case(l,listLTree,λhr.g2(f1h)(f2r))

Для того чтобы определение с фиксированной точкой было принято, «если встречается [в ], то… аргумент должен быть синтаксически распознан как структурно меньший, чем [аргумент, переданный в ]» (упрощение, потому что функции имеют единственный аргумент). Здесь мы должны проверить, чтот I е Ifjtifi

  • j = 2i=1 , : должен быть структурно меньше, чем в , хорошо.j=2ltsize
  • j = 1i=2 , : должен быть структурно меньше, чем в , выглядит хорошо, но не так!j=1hlsize_l
  • j = 2i=2 , : должен быть структурно меньше, чем в , хорошо.j=2rlsize_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 ]

Жиль "ТАК - перестань быть злым"
источник
7

Это, очевидно, проблема, специфичная для Coq, поскольку я считаю, что есть более хорошие способы обойти ее с некоторыми другими помощниками по проверке (я смотрю на Agda)

Сначала я думал, что rне был признан структурно меньшим, потому что структура только об индуктивном определении, которым в настоящее время занимается Fixpoint: так что это не LTreeподтери, даже если это listподтерма.

Но если вы расширите обработку списка, то это сработает:

Fixpoint size t :=
  match t with
  | Node l => S
     ((fix size_l l :=
     match l with
     | nil => 0
     | cons t l => size_l l + size t
     end) l)
 end.

Или, поскольку вспомогательная функция уже существует в стандартной библиотеке:

Require Import List.

Fixpoint size t :=
  match t with
  | Node l => S (fold_left (fun a t => a + size t) l 0)
  end.

Честно говоря, я не уверен, почему они приняты Coq, но я уверен, что они рады.

Существует также решение, которое работает чаще, и не только для списков: определение автономного индуктивного типа. В этом случае вы можете определить свою sizeфункцию вручную. (с двумя точками фиксации)

Inductive LTree : Set :=
  | Node : list_LTree -> LTree
with list_LTree : Set :=
  | LTree_nil : list_LTree
  | LTree_cons : LTree -> list_LTree -> list_LTree.

Обратите внимание, что если у вас есть проблемы с более сложными индуктивными определениями, вы можете использовать уменьшающий размер аргумент. Это возможно, но громоздко для этой проблемы (и я бы осмелился сказать для большинства проблем)

jmad
источник
Сегодня я до сих пор не понимаю, почему наивный подход не работает. В принципе, это должно быть следствием работы Эдуардо Хименеса, но я не вижу, где нарушается дедукция; это может быть ограничением двигателя Coq, а не базового исчисления.
Жиль "ТАК ... перестать быть злым"