Формализация многовариантных суждений ⊢ в пределах одного и того же Γ в Агде - PullRequest
Новая
       34

Формализация многовариантных суждений ⊢ в пределах одного и того же Γ в Агде

0 голосов
/ 27 августа 2018

Я новичок в Агде! Я прочитал основы языка программирования в Agda и Проверенное функциональное программирование в Agda , и теперь я хочу попытаться формализовать небольшой язык самостоятельно. Поскольку меня интересуют алгебраические эффекты и обработчики, я начал с урока Претнара «Введение в алгебраические эффекты и обработчики» . Язык Претнара имеет два типа суждений (значения Γ and и вычисления Γ)), так как обычно следует подход, близкий к CBPV. Кроме того, как это предлагается в PLPA, я пытаюсь использовать представление де Брюина.

Часть кода, который у меня есть: 

mutual
  data ValueType : Set where
    ~ℕ      : ValueType
    ~?      : ValueType
    ~⊤      : ValueType
    _⟶_    : ValueType → CompType → ValueType
    _⇒_     : CompType → CompType → ValueType

  data CompType : Set where
    _!_ : ValueType → Δ → CompType

data Type : Set where
  ⋆ : ValueType → Type
  ✪ : CompType → Type

data Context : Set where
  ∅   : Context
  _,_ : Context → Type → Context

data _∋_ : Context → Type → Set where
  Z  : ∀ {Γ A}   → Γ , A ∋ A
  S_ : ∀ {Γ A B} → Γ ∋ B → Γ , A ∋ B

mutual
  data _⊢ₖ_ : Context → CompType → Set where
  -- computation defs go here
  data _⊢ₑ_ : Context → ValueType → Set where
  -- values defs go here

data _⊢_ : Context → Type → Set where
  ~_ : ∀ {Γ A}
     → Γ ∋ A
       -----
     → Γ ⊢ A

  ⋆ : ∀ {Γ} {A : ValueType}
    → Γ ⊢ₑ A
      ------
    → Γ ⊢ ⋆ A

  ✪ : ∀ {Γ} {C : CompType}
    → Γ ⊢ₖ C
      -------
    → Γ ⊢ ✪ C

Затем я перехожу к доказательству переименования и подстановки, и здесь возникает моя проблема: как я могу их доказать? 

mutual
  renameₑ : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) 
      → (∀ {A} → Γ ⊢ₑ A → Δ ⊢ₑ A)
  renameₖ : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
      → (∀ {A} → Γ ⊢ₖ A → Δ ⊢ₖ A)

rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
   → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (~ x) = ~ (ρ x)
rename ρ (⋆ A) = {!!} (renameₑ ρ (⋆ A))
rename ρ (✪ A) = {!!} (renameₖ ρ (✪ A))

Я могу доказать rename для каждого из суждений, но я могу найти способ доказать «основную» функцию переименования, которая объединяет их. Интересно, если это правильный путь, и мне просто нужно, чтобы мои доказательства пришли (и если да, то как?) ... или есть другой, лучший способ формализовать интересующий меня язык Agda

1 Ответ

0 голосов
/ 27 августа 2018

Если вы напишите 

rename ρ (⋆ E) = {!!}

и посмотрите на контекст в отверстии, вы увидите, что E имеет тип .Γ ⊢ₑ .A. Это можно легко переименовать, используя renameₑ: 

renameₑ ρ E

, который имеет тип .Δ ⊢ₑ .A, и остается только применить ⋆ к результату, чтобы получить .Δ ⊢ .A.

Основная идея заключается в том, что вы сопоставляете шаблон с термином, выясняете, является ли это значением или вычислением, применяете соответствующую функцию переименования и переносите результат, используя тот же конструктор. То есть rename отображает значения в значения и вычисления в вычисления, но использует различные функции переименования для этих суждений под капотом.

код: 

rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
       → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
rename ρ (~ x) = ~ (ρ x)
rename ρ (⋆ E) = ⋆ (renameₑ ρ E)
rename ρ (✪ E) = ✪ (renameₖ ρ E)
...