1

この質問とこのAgda バグ レポート/機能リクエストで説明されているものと非常によく似た、終了チェックに問題があります。

unionWith問題は、以下が終了することをコンパイラーに納得させることです。重複キーの結合関数を使用して、unionWithキーでソートされた (キー、値) ペアのリストとして表される 2 つのマップをマージします。有限マップの Key パラメーターは、マップに含まれるキーの (厳密ではない) 下限です。(このデータ型を定義する理由の 1 つは、AVL ツリーに関するさまざまなプロパティを証明するために 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′&lt;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′&lt;k = _∷_ (k′ , v′) k′&lt;l (unionWith _⊕_ (_∷_ (k , v) k′&lt;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′&lt;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′&lt;k = _∷_ (k′ , v′) k′&lt;l (unionWith′ _⊕_ (k , v) k′&lt;k m m′)

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

unionWith'次に、最初に欠落しているケースを の必要な呼び出しに置き換えて再帰的な結び目を結ぶとすぐに、unionWith終了チェックに失敗します。

追加のパターンも導入しようとしましたが、再帰呼び出しでwithの結果を使用する必要があるため複雑です。（終了チェッカーに役立たないように見えるcompareネストされた句を使用する場合。）with

withこのコンパイルを取得するためにパターンまたは補助関数を使用する方法はありますか? それは簡単な状況のように思えるので、正しいトリックを知っているだけのケースであることを願っています.

(Agda 開発ブランチの新しい終了チェッカーで対処できるかもしれませんが、必要がない限り、開発バージョンのインストールは避けたいと思います。)

4

2 に答える 2

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′&lt;⁺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 終了ハックで必要とされる定型句よりも確かに少ないものです。

于 2014-02-05T22:57:34.170 に答える