Завершение проверки функции через три

Question

Мне трудно убедить Агду завершить проверку функции fmap ниже и аналогичные функции, определенные рекурсивно по структуре 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 возвращается в строго меньший аргумент в каждом случае; конечно, случай продукта хорош, если я уберу рекурсивные типы. С другой стороны, определение хорошо обрабатывает рекурсивные типы, если я удаляю продукты.

Какой самый простой способ продолжить здесь? Трюк со встроенным / предохранителем не выглядит особенно применимым, но, возможно, это так. Или я должен искать другой способ справиться с заменой в определении Trie?

Answer 1

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

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 видеть, что это не делает ничего прикольного. Поэтому мы должны применить трюк inline/fuse, чтобы пройти проверку завершения:

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 σ)

---

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

В простейшей форме размерный тип ведет себя как тип, проиндексированный натуральным числом. Этот индекс определяет верхнюю границу структурного размера. Вы можете думать об этом как о верхней границе для высоты дерева (учитывая, что тип данных является F-ветвящимся деревом для некоторого функтора F). Размерная версия 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 σ)