Definicje rekurencyjne nad typem indukcyjnym z zagnieżdżonymi komponentami

21

Rozważ typ indukcyjny, który ma pewne rekurencyjne zdarzenia w zagnieżdżonej, ale ściśle dodatniej lokalizacji. Na przykład drzewa ze skończonymi rozgałęzieniami z węzłami używającymi ogólnej struktury danych listy do przechowywania elementów potomnych.

Inductive LTree : Set := Node : list LTree -> LTree.

Naiwny sposób definiowania funkcji rekurencyjnej nad tymi drzewami przez rekurencję nad drzewami i listami drzew nie działa. Oto przykład z sizefunkcją obliczającą liczbę węzłów.

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.

Ta definicja jest źle sformułowana (fragment komunikatu o błędzie):

Error:
Recursive definition of size_l is ill-formed.
Recursive call to size has principal argument equal to
"h" instead of "r".

Dlaczego definicja jest źle sformułowana, mimo że rjest to oczywiste pojęcie l? Czy istnieje sposób na zdefiniowanie funkcji rekurencyjnych w takiej strukturze danych?

Jeśli nie znasz biegle składni Coq: LTreejest typem indukcyjnym odpowiadającym następującej gramatyce.

\begin{aligned} L T r e e ::= \\ | & l i s t (L T r e e) \end{aligned}

$\begin{align} \mathtt{LTree} ::= & \\ \vert & \mathtt{list}(\mathtt{LTree}) \\ \end{align}$

Próbujemy zdefiniować sizefunkcję przez indukcję nad drzewami i listami. W OCaml byłoby to:

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

logic coq type-theory recursion proof-assistants Gilles „SO- przestań być zły”
źródło

Czy to na temat? Nie jestem pewny; porozmawiajmy o tym na Meta .

Gilles 'SO - przestań być zły'

Czy możesz dodać równoważne definicje funkcji w czymś mniej Coqy i więcej math? Mam problem ze zrozumieniem składni.

Raphael

1

@Raphael Próbowałem, czy teraz jest lepiej? Szczerze mówiąc, to pytanie jest dość specyficzne dla Coq.

Gilles „SO- przestań być zły”

14

Co działa

Jeśli zagnieździsz definicję punktu stałego na listach w definicji punktu stałego na drzewach, wynik jest dobrze wpisany. Jest to ogólna zasada, gdy zagnieżdżasz rekurencję w typie indukcyjnym, tj. Gdy rekurencja przechodzi przez konstruktor podobny 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.

Lub jeśli wolisz napisać to bardziej zwięźle:

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.

(Nie mam pojęcia, od kogo go usłyszałem; z pewnością wiele razy odkryto to niezależnie).

Ogólny predykat rekurencyjny

Mówiąc bardziej ogólnie, można LTreeręcznie zdefiniować „właściwą” zasadę indukcji . Automatycznie generowana zasada indukcji LTree_rectpomija hipotezę z listy, ponieważ generator zasad indukcji rozumie tylko nie zagnieżdżone ściśle pozytywne zdarzenia typu indukcyjnego.

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

Dodajmy hipotezę indukcyjną do list. Aby spełnić go w wywołaniu rekurencyjnym, wywołujemy zasadę indukcji listy i przekazujemy ją jako zasadę indukcji drzewa na mniejszym drzewie w liście.

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.

Dlaczego

Odpowiedź na pytanie dlaczego leży w precyzyjnych zasadach akceptacji funkcji rekurencyjnych. Reguły te są bardzo subtelne, ponieważ istnieje delikatna równowaga między dopuszczaniem złożonych przypadków (takich jak ten z zagnieżdżoną rekurencją w typie danych) a nieuzasadnieniem. Podręcznik referencyjny Coq wprowadza język (rachunek konstrukcji indukcyjnych, który jest językiem sprawdzającym Coq), głównie z formalnie precyzyjnymi definicjami, ale jeśli chcesz dokładnych zasad dotyczących indukcji i koindukcji, musisz przejść do artykułów naukowych, na ten temat Eduardo Giméneza [1].

Fix $\mathsf{Fix} f_i \, \{ f_1 : A_1 := t_1 \; ; \;\; f_2 : A_2 := t_2 \}$

