Проверка завершения на unionWith

Question

У меня проблема с проверкой завершения, очень похожая на описанную в этом вопросе, а также на отчет об ошибке Agda / запрос функции.

Проблема заключается в том, чтобы убедить компилятор в следующем unionWith завершается. Используя функцию комбинирования для дубликатов ключей, unionWith объединяет две карты, представленные в виде списков пар (ключ, значение), отсортированных по ключу. Параметр Key конечной карты является (не жесткой) нижней границей ключей, содержащихся в карте. (Одной из причин определения этого типа данных является предоставление семантической области, в которую я могу интерпретировать деревья AVL, чтобы доказать различные свойства о них.)

open import Function
open import Relation.Binary renaming (IsEquivalence to IsEq)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module FiniteMap
   {k v ℓ ℓ′}
   {Key : Set k}
   (Value : Set v)
   {_<_ : Rel Key ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
   {_≈_ : Rel Value ℓ′}
   (isEquivalence : IsEq _≈_)
   where

   open import Algebra.FunctionProperties
   open import Data.Product
   open IsStrictTotalOrder isStrictTotalOrder
   open import Level

   KV : Set (k ⊔ v)
   KV = Key × Value

   data FiniteMap (l : Key) : Set (k ⊔ v ⊔ ℓ) where
      [] : FiniteMap l
      _∷_ : (kv : KV) → let k = proj₁ kv in l < k → (m : FiniteMap k) → FiniteMap l

   unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
   unionWith _ [] [] = []
   unionWith _ [] m = m
   unionWith _ m [] = m
   unionWith _⊕_ (_∷_ (k , v) k<l m) (_∷_ (k′ , v′) k′<l m′) with compare k k′
   ... | tri< k<k′ _ _ = _∷_ (k , v) k<l (unionWith _⊕_ m (_∷_ (k′ , v′) k<k′ m′))
   ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = {!!} --_∷_ (k , v ⊕ v′) k<l (unionWith _⊕_ m m′)
   ... | tri> _ _ k′<k = _∷_ (k′ , v′) k′<l (unionWith _⊕_ (_∷_ (k , v) k′<k m) m′)

Я не смог обобщить решения, обсуждаемые в указанном вопросе, к моей настройке. Например, если я введу вспомогательную функцию unionWith'определяется взаимно рекурсивно с unionWithкоторый вызывается из последнего в k' < k дело:

   unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
   unionWith′ : ∀ {l} → Op₂ Value → (kv : KV) → let k = proj₁ kv in l < k → FiniteMap k → Op₁ (FiniteMap l)

   unionWith _ [] [] = []
   unionWith _ [] m = m
   unionWith _ m [] = m
   unionWith _⊕_ (_∷_ (k , v) k<l m) (_∷_ (k′ , v′) k′<l m′) with compare k k′
   ... | tri< k<k′ _ _ = _∷_ (k , v) k<l (unionWith _⊕_ m (_∷_ (k′ , v′) k<k′ m′))
   ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = {!!} --_∷_ (k , v ⊕ v′) k<l (unionWith _⊕_ m m′)
   ... | tri> _ _ k′<k = _∷_ (k′ , v′) k′<l (unionWith′ _⊕_ (k , v) k′<k m m′)

   unionWith′ _ (k , v) l<k m [] = _∷_ (k , v) l<k m
   unionWith′ _⊕_ (k , v) l<k m (_∷_ (k′ , v′) k′<l m′) with compare k k′
   ... | tri< k<k′ _ _ = {!!}
   ... | tri≈ _ k≡k′ _ = {!!}
   ... | tri> _ _ k′<k = _∷_ (k′ , v′) k′<l (unionWith′ _⊕_ (k , v) k′<k m m′)

затем, как только я завяжу рекурсивный узел, заменив первый отсутствующий регистр в unionWith' с необходимым вызовом unionWith, он не может завершить проверку.

Я также попытался ввести дополнительные with шаблоны, но это сложно из-за необходимости использовать результат compare в рекурсивных вызовах. (Если я использую вложенный with пункты, которые, кажется, не помогают проверке завершения.)

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

(Возможно, с этим может справиться новая проверка завершения в ветке разработки Agda, но я бы не стал устанавливать версию для разработки, если мне не нужно.)

Answer 1

Вот альтернатива, основанная на размерных типах, основанная на ответе на этот более поздний вопрос. Вы можете подобрать Data.Extended-key модуль отсюда, или вы можете настроить код ниже, чтобы он использовал Data.AVL.Extended-key вместо стандартной библиотеки вместо.

Преамбула:

{-# OPTIONS --sized-types #-}

open import Relation.Binary renaming (IsStrictTotalOrder to IsSTO)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- A list of (key, value) pairs, sorted by key in strictly descending order.
module Temp
   {  ℓ}
   {Key : Set }
   (Value : Key → Set )
   {_<_ : Rel Key ℓ}
   (isStrictTotalOrder′ : IsSTO _≡_ _<_)
   where

   open import Algebra.FunctionProperties
   open import Data.Extended-key isStrictTotalOrder′
   open import Function
   open import Level
   open import Size
   open IsStrictTotalOrder isStrictTotalOrder

Теперь FiniteMap определение, дополненное индексами размера.

   data FiniteMap (l u : Key⁺) : {ι : Size} → Set ( ⊔  ⊔ ℓ) where
      [] : {ι : _} → .(l <⁺ u) → FiniteMap l u {↑ ι}
      _↦_∷[_]_ : {ι : _} (k : Key) (v : Value k) → .(l <⁺ [ k ]) → 
                 (m : FiniteMap [ k ] u {ι}) → FiniteMap l u {↑ ι}

   infixr 3 _↦_∷[_]_

Тогда мы можем написать версию unionWith что проверки завершения, не обходя стороной вспомогательные функции.

   unionWith : ∀ {l u} → (∀ {k} → Op₂ (Value k)) →
               {ι : Size} → FiniteMap l u {ι} → {ι′ : Size} → 
               FiniteMap l u {ι′} → FiniteMap l u
   unionWith _ ([] l<⁺u) ([] _) = [] l<⁺u
   unionWith _ ([] _) m = promote m
   unionWith _ m ([] _ )= promote m
   unionWith ∙ (k ↦ v ∷[ _ ] m) (k′ ↦ v′ ∷[ _ ] m′) with compare [ k ] [ k′ ]
   ... | (tri< k<⁺k′ _ _) = k ↦ v ∷[ _ ] unionWith ∙ m (k′ ↦ v′ ∷[ _ ] m′)
   unionWith ∙ (k ↦ v ∷[ l<⁺k ] m) (.k ↦ v′ ∷[ _ ] m′) | (tri≈ _ P.refl _) =
      k ↦ (v ⟨ ∙ ⟩ v′) ∷[ l<⁺k ] unionWith ∙ m m′
   ... | (tri> _ _ k′<⁺k) = k′ ↦ v′ ∷[ _ ] unionWith ∙ (k ↦ v ∷[ _ ] m) m′

Нам почти наверняка понадобится версия, в которой все индексы равны ∞, но это незначительное неудобство.

   unionWith′ : ∀ {l u} → (∀ {k} → Op₂ (Value k)) → Op₂ (FiniteMap l u)
   unionWith′ ∙ x y = unionWith ∙ x y

Доказательство собственности unionWith использование рекурсивной функции обычно требует, чтобы индексы использовались аналогичным образом.

Я еще не убежден, что не буду сталкиваться с тонкостями при более широком использовании индексов размеров, но пока я впечатлен тем, насколько они ненавязчивы. Это, конечно, меньше, чем требуется для обычных взломов Agda.

Answer 2

Похоже, что первое решение, предложенное для более раннего вопроса слияния, действительно работает здесь, но только в версии 2.3.3+ Agda. Вот полная версия, с немного более приятным синтаксисом для ∷.

data FiniteMap (l : Key) : Set (k ⊔ v ⊔ ℓ) where
   [] : FiniteMap l
   _∷[_]_ : (kv : KV) → let k = proj₁ kv in l < k → (m : FiniteMap k) → FiniteMap l

-- Split into two definitions to help the termination checker.
unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
unionWith′ : ∀ {l} → Op₂ Value → (kv : KV) → let k = proj₁ kv in l < k → FiniteMap k → Op₁ (FiniteMap l)

unionWith _ [] [] = []
unionWith _ [] m = m
unionWith _ m [] = m
unionWith _⊕_ ((k , v) ∷[ k<l ] m) ((k′ , v′) ∷[ k′<l ] m′) with compare k k′
... | tri< k<k′ _ _ = (k , v) ∷[ k<l ] (unionWith _⊕_ m ((k′ , v′) ∷[ k<k′ ] m′))
... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = (k , v ⊕ v′) ∷[ k<l ] (unionWith _⊕_ m m′)
... | tri> _ _ k′<k = (k′ , v′) ∷[ k′<l ] (unionWith′ _⊕_ (k , v) k′<k m m′)

unionWith′ _ (k , v) l<k m [] = (k , v) ∷[ l<k ] m
unionWith′ _⊕_ (k , v) l<k m ((k′ , v′) ∷[ k′<l ] m′) with compare k k′
... | tri< k<k′ _ _ = (k , v) ∷[ l<k ] (unionWith _⊕_ m ((k′ , v′) ∷[ k<k′ ] m′))
... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = (k , v ⊕ v′) ∷[ l<k ] (unionWith _⊕_ m m′)
... | tri> _ _ k′<k = (k′ , v′) ∷[ k′<l ] (unionWith′ _⊕_ (k , v) k′<k m m′)