1

我在终止检查时遇到问题，与此问题中描述的问题以及此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′&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

似乎为较早的列表合并问题提出的第一个解决方案确实在这里有效，但仅在 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′&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′ _ _ = (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′&lt;k = (k′ , v′) ∷[ k′&lt;l ] (unionWith′ _⊕_ (k , v) k′&lt;k m m′)
于 2014-01-19T14:58:29.473 回答
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 回答