Взаимно индуктивные описания с разными типами индексов? - PullRequest
Новая
       116

Взаимно индуктивные описания с разными типами индексов?

1 голос
/ 14 апреля 2020

Я использую описания, как они описаны здесь , как способ кодирования формы индуктивных типов данных. Однако я застрял на том, как представлять индуктивные типы, которые:

  1. Взаимно индуктивные
  2. Имеют разные индексы

Например, предположим, что мы ' у нас есть что-то вроде этого, где мы упорядочиваем разные типы: 

data Foo : Set where
  N : ℕ -> Foo 
  P : (Foo × Foo) -> Foo

data <N : ℕ -> ℕ -> Set where
  <0 : (n : ℕ) -> <N zero n
  <suc : (m n : ℕ) -> <N m n -> <N (suc m) (suc n)

data <P : (Foo × Foo) -> (Foo × Foo) -> Set 
data <F : Foo -> Foo -> Set 

data <P where
  <Pair : (x1 x2 y1 y2 : Foo) -> <F x1 y1 -> <F x2 y2 -> <P (x1 , x2) (y1 , y2)

data <F where
  <FN : ∀ (a b : ℕ) -> <N a b -> <F (N a) (N b)
  <FP : ∀ (p1 p2 : (Foo × Foo) ) -> <P p1 p2 -> <F (P p1) (P p2)

То есть у нас есть тип бинарных деревьев с nats на листьях. У нас есть частичный порядок между деревьями, где мы сравниваем nats обычным способом, и мы сравниваем пары узлов, сравнивая их соответствующие поддеревья.

Обратите внимание, как <F и <P взаимно зависят друг от друга , Конечно, мы могли бы встроить это, чтобы сделать <F и <P одним типом, я стараюсь избегать этого, в случаях, когда <P более сложный.

Что Мне интересно: Можно ли выразить вышеупомянутые типы частичного порядка с помощью описаний?

Я застреваю даже при попытке описать вышеупомянутые типы как фиксированную точку индексированного функтора. Обычно у нас есть индексный тип (I : Set), а функтор имеет тип (X : I -> Set) -> I -> Set. Но мы не можем иметь и «Foo», и «Foo × Foo», которые мы ценим. Есть ли какой-то трюк, который позволяет нам использовать I = Foo ⊎ (Foo × Foo)?

1 Ответ

2 голосов
/ 14 апреля 2020

Возьмите сумму всех индексов: 

Ix = ((Foo × Foo) × (Foo × Foo)) ⊎ (Foo × Foo)

data <P : Ix -> Set
data <F : Ix -> Set

data <P where
  <Pair : (x1 x2 y1 y2 : Foo) -> <F (inj₂(x1 , y1)) -> <F (inj₂(x2 , y2))
                              -> <P (inj₁((x1 , x2), (y1 , y2)))

data <F where
  <FN : ∀ (a b : ℕ) -> <N a b -> <F (inj₂(N a , N b))
  <FP : ∀ (p1 p2 : (Foo × Foo) ) -> <P (inj₁(p1 , p2)) -> <F (inj₂(P p1 , P p2))

Мы можем немного привести в порядок индексы и написать вещи в форме, которая более явно описывается индексированными функторами: 

data Ix : Set where
  <P : Foo × Foo → Foo × Foo → Ix
  <F : Foo → Foo → Ix

data T : Ix → Set where
  <Pair : ∀ x1 x2 y1 y2  → T (<F x1 y1) → T (<F x2 y2)
                         → T (<P (x1 , x2) (y1 , y2))
  <FN : ∀ (a b : ℕ) → <N a b → T (<F (N a) (N b))
  <FP : ∀ p1 p2 → T (<P p1 p2) → T (<F (P p1) (P p2))

Хочу отметить, что <P и <F могут быть определены рекурсивно, поэтому индукция здесь не обязательна. 

<F : Foo → Foo → Set
<F (N n) (N n')              = <N n n'
<F (P (x , y)) (P (x' , y')) = <F x x' × <F y y'
<F (N _) (P _) = ⊥
<F (P _) (N _) = ⊥
...