ソートされたリストのデータ型があり、証明に関係のないソートの目撃者があるとします。Agda の実験的なサイズの型機能を使用して、Agda の終了チェッカーを通過するデータ型の再帰関数を取得できるようにします。
{-# OPTIONS --sized-types #-}
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P
module ListMerge
{ ℓ}
(A : Set )
{_<_ : Rel A ℓ}
(isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where
open import Level
open import Size
data SortedList (l u : A) : {ι : _} → Set ( ⊔ ℓ) where
[] : {ι : _} → .(l < u) → SortedList l u {↑ ι}
_∷[_]_ : {ι : _} (x : A) → .(l < x) → (xs : SortedList x u {ι}) →
SortedList l u {↑ ι}
さて、そのようなデータ構造に対して定義したい古典的な関数は ですmerge。これは 2 つのソートされたリストを取り、入力リストの要素を正確に含むソートされたリストを出力します。
open IsStrictTotalOrder isStrictTotalOrder
merge : ∀ {l u} → SortedList l u → SortedList l u → SortedList l u
merge xs ([] _) = xs
merge ([] _) ys = ys
merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
... | tri< _ _ _ = x ∷[ l<x ] (merge xs (y ∷[ _ ] ys))
merge (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ =
x ∷[ l<x ] (merge xs ys)
... | tri> _ _ _ = y ∷[ l<y ] (merge (x ∷[ _ ] xs) ys)
この関数は無害に思えますが、Agda にそれが合計であることを納得させるのは難しい場合があります。実際、明示的なサイズ インデックスがないと、関数は終了チェックに失敗します。1 つのオプションは、関数を 2 つの相互に再帰的な定義に分割することです。これは機能しますが、定義と関連する証明の両方にある程度の冗長性が追加されます。
mergeしかし同様に、サイズ インデックスを明示的に指定して、Agda が受け入れる署名を持つことができるかどうかもわかりません。これらのスライドmergesortでは、明確に議論しています。そこに与えられた署名は、以下が機能することを示唆しています:
merge′ : ∀ {l u} → {ι : _} → SortedList l u {ι} →
{ι′ : _} → SortedList l u {ι′} → SortedList l u
merge′ xs ([] _) = xs
merge′ ([] _) ys = ys
merge′ (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
... | tri< _ _ _ = x ∷[ l<x ] (merge′ xs (y ∷[ _ ] ys))
merge′ (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ =
x ∷[ l<x ] (merge′ xs ys)
... | tri> _ _ _ = y ∷[ l<y ] (merge' (x ∷[ _ ] xs) ys)
ここで行っているのは、入力が任意の (そして異なる) サイズを持つことを許可し、出力のサイズが ∞ であることを指定することです。
残念ながら、この署名では、Agdaは、定義の最初の節の.ι != ∞ of type Size本文を確認すると、 と不満を漏らしています。xsサイズの型をよく理解しているとは言えませんが、どのサイズの ι も ∞ に統一されるという印象を受けました。おそらく、これらのスライドが作成されてから、サイズ指定された型のセマンティクスが変更されたのでしょう。
では、私のシナリオは、意図されたサイズの型のユースケースですか? もしそうなら、どのように使用すればよいですか？ここでサイズ化された型が適切でない場合、以下が行うmergeことを考えると、上記の最初のバージョンが終了チェックを行わないのはなぜですか:
open import Data.Nat
open import Data.List
open import Relation.Nullary
merge : List ℕ → List ℕ → List ℕ
merge (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | _ = y ∷ merge (x ∷ xs) ys
merge xs ys = xs ++ ys