\begin{aligned} Γ_{1} & = (x : L T r e e) & A_{1} & = n a t & t_{1} & = c a s e (x, L T r e e, λ y . g_{1} (f_{2} y)) \\ Γ_{2} & = (l : l i s t L T r e e) & A_{2} & = n a t & t_{2} & = c a s e (l, l i s t L T r e e, λ h r . g_{2} (f_{1} h) (f_{2} r)) \end{aligned}

$\begin{align*} \Gamma_1 &= (x : \mathtt{LTree}) & A_1 &= \mathrm{nat} & t_1 &= \mathsf{case}(x, \mathtt{LTree}, \lambda y. g_1 (f_2 y)) \\ \Gamma_2 &= (l : \mathtt{list}\;\mathtt{LTree}) & A_2 &= \mathrm{nat} & t_2 &= \mathsf{case}(l, \mathtt{list \: LTree}, \lambda h \: r. g_2 (f_1 h) (f_2 r)) \\ \end{align*}$

$f_j$ $t_i$ $f_i$

$i=1$ $j=2$ ltsize
$i=2$ $j=1$ hlsize_l
$i=2$ $j=2$ rlsize_l

Powód, dla którego hnie jest strukturalnie mniejszy niż lwedług interpretera Coq, nie jest dla mnie jasny. O ile rozumiem z dyskusji na liście klubów Coq [1] [2], jest to ograniczenie tłumacza, które w zasadzie można znieść, ale bardzo ostrożnie, aby uniknąć wprowadzenia niespójności.

Bibliografia

Cocorico, niekończąca się wiki Coq: Mutual Induction

Lista mailingowa Coq-Club:

[1] Wątek „Teoria meta: indukcja nad terminami za pomocą zmiennych abstrakcyjnych”; pierwsza wiadomość Robberta Krebbersa w dniu 21.10.2009; wyjaśnienie Adama Chlipali ; kontrprzykład Brunona Barrasa ; odpowiedź Hugo Herbelin .
[2] Wątek „Sprawdzanie zakończenia z zagnieżdżoną rekurencją”; pierwsza wiadomość Gert Smolka; odpowiedź Hugo Herbelin.

Zespół programistów Coq. Coq Proof Assistant: Podręcznik referencyjny . Wersja 8.3 (2010). [ web ] ch. 4 .

Eduardo Giménez. Kodyfikacja strzeżonych definicji za pomocą schematów rekurencyjnych . W Types'94: Typy dla dowodów i programów , LNCS 996. Springer-Verlag, 1994. doi: 10.1007 / 3-540-60579-7_3 [ Springer ]

Eduardo Giménez. Strukturalne definicje rekurencyjne w teorii typów . W ICALP'98: Materiały z 25. Międzynarodowego Kolokwium na temat automatów, języków i programowania. Springer-Verlag, 1998. [ PDF ]

Gilles „SO- przestań być zły”
źródło

7

Jest to oczywiście problem specyficzny dla Coq, ponieważ uważam, że są lepsze sposoby na obejście tego z innymi asystentami dowodowymi (patrzę na Agdę)

Na początku myślałem, że rnie został rozpoznany jako strukturalnie mniejszy, ponieważ struktura dotyczy tylko definicji indukcyjnej, którą obecnie obsługuje Fixpoint: więc nie jest to LTreesubterm, nawet jeśli jest listsubtermem.

Ale jeśli rozszerzysz przetwarzanie listy, to zadziała:

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.

Lub ponieważ funkcja pomocnicza już istnieje w standardowej bibliotece:

Require Import List.

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

Szczerze mówiąc, nie jestem pewien, dlaczego są akceptowane przez Coq, ale jestem pewien, że tak.

Istnieje również rozwiązanie, które działa częściej i nie tylko w przypadku list: definiowanie niezależnego typu indukcyjnego. W takim przypadku możesz sizeręcznie zdefiniować swoją funkcję. (z dwoma punktami stałymi)

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

Zauważ, że jeśli masz problemy z bardziej złożonymi definicjami indukcyjnymi, możesz użyć argumentu zmniejszającego rozmiar. Jest to możliwe, ale kłopotliwe dla tego problemu (i odważyłbym się powiedzieć w przypadku większości problemów)

jmad
źródło

Nadal nie rozumiem dzisiaj, dlaczego naiwne podejście nie działa. Zasadniczo powinno to być konsekwencją pracy Eduardo Giméneza, ale nie wiem, gdzie kończy się dedukcja; może to być ograniczenie silnika Coq, a nie rachunek różniczkowy.