Bagaimana Anda bisa membangun tabel memoisasi coinductive untuk fungsi rekursif di atas pohon biner?

The StreamMemo perpustakaan untuk Coq menggambarkan bagaimana memoize fungsi f : nat -> Amelalui nomor alami. Terutama saat f (S n) = g (f n), imemo_makeberbagi perhitungan panggilan rekursif.

Misalkan alih-alih bilangan alami, kami ingin memoize fungsi rekursif atas pohon biner:

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

Misalkan kita memiliki fungsi f : binTree -> Ayang bersifat rekursif secara struktural, artinya ada fungsi g : A -> A -> Asedemikian rupa f (Branch x y) = g (f x) (f y). Bagaimana kita membuat tabel memo serupa untuk fdalam Coq sehingga perhitungan rekursif dibagikan?

Di Haskell, tidak terlalu sulit untuk membuat tabel memo seperti itu (lihat MemoTrie misalnya) dan mengikat. Jelas tabel memo seperti itu produktif. Bagaimana kita bisa mengatur hal-hal untuk meyakinkan bahasa yang diketik secara dependen untuk menerima ikatan seperti itu produktif?

Meskipun saya telah menentukan masalah dalam Coq, saya akan senang dengan jawaban dalam Agda atau bahasa yang diketik dengan dependen lainnya.

Cukup mudah untuk mendapatkan pola rekursi untuk bekerja dengan tipe berukuran. Semoga pembagian ini dipertahankan melalui kompilasi! [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

Saya telah menciptakan "solusi" yang secara rekursif menghafal fungsi rekursif struktur pohon biner dalam Coq. Intisari saya ada di https://gist.github.com/roconnor/286d0f21af36c2e97e74338f10a4315b .

Ini beroperasi mirip dengan solusi Saizan , dengan stratifikasi pohon biner berdasarkan ukuran metrik, dalam kasus saya menghitung jumlah node internal pohon biner, dan menghasilkan aliran malas wadah semua solusi untuk ukuran tertentu. Berbagi terjadi karena pernyataan let di generator aliran yang memegang bagian awal dari aliran yang akan digunakan di bagian selanjutnya dari aliran.

Contoh menunjukkan bahwa untuk vm_compute, mengevaluasi pohon biner sempurna dengan 8 level setelah mengevaluasi pohon biner sempurna dengan 9 level jauh lebih cepat daripada hanya mengevaluasi pohon biner sempurna dengan 8 level.

Namun, saya ragu untuk menerima jawaban ini karena overhead dari solusi khusus ini buruk sehingga berkinerja jauh lebih buruk daripada memoisasi saya tanpa rekursi struktural untuk contoh input praktis saya. Secara alami, saya ingin solusi yang berkinerja lebih baik di bawah input yang masuk akal.

Saya punya beberapa komentar lebih lanjut di " [Coq-Club] Bagaimana Anda bisa membangun tabel memoisasi coinductive untuk fungsi rekursif atas pohon biner? ".