Прекращение проверки функции по trie

Question

У меня возникли трудности с убеждением Agda в завершении проверки функции fmap ниже и аналогичных функций, определенных рекурсивно над структурой Trie. A Trie - это номер trie, домен которого Type, тип уровня объекта, сформированный из единицы, продуктов и неподвижных точек (я пропустил сопроводительные материалы, чтобы сохранить код минимальным). Проблема, похоже, связана с заменой типа уровня, которую я использую в определении Trie. (Выражение const (μₜ τ) * τ средством применить замену const (μₜ τ) к типу τ.)

module Temp where 

    open import Data.Unit 
    open import Category.Functor 
    open import Function 
    open import Level 
    open import Relation.Binary 

    -- A context is just a snoc-list. 
    data Cxt {} (A : Set) : Set where 
     ε : Cxt A 
     _∷ᵣ_ : Cxt A → A → Cxt A 

    -- Context membership. 
    data _∈_ {} {A : Set } (a : A) : Cxt A → Set where 
     here : ∀ {Δ} → a ∈ Δ ∷ᵣ a 
     there : ∀ {Δ a′} → a ∈ Δ → a ∈ Δ ∷ᵣ a′ 
    infix 3 _∈_ 

    -- Well-formed types, using de Bruijn indices. 
    data _⊦ (Δ : Cxt ⊤) : Set where 
     nat : Δ ⊦ 
     : Δ ⊦ 
     var : _ ∈ Δ → Δ ⊦ 
     _+_ _⨰_ : Δ ⊦ → Δ ⊦ → Δ ⊦ 
     μ : Δ ∷ᵣ _ ⊦ → Δ ⊦ 
    infix 3 _⊦ 

    -- A closed type. 
    Type : Set 
    Type = ε ⊦ 

    -- Type-level substitutions and renamings. 
    Sub Ren : Rel (Cxt ⊤) zero 
    Sub Δ Δ′ = _ ∈ Δ → Δ′ ⊦ 
    Ren Δ Δ′ = ∀ {x} → x ∈ Δ → x ∈ Δ′ 

    -- Renaming extension. 
    extendᵣ : ∀ {Δ Δ′} → Ren Δ Δ′ → Ren (Δ ∷ᵣ _) (Δ′ ∷ᵣ _) 
    extendᵣ ρ here = here 
    extendᵣ ρ (there x) = there (ρ x) 

    -- Lift a type renaming to a type. 
    _*ᵣ_ : ∀ {Δ Δ′} → Ren Δ Δ′ → Δ ⊦ → Δ′ ⊦ 
    _ *ᵣ nat = nat 
    _ *ᵣ = 
    ρ *ᵣ (var x) = var (ρ x) 
    ρ *ᵣ (τ₁ + τ₂) = (ρ *ᵣ τ₁) + (ρ *ᵣ τ₂) 
    ρ *ᵣ (τ₁ ⨰ τ₂) = (ρ *ᵣ τ₁) ⨰ (ρ *ᵣ τ₂) 
    ρ *ᵣ (μ τ) = μ (extendᵣ ρ *ᵣ τ) 

    -- Substitution extension. 
    extend : ∀ {Δ Δ′} → Sub Δ Δ′ → Sub (Δ ∷ᵣ _) (Δ′ ∷ᵣ _) 
    extend θ here = var here 
    extend θ (there x) = there *ᵣ (θ x) 

    -- Lift a type substitution to a type. 
    _*_ : ∀ {Δ Δ′} → Sub Δ Δ′ → Δ ⊦ → Δ′ ⊦ 
    θ * nat = nat 
    θ * = 
    θ * var x = θ x 
    θ * (τ₁ + τ₂) = (θ * τ₁) + (θ * τ₂) 
    θ * (τ₁ ⨰ τ₂) = (θ * τ₁) ⨰ (θ * τ₂) 
    θ * μ τ = μ (extend θ * τ) 

    data Trie {} (A : Set) : Type → Set where 
     〈〉 : A → ▷ A 
     〔_,_〕 : ∀ {τ₁ τ₂} → τ₁ ▷ A → τ₂ ▷ A → τ₁ + τ₂ ▷ A 
     ↑_ : ∀ {τ₁ τ₂} → τ₁ ▷ τ₂ ▷ A → τ₁ ⨰ τ₂ ▷ A 
     roll : ∀ {τ} → (const (μ τ) * τ) ▷ A → μ τ ▷ A 

    infixr 5 Trie 
    syntax Trie A τ = τ ▷ A 

    {-# NO_TERMINATION_CHECK #-} 
    fmap : ∀ {a} {A B : Set a} {τ} → (A → B) → τ ▷ A → τ ▷ B 
    fmap f (〈〉 x) = 〈〉 (f x) 
    fmap f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕 
    fmap f (↑ σ) = ↑ (fmap (fmap f) σ) 
    fmap f (roll σ) = roll (fmap f σ) 

Казалось бы, что fmap рекурсивно в строго меньшего аргумента в каждом случае; конечно, случай продукта прекрасен, если я удаляю рекурсивные типы. С другой стороны, определение обрабатывает рекурсивные типы, если я удаляю продукты.

Что является самым простым способом здесь? inline/fuse trick не выглядит особенно применимым, но, возможно, это так. Или я должен искать другой способ справиться с заменой в определении Trie?

Answer 1

Ввод встроенного/предохранителя может быть применен (возможно) удивительным способом. Этот прием подходит для задач такого рода:

data Trie (A : Set) : Set where 
    nil :      Trie A 
    node : A → List (Trie A) → Trie A 

map-trie : {A B : Set} → (A → B) → Trie A → Trie B 
map-trie f nil = nil 
map-trie f (node x xs) = node (f x) (map (map-trie f) xs) 

Эта функция структурно рекурсивными, но в скрытой форме. map просто применяет map-trie f к элементам xs, поэтому map-trie применяется к меньшим (суб) попыткам. Но Агда не рассматривает определение map, чтобы убедиться, что он не делает ничего напуганного. Таким образом, мы должны применить встроенный/предохранитель трюк, чтобы получить его мимо окончания проверки:

map-trie : {A B : Set} → (A → B) → Trie A → Trie B 
map-trie   f nil = nil 
map-trie {A} {B} f (node x xs) = node (f x) (map′ xs) 
    where 
    map′ : List (Trie A) → List (Trie B) 
    map′ [] = [] 
    map′ (x ∷ xs) = map-trie f x ∷ map′ xs 

---

Ваши fmap функция разделяет те же структуры, то сопоставить поднятую функцию своего рода. Но что делать? Если мы следуем приведенному выше примеру, мы должны указать сам fmap. Это выглядит и чувствует себя немного странно, но на самом деле, это работает:

fmap fmap′ : ∀ {a} {A B : Set a} {τ} → (A → B) → τ ▷ A → τ ▷ B 

fmap f (〈〉 x) = 〈〉 (f x) 
fmap f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕 
fmap f (↑ σ) = ↑ (fmap (fmap′ f) σ) 
fmap f (roll σ) = roll (fmap f σ) 

fmap′ f (〈〉 x) = 〈〉 (f x) 
fmap′ f 〔 σ₁ , σ₂ 〕 = 〔 fmap′ f σ₁ , fmap′ f σ₂ 〕 
fmap′ f (↑ σ) = ↑ (fmap′ (fmap f) σ) 
fmap′ f (roll σ) = roll (fmap′ f σ) 

---

Там другая техника, которую вы можете применить: это называется типы размеров. Вместо того, чтобы полагаться на компилятор, чтобы выяснить, когда somethig является или не является структурно рекурсивным, вы указываете его напрямую. Однако вам необходимо индексировать свои типы данных с помощью типа Size, поэтому этот подход довольно навязчив и не может применяться к уже существующим типам, но я думаю, что это стоит упомянуть.

В простейшей форме размерный тип ведет себя как тип, индексированный натуральным числом. Этот индекс указывает верхнюю границу структурного размера. Вы можете рассматривать это как верхнюю границу высоты дерева (учитывая, что тип данных является F-ветвящимся деревом для некоторого функтора F). Sized версия List выглядит почти как Vec, например:

data SizedList (A : Set) : ℕ → Set where 
    [] : ∀ {n} → SizedList A n 
    _∷_ : ∀ {n} → A → SizedList A n → SizedList A (suc n) 

Но размера типов добавить несколько особенностей, которые делают их более удобными в использовании. У вас есть постоянный номер ∞ для случая, когда вам не нужен размер. suc называется ↑, и Agda реализует несколько правил, таких как ↑ ∞ = ∞.

Давайте переписать пример Trie, чтобы использовать типоразмеры. Нам нужна прагма в верхней части файла и один импорт:

{-# OPTIONS --sized-types #-} 
open import Size 

И вот модифицированный тип данных:

data Trie (A : Set) : {i : Size} → Set where 
    nil : ∀ {i}       → Trie A {↑ i} 
    node : ∀ {i} → A → List (Trie A {i}) → Trie A {↑ i} 

Если оставить функцию map-trie как есть, прекращение проверка продолжается жаловаться. Это потому, что, когда вы не укажете какой-либо размер, Agda заполнит бесконечность (т. Е. Значение не-уход), и мы вернемся в начале.

Однако мы можем отметить map-trie как размер сохраняющих:

map-trie : ∀ {i A B} → (A → B) → Trie A {i} → Trie B {i} 
map-trie f nil   = nil 
map-trie f (node x xs) = node (f x) (map (map-trie f) xs) 

Итак, если вы дать ему Trie ограниченную i, это даст вам еще Trie ограниченную i, а также. Таким образом, map-trie никогда не сможет сделать Trie больше, только одинаково большим или меньшим. Этого достаточно для проверки завершения проверки, что map (map-trie f) xs в порядке.

---

Этот метод также может быть применен к вашим Trie:

open import Size 
    renaming (↑_ to ^_) 

data Trie {} (A : Set) : {i : Size} → Type → Set where 
    〈〉 : ∀ {i} → A → 
    Trie A {^ i} 
    〔_,_〕 : ∀ {i τ₁ τ₂} → Trie A {i} τ₁ → Trie A {i} τ₂ → 
    Trie A {^ i} (τ₁ + τ₂) 
    ↑_ : ∀ {i τ₁ τ₂} → Trie (Trie A {i} τ₂) {i} τ₁ → 
    Trie A {^ i} (τ₁ ⨰ τ₂) 
    roll : ∀ {i τ} → Trie A {i} (const (μ τ) * τ) → 
    Trie A {^ i} (μ τ) 

infixr 5 Trie 
syntax Trie A τ = τ ▷ A 

fmap : ∀ {i } {A B : Set } {τ} → (A → B) → Trie A {i} τ → Trie B {i} τ 
fmap f (〈〉 x) = 〈〉 (f x) 
fmap f 〔 σ₁ , σ₂ 〕 = 〔 fmap f σ₁ , fmap f σ₂ 〕 
fmap f (↑ σ) = ↑ fmap (fmap f) σ 
fmap f (roll σ) = roll (fmap f σ)