Производные структур данных в Агде - PullRequest
Новая
       89

Производные структур данных в Агде

7 голосов
/ 15 апреля 2020

В настоящее время я реализую производные регулярных структур данных в Agda, как это представлено в документе «Контур с одним отверстием» Конором МакБрайдом [5].

При реализации его прямо из статьи OH C , что также было сделано Löh & Magalhães [3,4], у нас осталась функция ⟦_⟧, выделенная красным, поскольку Agda не может сказать, завершатся ли случаи μ и I вместе. Löh & Magalhães прокомментировали это в их хранилище .

Другие документы также включили аналогичную реализацию или определения в свои документы [7,8], но не имеют репо (в по крайней мере, я не смог его найти) [1,2,6], или они следуют другому подходу [9], в котором μ определяется отдельно от Reg, ⟦_⟧ и derive ( или рассечение в их случае), без среды, и операции выполняются в стеке.

Использование флагов {-# TERMINATING #-} или {-# NON_TERMINATING #-} нежелательно. В частности, все, что использует ⟦_⟧, не нормализуется, и поэтому я не могу использовать эту функцию, чтобы доказать что-либо.

Реализация, представленная ниже, является небольшим изменением для реализации OH C. Устраняет ослабление и замещение как часть структурного определения Reg. Что, во-первых, делает ⟦_⟧ счастливым! Но я обнаружил аналогичную проблему при реализации derive - проверка завершения Agda не устраивает случай μ.

Мне не удалось убедить Агду, что derive заканчивается. Мне было интересно, если кто-нибудь успешно реализовал derive с подписью derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n

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

 -- Regular universe, multivariate.
 -- n defines the number of variables
 data Reg : ℕ → Set₁ where
   0′    : {n : ℕ} → Reg n
   1′    : {n : ℕ} → Reg n
   I     : {n : ℕ} → Fin n → Reg n 
   _⨁_  : {n : ℕ} → (l r : Reg n) → Reg n
   _⨂_  : {n : ℕ} → (l r : Reg n) → Reg n
   μ′    : {n : ℕ} → Reg (suc n)   → Reg n

 infixl 30 _⨁_
 infixl 40 _⨂_

 data Env : ℕ → Set₁ where
   []  : Env 0
   _,_ : {n : ℕ} → Reg n → Env n → Env (suc n)

 mutual
   ⟦_⟧ : {n : ℕ} → Reg n → Env n → Set
   ⟦ 0′ ⟧  _ = ⊥
   ⟦ 1′ ⟧  _ = ⊤
   ⟦ I zero  ⟧   (X , Xs) = ⟦ X ⟧  Xs   
   ⟦ I (suc n) ⟧ (X , Xs) = ⟦ I n ⟧ Xs  
   ⟦ L ⨁ R ⟧ Xs = ⟦ L ⟧ Xs ⊎ ⟦ R ⟧ Xs
   ⟦ L ⨂ R ⟧ Xs = ⟦ L ⟧ Xs × ⟦ R ⟧ Xs
   ⟦  μ′ F  ⟧ Xs =  μ F Xs

   data μ {n : ℕ} (F : Reg (suc n)) (Xs : Env n) : Set where
     ⟨_⟩ : ⟦ F ⟧ (μ′ F , Xs) → μ F Xs

 infixl 50 _[_]
 infixl 50 ^_

 _[_]  : {n : ℕ} → Reg (suc n) → Reg n → Reg n
 ^_    : {n : ℕ} → Reg n → Reg (suc n)

 derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
 derive = {!!}

Полный код: https://pastebin.com/awr9Bc0R

[1] Abbott, M., Altenkirch, T., Ghani, N. и McBride, C. (2003). Производные контейнеров. В Международной конференции по типизированным лямбда-исчислениям и их приложениям, страницы 16–30. Springer.

[2] Abbott, M., Altenkirch, T., McBride, C., И Ghani, N. (2005). δ для данных: различающиеся структуры данных. Fundamenta Informaticae, 65 (1-2): 1–28.

[3] Löh, A. & Magalhães JP (2011). Generi c Программирование с индексированными функторами. В материалах седьмого семинара ACM SIGPLAN по программированию Generi c (WGP'11).

[4] Magalhães JP. & Löh, A. (2012) Формальное сравнение подходов к программированию Datatype-Generi c. В материалах четвертого семинара по математически структурированному функциональному программированию (MSFP '12).

[5] McBride, C. (2001). Производная регулярного типа - это тип контекста с одним отверстием. Неопубликованная рукопись, стр. 74–88.

[6] МакБрайд, C. (2008). Клоуны слева от меня, шутники справа (жемчужина): расчленение структур данных. В Уведомлениях ACM SIGPLAN, том 43, страницы 287–295. ACM.

[7] Моррис П., Альтенкирх Т. и Макбрайд C. (2004 г., декабрь). Изучение регулярных типов деревьев. В Международном семинаре по типам доказательств и программ (с. 252-267). Springer, Berlin, Heidelberg.

[8] Sefl, V. (2019). Анализ производительности молнии. Препринт arXiv arXiv: 1908.10926.

[9] Том Кортинас, C. и Swierstra, W. (2018). От алгебры до абстрактной машины: проверенная конструкция generi c. В материалах 3-го Международного семинара ACM SIGPLAN по разработке на основе типов, стр. 78–90. ACM.

1 Ответ

4 голосов
/ 16 апреля 2020

Определение derive заканчивается, вы просто неправильно адаптировали код из репо . Если derive вызывается только на F в случае μ′ F, это явно структурно. В примере кода вместо этого вы попытались использовать ^ (F [ μ′ F ]). 

derive : {n : ℕ} → (i : Fin n) → Reg n → Reg n
derive i 0′ = 0′
derive i 1′ = 0′
derive i (I j) with i ≟ j
derive i (I j) | yes refl = 1′
...            | no _     = 0′
derive i (L ⨁ R) = derive i L ⨁ derive i R
derive i (L ⨂ R) = (derive i L ⨂ R) ⨁ (L ⨂ derive i R)
derive i (μ′ F) = μ′ (    (^ (derive (suc i) F [ μ′ F ]))
                       ⨁ (^ (derive zero F [ μ′ F ])) ⨂ I zero)

Я также предлагаю настроить Reg следующим образом, поскольку n в качестве индекса не требуется, и Set₁. 

data Reg (n : ℕ) : Set where
  0′    : Reg n
  1′    : Reg n
  I     : Fin n → Reg n
  _⨁_  : (l r : Reg n) → Reg n
  _⨂_  : (l r : Reg n) → Reg n
  μ′    : Reg (suc n)  → Reg n
...