Проверка окончания соединения с

Question

У меня возникла проблема с проверкой завершения, очень похожей на ту, что описана в this question, а также на этот Agda bug report/feature request.

Проблема заключается в том, чтобы убедить компилятор, что следующие 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′) 

я не смог обобщить решения, описанные в referenced question в мою настройку. Например, если я ввести вспомогательную функцию 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 шаблоны или вспомогательные функции для компиляции? Похоже, ситуация достаточно проста, поэтому я надеюсь, что это всего лишь случай, когда вы поймете, какой трюк.

(Может быть, новое прекращение проверки в отрасли разработки Агда может справиться с этим, но я хотел бы избежать установки разрабатываемой версии, если я не должен.)

Answer 1

Вот альтернатива на основе типов размеров, на основе the answer to this later question. Вы можете получить модуль 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, что прекращение проверок, без cheesing вокруг с дополнительными функциями.

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

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

Answer 2

кажется первое решение, предложенное для earlier list-merge question действительно работает здесь, но только под версией Agda 2.3.3+. Вот полная версия, с немного более сильным синтаксисом для ∷.

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