在 Agda 中形式化多个类型判断 ⊢ 在同一个 Γ 内

Question

我是 Agda 初学者！ Programming language foundations in Agda和Verified functional programming in Agda我都读过，现在我想自己尝试将一种小语言形式化。由于我对代数效果和处理程序感兴趣，我从 Pretnar 的教程 "An Introduction to Algebraic Effects and Handlers" 开始。 Pretnar 的语言有 2 种类型判断（Γ ⊢ 值和 Γ ⊢ 计算），因为通常遵循接近 CBPV 的方法。此外，正如 PLPA 中所建议的那样，我正在尝试使用 de Bruijn 表示。

我有的一些代码：

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，但我似乎可以找到一种方法来证明统一它们的“主要”重命名函数。我想知道这是否是正确的方法，我只需要证明我的证明（如果是的话，怎么做？）......或者还有另一种更好的方法来形式化我感兴趣的语言阿格达？

Answer 1

如果你写

rename ρ (⋆ E) = {!!}

并查看孔中的上下文，您会看到E 的类型为.Γ ⊢ₑ .A。这可以使用renameₑ 轻松重命名：

renameₑ ρ E

它是.Δ ⊢ₑ .A 类型，只需将⋆ 应用于结果即可获得.Δ ⊢ .A。

基本思想是你对一个术语进行模式匹配，确定它是一个值还是一个计算，应用相应的重命名函数并使用相同的构造函数包装结果。 IE。 rename 将值映射到值，将计算映射到计算，但在后台使用不同的重命名函数来进行这些判断。

代码：

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