Wie können Sie eine koinduktive Memoisierungstabelle für rekursive Funktionen über Binärbäumen erstellen?

Die StreamMemo- Bibliothek für Coq zeigt, wie eine Funktion f : nat -> Aüber die natürlichen Zahlen gespeichert wird . Insbesondere wenn f (S n) = g (f n)die imemo_makeFreigabe die Berechnung von rekursiven Aufrufen teilt.

Angenommen, wir möchten anstelle natürlicher Zahlen rekursive Funktionen über Binärbäume speichern:

Inductive binTree : Set := | Leaf : binTree | Branch : binTree -> binTree -> binTree.

Angenommen, wir haben eine Funktion f : binTree -> A, die strukturell rekursiv ist, was bedeutet, dass es eine g : A -> A -> Asolche Funktion gibt f (Branch x y) = g (f x) (f y). Wie erstellen wir eine ähnliche Memotabelle für fin Coq, sodass die rekursiven Berechnungen gemeinsam genutzt werden?

In Haskell ist es nicht allzu schwierig, eine solche Memotabelle (siehe beispielsweise MemoTrie ) zu erstellen und den Knoten zu knüpfen. Offensichtlich sind solche Memotabellen produktiv. Wie können wir Dinge arrangieren, um eine abhängig getippte Sprache davon zu überzeugen, dass eine solche Knotenbindung produktiv ist?

Obwohl ich das Problem in Coq angegeben habe, würde ich mich über eine Antwort in Agda oder einer anderen abhängig getippten Sprache freuen.

Es ist einfach genug, das Rekursionsmuster für Typen mit Größe zu verwenden. Hoffentlich bleibt das Teilen durch Zusammenstellung erhalten! [1]

module _ where

open import Size
open import Data.Nat

data BT (i : Size) : Set where
  Leaf : BT i
  Branch : ∀ {j : Size< i} → BT j → BT j → BT i

record Memo (A : Set) (i : Size) : Set where
  coinductive
  field
    leaf : A
    branch : ∀ {j : Size< i} → Memo (Memo A j) j

open Memo

trie : ∀ {i} {A} → (BT i → A) → Memo A i
trie f .leaf = f Leaf
trie f .branch = trie (\ l → trie \ r → f (Branch l r))

untrie : ∀ {i A} → Memo A i → BT i → A
untrie m Leaf         = m .leaf
untrie m (Branch l r) = untrie (untrie (m .branch) l) r

memo : ∀ {i A} → (BT i → A) → BT i → A
memo f = untrie (trie f)

memoFix : ∀ {A : Set} → A → (A → A → A) → ∀ {i} → BT i → A
memoFix {A} lf br = go
 where
  go h : ∀ {i} → BT i → A
  go = memo h
  h Leaf = lf
  h (Branch l r) = br (go l) (go r)

[1] https://github.com/agda/agda/issues/2918

Ich habe eine "Lösung" erstellt, die rekursiv strukturell rekursive Funktionen von Binärbäumen in Coq speichert. Mein Kern ist unter https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b .

Es funktioniert ähnlich wie die Lösung von Saizan , indem Binärbäume basierend auf einer Größenmetrik geschichtet werden , in meinem Fall die Anzahl der internen Knoten von Binärbäumen gezählt wird und ein verzögerter Strom von Containern aller Lösungen für eine bestimmte Größe erzeugt wird. Die Freigabe erfolgt aufgrund einer let-Anweisung im Stream-Generator, die den ersten Teil des Streams enthält, der in späteren Teilen des Streams verwendet werden soll.

Beispiele zeigen, dass die vm_computeBewertung eines perfekten Binärbaums mit 8 Ebenen nach der Bewertung eines perfekten Binärbaums mit 9 Ebenen viel schneller ist als die Bewertung eines perfekten Binärbaums mit 8 Ebenen.

Ich zögere jedoch, diese Antwort zu akzeptieren, da der Aufwand für diese spezielle Lösung schlecht ist, da sie viel schlechter abschneidet als meine Memoisierung ohne strukturelle Rekursion für meine Beispiele praktischer Eingaben. Natürlich möchte ich eine Lösung, die bei angemessenen Eingaben eine bessere Leistung erbringt.

Ich habe einige weitere Kommentare unter " [Coq-Club] Wie kann eine koinduktive Memoisierungstabelle für rekursive Funktionen über Binärbäumen erstellt werden? ".