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

编程问答 2022-06-13

问题描述

我正在尝试从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)))

解决方法

我解决此类问题的策略是首先忽略未解决的约束，而是尝试帮助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 ]

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

PS：通常人们更喜欢以等式推理风格（例如参见this example in the standard library）来编写这类证明，这在这种情况下可能会迫使您拼写出隐式参数。

agdacontext-free-grammar