了解关于 FSA 和 Agda 中常规语言的简单证明的递归调用失败
Understanding failures of recursive calls on simple proof about FSA and regular languages in Agda
我试图证明 Agda 中的简单 FSA 只接受以零结尾的字符串——这是 Sipser 书中的第一个例子。我没有将 evalFSA 作为谓词来实现，而是作为函数来实现，我对这是正确还是错误的选择感到困惑，因为我现在无法证明机器和语言的可靠性和完整性结果，以及这个实现细节是否是我遇到困难的原因。
只要我在下面的 x 上进行模式匹配，它就会将下面的行突出显示为蓝色。这是什么意思，为什么要这样做，为什么 x0 上的模式匹配可以解决它？
soundM : (xs : List Σ') → evalFSA' M xs → endsIn0 xs
soundM (x ∷ []) evM = {!!}
soundM (x0 ∷ x1 ∷ xs) evM = {!!}
-- soundM (0' ∷ []) f = tt
这是最后一期了。为什么我不能在 1' 的情况下应用递归调用？ f 之间的唯一区别是使用机器的当前状态和输入字符串，但显然这似乎是系统的对称性，不应影响我们的计算能力。
soundM' : (xs : List Σ') → evalFSA' M xs → endsIn0 xs
soundM' (0' ∷ []) evM = tt
soundM' (0' ∷ x1 ∷ xs) f = soundM' (x1 ∷ xs) f
soundM' (1' ∷ x1 ∷ xs) f = soundM' {!!} f
这是在 0' 情况下推断的 f：
f : modal.helper M 0' (x1 ∷ xs) M xs (δ' S₁ x1)
同样在 1' 的情况下：
f : modal.helper M 1' (x1 ∷ xs) M xs (δ' S₂ x1)
我同时遇到了所谓的完整性问题
completeM : (xs : List Σ') → endsIn0 xs → evalFSA' M xs ≡ ⊤
completeM (0' ∷ []) ex = refl
completeM (0' ∷ x1 ∷ xs) ex = completeM (x1 ∷ xs) ex
completeM (1' ∷ x1 ∷ xs) ex = {!!}
这是到达此处的代码
module fsa where
open import Bool
open import Level using (_⊔_)
open import Data.Nat.Base as Nat using (ℕ; zero; suc; _<′_; _+_)
open import Data.List.Base as List using (List; []; _∷_)
-- open import Data.Product as Prod using (∃; _×_; _,_)
open import Data.Empty
open import Data.Unit
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
-- open import Data.Fin as Fin
record FSA : Set₁ where
field
Q : Set
Σ : Set
δ : Q → Σ → Q
q₀ : Q
F : Q → Set
evalFSA' : (fsa : FSA) → List (FSA.Σ fsa) → Set
evalFSA' fsa [] = ⊥
evalFSA' fsa (x ∷ xs) = helper fsa (x ∷ xs) (FSA.q₀ fsa)
where
helper : (fsa : FSA) → List (FSA.Σ fsa) → (FSA.Q fsa) → Set
helper fsa [] q = FSA.F fsa q
helper fsa (x ∷ xs) q = helper fsa xs ((FSA.δ fsa) q x)
data Q' : Set where
S₁ : Q'
S₂ : Q'
data Σ' : Set where
0' : Σ'
1' : Σ'
q₀' : Q'
q₀' = S₁
F' : Q' → Set
F' S₁ = ⊤
F' S₂ = ⊥
δ' : Q' → Σ' → Q'
δ' S₁ 0' = S₁
δ' S₁ 1' = S₂
δ' S₂ 0' = S₁
δ' S₂ 1' = S₂
M : FSA
FSA.Q M = Q'
FSA.Σ M = Σ'
FSA.δ M = δ'
FSA.q₀ M = q₀'
FSA.F M = F'
exF1 = evalFSA' M (0' ∷ [])
exF2 = evalFSA' M (1' ∷ (0' ∷ 0' ∷ 1' ∷ []))
-- a more general endIn that i was orignally trying to use, but likewise failed to get to work
data Dec (A : Set) : Set where
yes : A → Dec A
no : (A → ⊥) → Dec A
sigDec : (x y : Σ') → Dec (x ≡ y)
sigDec 0' 0' = yes refl
sigDec 0' 1' = no (λ ())
sigDec 1' 0' = no (λ ())
sigDec 1' 1' = yes refl
endsIn : {X : Set} → ((x y : X) → Dec (x ≡ y)) → List X → X → Set
endsIn d [] x = ⊥
endsIn d (x ∷ []) x0 with (d x0 x)
... | yes refl = ⊤
... | no x1 = ⊥
endsIn d (x ∷ x1 ∷ xs) x0 = endsIn d (x1 ∷ xs) x0
_endsIn'_ : List Σ' → Σ' → Set
xs endsIn' x = endsIn sigDec xs x
endsIn0 : List Σ' → Set
endsIn0 [] = ⊥
endsIn0 (0' ∷ []) = ⊤
endsIn0 (0' ∷ x ∷ xs) = endsIn0 (x ∷ xs)
endsIn0 (1' ∷ xs) = endsIn0 xs
-- testing
10endsin0 = (1' ∷ 0' ∷ []) endsIn' 0'
n10endsin0 = (1' ∷ 1' ∷ []) endsIn' 0'
您的 post 非常大，包含很多元素，都可以用不同的方式进行评论。我将一一解决它们，并解释我为使这些元素更易于访问而做出的选择。请注意，这些选择包含在您的代码中的次要元素中，主要是装饰性的，它们不会以任何方式改变您定义的语义。我首先详细给你正确的代码，然后我回答问题。
详细的正确代码
让我们首先将这些导入清理到所需的最低限度：
module FSA where
open import Data.List.Base
open import Data.Empty
open import Data.Unit
然后我保留了你对自动机记录的定义：
record FSA : Set₁ where
field
Q : Set
Σ : Set
δ : Q → Σ → Q
q₀ : Q
F : Q → Set
我已经从 evalFSA' 函数中提取了您的 helper 函数。这种变化的原因是，当使用 when 时，该函数继承了父函数的所有参数，这使得更难以理解 modal.helper M 0' (x1 ∷ xs) M xs (δ' S₁ x1).
等进一步的目标。
helper : (fsa : FSA) → List (FSA.Σ fsa) → (FSA.Q fsa) → Set
helper fsa [] q = FSA.F fsa q
helper fsa (x ∷ xs) q = helper fsa xs ((FSA.δ fsa) q x)
evalFSA' : (fsa : FSA) → List (FSA.Σ fsa) → Set
evalFSA' fsa [] = ⊥
evalFSA' fsa (x ∷ xs) = helper fsa (x ∷ xs) (FSA.q₀ fsa)
然后你的案例研究自动机保持不变，尽管我简化了记录实例化而不使用copatterns:
data Q' : Set where
S₁ : Q'
S₂ : Q'
data Σ' : Set where
0' : Σ'
1' : Σ'
q₀' : Q'
q₀' = S₁
F' : Q' → Set
F' S₁ = ⊤
F' S₂ = ⊥
δ' : Q' → Σ' → Q'
δ' S₁ 0' = S₁
δ' S₁ 1' = S₂
δ' S₂ 0' = S₁
δ' S₂ 1' = S₂
M : FSA
M = record { Q = Q' ; Σ = Σ' ; δ = δ' ; q₀ = q₀' ; F = F' }
我还简化了你的谓词endsWith0如下：
endsWith0 : List Σ' → Set
endsWith0 [] = ⊥
endsWith0 (0' ∷ []) = ⊤
endsWith0 (_ ∷ xs) = endsWith0 xs
至此，soundM和completeM证明如下（我将他们的签名同质化）：
soundM : ∀ xs → evalFSA' M xs → endsWith0 xs
soundM (0' ∷ []) evM = evM
soundM (0' ∷ x₁ ∷ xs) evM = soundM (x₁ ∷ xs) evM
soundM (1' ∷ 0' ∷ xs) evM = soundM (0' ∷ xs) evM
soundM (1' ∷ 1' ∷ xs) evM = soundM (1' ∷ xs) evM
completeM : ∀ xs → endsWith0 xs → evalFSA' M xs
completeM (0' ∷ []) ex = ex
completeM (0' ∷ x₁ ∷ xs) = completeM (x₁ ∷ xs)
completeM (1' ∷ 0' ∷ xs) = completeM (0' ∷ xs)
completeM (1' ∷ 1' ∷ xs) = completeM (1' ∷ xs)
非证明相关问题的答案
- 关于谓词与返回类型的函数，您问过：
I didn't implement evalFSA as a predicate, but rather as function,
and am confused as to whether this was the right or wrong choice
这个问题没有好的答案。这两种想法都是可能的，并且经常在本网站上就其他问题进行辩论。我个人总是尽可能使用谓词，但其他人有支持函数返回 ⊤ 或 ⊥ 的论据。而且，正如您所注意到的，可以使用您的实现来证明您想要什么。
- 关于奇怪的突出显示，你问：
it highlights the below line blue. what does this mean
据我所知，这是一个错误。我最近也开始偶尔出现这种奇怪的颜色，但它们显然没有任何意义。
你的证明相关问题的答案
您提出了以下问题：
why can't I apply the recursive call in the 1' case? the only
difference between the f's is the use current state of the machine and
the input string, but obviously this seems like a symmetry of the
system that shouldn't effect our ability to compute
回答这个问题其实很简单，但这个答案在你的实现中有些隐藏，因为你将 helper 的定义嵌入到 evalFSA' 的定义中，我按照解释进行了更改。
让我们考虑下面的代码来证明soundM：
soundM : (xs : List Σ') → evalFSA' M xs → endsWith0 xs
soundM (0' ∷ []) evM = evM
soundM (0' ∷ x ∷ xs) evM = soundM (x ∷ xs) {!evM!}
soundM (1' ∷ x ∷ xs) evM = soundM (x ∷ xs) {!evM!}
当询问 Agda 目标是什么以及第一个目标中当前元素的类型时，它回答：
Goal: helper M xs (δ' q₀' x)
Have: helper M xs (δ' S₁ x)
由于您定义了 q₀' 如下：
q₀' : Q'
q₀' = S₁
Agda 知道 q₀' 在定义上等于 S₁ 这意味着当前术语实际上与目标具有相同的类型，这就是它被接受的原因。
然而，在另一个洞中，向 Agda 询问相同的信息得到：
Goal: helper M xs (δ' q₀' x)
Have: helper M xs (δ' S₂ x)
在这种情况下，q₀' 在定义上不等于 S₂（实际上在任何方面都不相等）这意味着这些类型不相等，并且无法立即得出结论.
如我的代码所示，在 x 上再进行一次模式匹配允许 agda 进一步减少目标，这让我们可以得出结论。
类似的推理被用来证明completeM
我试图证明 Agda 中的简单 FSA 只接受以零结尾的字符串——这是 Sipser 书中的第一个例子。我没有将 evalFSA 作为谓词来实现，而是作为函数来实现，我对这是正确还是错误的选择感到困惑，因为我现在无法证明机器和语言的可靠性和完整性结果，以及这个实现细节是否是我遇到困难的原因。
只要我在下面的 x 上进行模式匹配，它就会将下面的行突出显示为蓝色。这是什么意思，为什么要这样做，为什么 x0 上的模式匹配可以解决它？
soundM : (xs : List Σ') → evalFSA' M xs → endsIn0 xs
soundM (x ∷ []) evM = {!!}
soundM (x0 ∷ x1 ∷ xs) evM = {!!}
-- soundM (0' ∷ []) f = tt
这是最后一期了。为什么我不能在 1' 的情况下应用递归调用？ f 之间的唯一区别是使用机器的当前状态和输入字符串，但显然这似乎是系统的对称性，不应影响我们的计算能力。
soundM' : (xs : List Σ') → evalFSA' M xs → endsIn0 xs
soundM' (0' ∷ []) evM = tt
soundM' (0' ∷ x1 ∷ xs) f = soundM' (x1 ∷ xs) f
soundM' (1' ∷ x1 ∷ xs) f = soundM' {!!} f
这是在 0' 情况下推断的 f：
f : modal.helper M 0' (x1 ∷ xs) M xs (δ' S₁ x1)
同样在 1' 的情况下：
f : modal.helper M 1' (x1 ∷ xs) M xs (δ' S₂ x1)
我同时遇到了所谓的完整性问题
completeM : (xs : List Σ') → endsIn0 xs → evalFSA' M xs ≡ ⊤
completeM (0' ∷ []) ex = refl
completeM (0' ∷ x1 ∷ xs) ex = completeM (x1 ∷ xs) ex
completeM (1' ∷ x1 ∷ xs) ex = {!!}
这是到达此处的代码
module fsa where
open import Bool
open import Level using (_⊔_)
open import Data.Nat.Base as Nat using (ℕ; zero; suc; _<′_; _+_)
open import Data.List.Base as List using (List; []; _∷_)
-- open import Data.Product as Prod using (∃; _×_; _,_)
open import Data.Empty
open import Data.Unit
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
-- open import Data.Fin as Fin
record FSA : Set₁ where
field
Q : Set
Σ : Set
δ : Q → Σ → Q
q₀ : Q
F : Q → Set
evalFSA' : (fsa : FSA) → List (FSA.Σ fsa) → Set
evalFSA' fsa [] = ⊥
evalFSA' fsa (x ∷ xs) = helper fsa (x ∷ xs) (FSA.q₀ fsa)
where
helper : (fsa : FSA) → List (FSA.Σ fsa) → (FSA.Q fsa) → Set
helper fsa [] q = FSA.F fsa q
helper fsa (x ∷ xs) q = helper fsa xs ((FSA.δ fsa) q x)
data Q' : Set where
S₁ : Q'
S₂ : Q'
data Σ' : Set where
0' : Σ'
1' : Σ'
q₀' : Q'
q₀' = S₁
F' : Q' → Set
F' S₁ = ⊤
F' S₂ = ⊥
δ' : Q' → Σ' → Q'
δ' S₁ 0' = S₁
δ' S₁ 1' = S₂
δ' S₂ 0' = S₁
δ' S₂ 1' = S₂
M : FSA
FSA.Q M = Q'
FSA.Σ M = Σ'
FSA.δ M = δ'
FSA.q₀ M = q₀'
FSA.F M = F'
exF1 = evalFSA' M (0' ∷ [])
exF2 = evalFSA' M (1' ∷ (0' ∷ 0' ∷ 1' ∷ []))
-- a more general endIn that i was orignally trying to use, but likewise failed to get to work
data Dec (A : Set) : Set where
yes : A → Dec A
no : (A → ⊥) → Dec A
sigDec : (x y : Σ') → Dec (x ≡ y)
sigDec 0' 0' = yes refl
sigDec 0' 1' = no (λ ())
sigDec 1' 0' = no (λ ())
sigDec 1' 1' = yes refl
endsIn : {X : Set} → ((x y : X) → Dec (x ≡ y)) → List X → X → Set
endsIn d [] x = ⊥
endsIn d (x ∷ []) x0 with (d x0 x)
... | yes refl = ⊤
... | no x1 = ⊥
endsIn d (x ∷ x1 ∷ xs) x0 = endsIn d (x1 ∷ xs) x0
_endsIn'_ : List Σ' → Σ' → Set
xs endsIn' x = endsIn sigDec xs x
endsIn0 : List Σ' → Set
endsIn0 [] = ⊥
endsIn0 (0' ∷ []) = ⊤
endsIn0 (0' ∷ x ∷ xs) = endsIn0 (x ∷ xs)
endsIn0 (1' ∷ xs) = endsIn0 xs
-- testing
10endsin0 = (1' ∷ 0' ∷ []) endsIn' 0'
n10endsin0 = (1' ∷ 1' ∷ []) endsIn' 0'
您的 post 非常大，包含很多元素，都可以用不同的方式进行评论。我将一一解决它们，并解释我为使这些元素更易于访问而做出的选择。请注意，这些选择包含在您的代码中的次要元素中，主要是装饰性的，它们不会以任何方式改变您定义的语义。我首先详细给你正确的代码，然后我回答问题。
详细的正确代码
让我们首先将这些导入清理到所需的最低限度：
module FSA where
open import Data.List.Base
open import Data.Empty
open import Data.Unit
然后我保留了你对自动机记录的定义：
record FSA : Set₁ where
field
Q : Set
Σ : Set
δ : Q → Σ → Q
q₀ : Q
F : Q → Set
我已经从 evalFSA' 函数中提取了您的 helper 函数。这种变化的原因是，当使用 when 时，该函数继承了父函数的所有参数，这使得更难以理解 modal.helper M 0' (x1 ∷ xs) M xs (δ' S₁ x1).
helper : (fsa : FSA) → List (FSA.Σ fsa) → (FSA.Q fsa) → Set
helper fsa [] q = FSA.F fsa q
helper fsa (x ∷ xs) q = helper fsa xs ((FSA.δ fsa) q x)
evalFSA' : (fsa : FSA) → List (FSA.Σ fsa) → Set
evalFSA' fsa [] = ⊥
evalFSA' fsa (x ∷ xs) = helper fsa (x ∷ xs) (FSA.q₀ fsa)
然后你的案例研究自动机保持不变，尽管我简化了记录实例化而不使用copatterns:
data Q' : Set where
S₁ : Q'
S₂ : Q'
data Σ' : Set where
0' : Σ'
1' : Σ'
q₀' : Q'
q₀' = S₁
F' : Q' → Set
F' S₁ = ⊤
F' S₂ = ⊥
δ' : Q' → Σ' → Q'
δ' S₁ 0' = S₁
δ' S₁ 1' = S₂
δ' S₂ 0' = S₁
δ' S₂ 1' = S₂
M : FSA
M = record { Q = Q' ; Σ = Σ' ; δ = δ' ; q₀ = q₀' ; F = F' }
我还简化了你的谓词endsWith0如下：
endsWith0 : List Σ' → Set
endsWith0 [] = ⊥
endsWith0 (0' ∷ []) = ⊤
endsWith0 (_ ∷ xs) = endsWith0 xs
至此，soundM和completeM证明如下（我将他们的签名同质化）：
soundM : ∀ xs → evalFSA' M xs → endsWith0 xs
soundM (0' ∷ []) evM = evM
soundM (0' ∷ x₁ ∷ xs) evM = soundM (x₁ ∷ xs) evM
soundM (1' ∷ 0' ∷ xs) evM = soundM (0' ∷ xs) evM
soundM (1' ∷ 1' ∷ xs) evM = soundM (1' ∷ xs) evM
completeM : ∀ xs → endsWith0 xs → evalFSA' M xs
completeM (0' ∷ []) ex = ex
completeM (0' ∷ x₁ ∷ xs) = completeM (x₁ ∷ xs)
completeM (1' ∷ 0' ∷ xs) = completeM (0' ∷ xs)
completeM (1' ∷ 1' ∷ xs) = completeM (1' ∷ xs)
非证明相关问题的答案
- 关于谓词与返回类型的函数，您问过：
I didn't implement evalFSA as a predicate, but rather as function, and am confused as to whether this was the right or wrong choice
这个问题没有好的答案。这两种想法都是可能的，并且经常在本网站上就其他问题进行辩论。我个人总是尽可能使用谓词，但其他人有支持函数返回 ⊤ 或 ⊥ 的论据。而且，正如您所注意到的，可以使用您的实现来证明您想要什么。
- 关于奇怪的突出显示，你问：
it highlights the below line blue. what does this mean
据我所知，这是一个错误。我最近也开始偶尔出现这种奇怪的颜色，但它们显然没有任何意义。
你的证明相关问题的答案
您提出了以下问题：
why can't I apply the recursive call in the 1' case? the only difference between the f's is the use current state of the machine and the input string, but obviously this seems like a symmetry of the system that shouldn't effect our ability to compute
回答这个问题其实很简单，但这个答案在你的实现中有些隐藏，因为你将 helper 的定义嵌入到 evalFSA' 的定义中，我按照解释进行了更改。
让我们考虑下面的代码来证明soundM：
soundM : (xs : List Σ') → evalFSA' M xs → endsWith0 xs
soundM (0' ∷ []) evM = evM
soundM (0' ∷ x ∷ xs) evM = soundM (x ∷ xs) {!evM!}
soundM (1' ∷ x ∷ xs) evM = soundM (x ∷ xs) {!evM!}
当询问 Agda 目标是什么以及第一个目标中当前元素的类型时，它回答：
Goal: helper M xs (δ' q₀' x)
Have: helper M xs (δ' S₁ x)
由于您定义了 q₀' 如下：
q₀' : Q'
q₀' = S₁
Agda 知道 q₀' 在定义上等于 S₁ 这意味着当前术语实际上与目标具有相同的类型，这就是它被接受的原因。
然而，在另一个洞中，向 Agda 询问相同的信息得到：
Goal: helper M xs (δ' q₀' x)
Have: helper M xs (δ' S₂ x)
在这种情况下，q₀' 在定义上不等于 S₂（实际上在任何方面都不相等）这意味着这些类型不相等，并且无法立即得出结论.
如我的代码所示，在 x 上再进行一次模式匹配允许 agda 进一步减少目标，这让我们可以得出结论。
类似的推理被用来证明completeM