使用 CFG 示例调试 Agda 中的约束满足错误

Question

我正在尝试根据 Sipser 的计算理论实现第一个示例，但我得到了一个无法辨认的黄色突出显示。通常如何调试 Agda 中的这些约束错误，特别是在我的示例中？是否有任何成功的技术可以从一开始就避免它们？ SipserExample1 下面会产生这样的混乱：

_r2_61 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r3_62 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r2_66 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]
_r3_67 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]

———— Errors ————————————————————————————————————————————————
Failed to solve the following constraints:
  _r2_66 ++ inj₁ A0 ∷ _r3_67 = inj₁ A0 ∷ []
    : List (CFG.V Sipser1 ⊎ CFG.Σ' Sipser1)
    (blocked on _r2_66)
  _r2_66 ++ (inj₁ B0 ∷ []) ++ _r3_67 = _r2_61 ++ inj₁ A0 ∷ _r3_62
    : List (CFG.V Sipser1 ⊎ CFG.Σ' Sipser1)
    (blocked on any(_r2_61, _r3_62, _r2_66, _r3_67))
  _r2_61 ++ (inj₁ B0 ∷ []) ++ _r3_62
    = inj₂ a0 ∷ map inj₂ (a0 ∷ a# ∷ a1 ∷ a1 ∷ [])
    : List (CFG.V Sipser1 ⊎ CFG.Σ' Sipser1)
    (blocked on _r2_61)

这是生成黄色的代码。 CFG 是一个简单的记录，我在终端和非终端列表上定义了多步缩减关系。 generation 只允许用户证明给定的 CFG 允许的终端列表。

module toy where

open import Data.List 
open import Data.Sum using (_⊎_ ; inj₁; inj₂)
open import Data.Product using (_×_; _,_)
open import Data.Unit
open import Data.Empty

binRel : Set → Set → Set₁
binRel A B = A → B → Set

record CFG : Set₁ where
  field
    V : Set -- non-terminal, or variable
    Σ' : Set -- terminals
    R : binRel V (List (V ⊎ Σ'))-- rules
    S : V -- start symbol

module ManyStep where
  open CFG

  rule : CFG → Set
  rule cfg = List (V cfg ⊎ Σ' cfg)

  data ↦* (cfg : CFG) : rule cfg → rule cfg → Set where
    refl : {r : (rule cfg)} → ↦* cfg r r --∀ {σ : Σ' cfg} → {!!}
    trans : {r1 r2 r3 : (rule cfg)} {v : V cfg} {X : (rule cfg)} → R cfg v X
            → ↦* cfg r1 (r2 ++ (inj₁ v) ∷ r3)
            → ↦* cfg r1 (r2 ++ X ++ r3)

  derives : (cfg : CFG) → rule cfg → Set
  derives cfg x = ↦* cfg (inj₁ (S cfg) ∷ []) x

  generates : (cfg : CFG) → List (Σ' cfg) → Set
  generates cfg xs = derives cfg (map inj₂ xs)

open ManyStep public

data V0 : Set where
  A0 : V0
  B0 : V0

data Σ0 : Set where
  a0 : Σ0
  a1 : Σ0
  a# : Σ0

data _⟶_ : V0 → List (V0 ⊎ Σ0) → Set where
  r0 : A0 ⟶ (inj₂ a0 ∷ inj₁ A0 ∷ inj₂ a1 ∷ [])
  r1 : A0 ⟶ (inj₁ B0 ∷ [])
  r2 : B0 ⟶ (inj₂ a# ∷ [])

Sipser1 : CFG
Sipser1 = record { V = V0 ; Σ' = Σ0 ; R = _⟶_ ; S = A0 }

SipserExample1 : generates Sipser1 (a0 ∷ a0 ∷ a# ∷ a1 ∷ a1 ∷ [])
SipserExample1 = trans r1 (trans r1 (refl {Sipser1} {inj₁ A0 ∷ []}))

-----编辑-----

根据@Jesper 的一些见解，正确的解决方案实际上是：

SipserExample1 : generates Sipser1 (a0 ∷ a0 ∷ a# ∷ a1 ∷ a1 ∷ [])
SipserExample1 = trans {r2 = inj₂ a0 ∷ inj₂ a0 ∷ []} {r3 = inj₂ a1 ∷ inj₂ a1 ∷ []} r2
                 (trans {r2 = inj₂ a0 ∷ inj₂ a0 ∷ []} {r3 = inj₂ a1 ∷ inj₂ a1 ∷ []} r1
                 (trans {r2 = inj₂ a0 ∷ []} {r3 = inj₂ a1 ∷ []} r0

                 (trans {r2 = []} {r3 = []} r0 refl)))

Answer 1

我解决此类问题的策略是首先忽略未解决的约束，而是尝试帮助 Agda 填充未解决的元变量，在您的情况下是以下部分：

_r2_61 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r3_62 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,18-23 ]
_r2_66 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]
_r3_67 : rule Sipser1  [ at /home/wmacmil/agdaFall2019/constructiveTypeTheoriesNLSem/TT_course/agda_files/toy.agda:60,28-33 ]

这些元变量的命名及其位置为您提供了一个很好的线索：它们是 SipserExample1 主体中对 trans 函数的第一次和第二次调用的第二个和第三个隐式参数.下一步是使这些隐式参数显式化：在调用 trans 之后写入 {r2 = ?} {r3 = ?}，重新加载文件，并尝试填充漏洞，直到约束消失或收到正确的错误消息。

PS：通常人们更喜欢用等式推理风格来写这些类型的证明（参见 this example in the standard library），这会迫使你在这种情况下拼出隐含的论点.

使用 CFG 示例调试 Agda 中的约束满足错误

Debugging constraint satisfaction errors in Agda with CFG example

context-free-grammar

agda