크기가 지정된 정렬 된 목록의 병합

Question

정렬되지 않은 정렬 증인과 함께 정렬 된 데이터 형식이 있다고 가정합니다. 우리는 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이다.

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가 전체라는 것을 납득시키기가 까다로울 수 있다는 점을 제외하면 충분히 무해한 것 같습니다. 실제로 명시적인 크기 인덱스가 없으면 함수가 종료 확인에 실패합니다. 하나의 옵션은 split the function into two mutually recursive definitions입니다. 이 방법은 효과가 있지만 정의 및 관련 교정에 일정량의 중복성을 추가합니다.

마찬가지로, 크기 인덱스를 명시 적으로 부여 할 수 있는지 여부도 확실하지 않으므로 merge에 Agda가 승인 할 서명이 있습니다. These slides은 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의 첫 번째 버전을 수행 the following does 그 :

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 

Answer 1

흥미롭게도, 첫 번째 버전은 실제로 맞습니다. Agda가 Size을 고려한 몇 가지 추가 규칙을 허용한다고 언급했는데 그 중 하나는 ↑ ∞ ≡ ∞입니다. 그런데 다음을 통해 확인할 수 있습니다.

↑inf : ↑ ∞ ≡ ∞ 
↑inf = refl 

글쎄, 다른 규칙이 무엇인지 조사하게되었습니다. 나는 (here를 찾을 수 있습니다) 크기의 종류에 안드레아스 아벨의 슬라이드 안에 그들의 나머지를 발견

• ↑ ∞ ≡ ∞
• i ≤ ↑ i ≤ ∞
• T {i} <: T {↑ i} <: T {∞}

<: 관계는 하위 유형의 관계이다 당신은 객체 지향 언어에서 알 수 있습니다.이이 관계와 관련된 규칙이 포섭 규칙, 또한 : 당신은 유형 A의 값 x이있는 경우

Γ ⊢ x : A Γ ⊢ A <: B 
────────────────────── (sub) 
     Γ ⊢ x : B 

은, 그래서 당신은 A이 B의 하위 유형 것을 알고, 당신은 것으로 x을 처리 할 수 ​​있습니다 형식은 B입니다. 크기가 큰 유형의 하위 유형 지정 규칙을 따르면 SortedList l u {ι} 유형의 값을 SortedList l u으로 처리 할 수 ​​있어야하므로 이상하게 보입니다.

그래서 나는 조금 파고 가서 이것을 발견했습니다. bug report. 실제로 문제는 Agda가 크기를 올바르게 인식하지 못하고 규칙이 실행되지 않는다는 것입니다. 내가 할 필요가 모든에 SortedList의 정의를 다시 작성했다 :

data SortedList (l u : A) : {ι : Size} → Set (⊔ ℓ) where 
    -- ... 

그리고 바로 그거야!

---

부록으로, 여기에 내가 테스트에 사용 된 코드이다 : 모든

data ℕ : {ι : _} → Set where   -- does not work 
-- data ℕ : {ι : Size} → Set where -- works 
    zero : ∀ {ι} →   ℕ {↑ ι} 
    suc : ∀ {ι} → ℕ {ι} → ℕ {↑ ι} 

test : ∀ {ι} → ℕ {ι} → ℕ 
test n = n