了解关于FSA和Agda中常规语言的简单证明的递归调用失败

问题描述 投票：0回答：1

我正在尝试证明，Agda中的简单FSA仅接受以0结尾的字符串-这是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'
recursion functional-programming state-machine regular-language agda
1个回答
0
投票

您的帖子很大，包含许多元素，所有元素都可以用不同的方式进行评论。我将逐一介绍这些内容，并说明为使这些元素更易于访问而做出的选择。请注意，这些选择包含在代码中的次要元素中，大部分是修饰性元素，它们不会以任何方式改变定义的语义。首先，为您提供正确的详细代码，然后我回答问题。

详细的正确代码

让我们首先将这些进口清理到所需的最低限度：

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

我已经从helper功能中提取了evalFSA'功能。进行此更改的原因是，在使用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)

然后，您的案例研究自动机保持不变，尽管我简化了记录实例化，但没有使用协同模式：
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

从现在开始，您所称的FSA的健全性和完整性，证明如下：
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)

与非证明相关的问题的答案
  1. 关于谓词与返回类型的函数，您问：

    2. 我不是将evalFSA作为谓词来实现，而是作为函数来实现， 并对这是正确还是错误的选择感到困惑

此问题没有好的答案。这两种想法都是可能的，并且经常在该站点上就其他问题进行辩论。我个人总是在可能的情况下使用谓词，但是其他人则使用支持返回⊤或⊥的函数的参数。而且，正如您所注意到的，可以使用实现来证明您想要的东西。

  1. 在奇怪的突出显示上，您问：

    2. 突出显示下面的蓝色行。这是什么意思

据我所知，这是一个错误。像这样的奇怪的变色最近也开始在我身上偶发，但它们显然没有任何意义。

与证明有关的问题的答案

您问了以下问题：

为什么我不能在1'的情况下应用递归调用？唯一的 f之间的差异是机器的当前使用状态 输入字符串，但显然这似乎是对称的 不会影响我们计算能力的系统

回答这个问题实际上很简单，但是这个答案在您的实现中有些隐藏，因为您将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!}

问阿格达第一个目标的目标是什么以及当前元素的类型时，它回答：
Goal: helper M xs (δ' q₀' x)
Have: helper M xs (δ' S₁ x)

由于您已如下定义q₀'：
q₀' : Q'
q₀' = S₁

[Agda知道q₀'在定义上等于S₁，这意味着当前术语实际上与目标具有相同的类型，这就是为什么它被接受的原因。

但是在另一个洞里，向阿格达询问相同的信息会给出：

Goal: helper M xs (δ' q₀' x)
Have: helper M xs (δ' S₂ x)

在这种情况下，q₀'在定义上不等于S₂（并且实际上不以任何方式相等），这意味着这些类型不相等，并且不可能立即得出结论。

如我的代码所示，模式匹配x₁上的额外时间使agda进一步降低了目标，使我们可以得出结论。

使用类似的推理提供completeM的证明

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.