无法解决的尺寸限制答案

【问题标题】：Unsolvable size constraints无法解决的尺寸限制
【发布时间】：2014-08-14 11:48:56
【问题描述】：

我想在 pi 演算的转换关系的推导上定义一个保持大小的函数。我无法让 Agda 相信它确实可以保持尺寸。我还收到了一条看起来毫无意义的错误消息，因此其中可能有线索。

我已经尽可能地简化了代码，同时仍然保留了设置的风格。这是序言。

{-# OPTIONS --sized-types #-}

module SizedTypes where

   open import Data.Product public hiding (swap)
   open import Relation.Binary.PropositionalEquality
   open import Size

   -- Processes.
   data Proc : Set where
      ν_ : Proc → Proc

   -- Actions.
   data ⟿ᵇ : Set where
      input : ⟿ᵇ
      boundOut : ⟿ᵇ

   data ⟿ᶜ : Set where
      out : ⟿ᶜ

   data ⟿ : Set where
      _ᵇ : ⟿ᵇ → ⟿
      _ᶜ : ⟿ᶜ → ⟿

   -- Renamings.
   data Ren : Set where

   postulate
      push : Ren
      swap : Ren
      _ᴬ*_ : Ren → ⟿ᶜ →  ⟿ᶜ

   -- Transitions.
   data _—[_]→_ : {ι : Size} → Proc → (a : ⟿) → Proc → Set where
      ν•_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P (out ᶜ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (boundOut ᵇ) R
      νᵇ_ : ∀ {ι P R} {a : ⟿ᵇ} → _—[_]→_ {ι = ι} P (boundOut ᵇ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (a ᵇ) (ν R)
      νᶜ_ : ∀ {ι P R} → _—[_]→_ {ι = ι} P ((push ᴬ* out) ᶜ) R →
            _—[_]→_ {ι = ↑ ι} (ν P) (out ᶜ) (ν R)

   infixl 0 _—[_]→_

   postulate
      _ᴾ*_ : Ren → Proc → Proc
      _ᵀ*_ : ∀ {ι} (ρ : Ren) {P R} {a : ⟿ᶜ} → _—[_]→_ {ι = ι} P (a ᶜ) R →
             _—[_]→_ {ι = ι} (ρ ᴾ* P) ((ρ ᴬ* a) ᶜ) (ρ ᴾ* R)
      swap-involutive : ∀ (P : Proc) → swap ᴾ* swap ᴾ* P ≡ P
      swap∘push : swap ᴬ* push ᴬ* out ≡ out

   infixr 8 _ᵀ*_ _ᴾ*_ _ᴬ*_

   -- Structural congruence.
   infix 4 _≅_
   data _≅_ : Proc → Proc → Set where
      νν-swap : ∀ P → ν (ν (swap ᴾ* P)) ≅ ν (ν P)

现在这是我做不到的。

   -- "Residual" of a transition E after a structural congruence φ.
   ⊖ : ∀ {ι P P′} {a : ⟿} {R} (E : _—[_]→_ {ι = ι} P a R) (φ : P ≅ P′) →
       Σ[ R ∈ Proc ] _—[_]→_ {ι = ι} P′ a R
   ⊖ (ν•_ (νᶜ E)) (νν-swap P) with swap ᵀ* E
   ... | swap*E rewrite swap-involutive P | swap∘push =
      _ , {!!} -- νᵇ (ν• swap*E)
   ⊖ E φ = {!!}

大致上，我匹配有相邻 ν 活页夹的情况，并表明如果我转置活页夹（通过在活页夹下应用“交换”重命名），那么推导中的相关步骤也会转置。直观地说，这保留了转换推导的大小。

切换隐藏参数（在 Emacs 中）显示有问题的子句中的目标类型为 _—[_]→_ {↑ (↑ .ι)}，因此我希望能够应用两个构造函数（在本例中为 νᵇ 和 ν•）。我还可以看到 E 具有 _—[_]→_ {.ι} 类型，swap*E 也是如此，所以我（天真地）期望 νᵇ (ν• swap*E) 与目标大小一致。然而，Agda 抱怨约束不一致。

奇怪的是，如果我使用 with 子句将 ν• swap*E 引入上下文，则会收到以下错误：

.ι !=< P of type Size
when checking that the expression E has type
swap ᴾ* P —[ (push ᴬ* out) ᶜ ]→ .R

这令人费解，因为元变量 P 的选择表明 Agda 试图将大小索引与 Proc 类型的变量进行匹配。

我在这里做错了什么？

【问题讨论】：

标签： termination agda

【解决方案1】：

感谢 Andrea Vezzosi 在 Agda 邮件列表中回答此问题。在这种情况下，它就像显式传递 ι 索引一样简单：

⊖ (ν• (νᶜ_ {ι} E)) (νν-swap P) with swap ᵀ* E
   ... | swap*E rewrite swap-involutive P | swap∘push
     = _ , νᵇ (ν•_ {ι = ι} swap*E)

【讨论】：

【解决方案2】：

原来这是bug，原来是fixed in Agda 2.4.0.2。现在可以简单地写：

⊖ (ν• (νᶜ E)) (νν-swap P) with swap ᵀ* E
   ... | swap*E rewrite swap-involutive P | swap∘push
     = _ , νᵇ (ν• swap*E)

正如人们所期望的那样。

【讨论】：