Понимание сбоев рекурсивных вызовов на простом доказательстве FSA и обычных языков в Agda - PullRequest
Новая
       88

Понимание сбоев рекурсивных вызовов на простом доказательстве FSA и обычных языков в Agda

0 голосов
/ 17 июня 2020

Я пытаюсь доказать, что простой FSA в Agda принимает только строки, оканчивающиеся на ноль - это первый пример в книге 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

Вот вывод f в случае 0 ': 

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'

1 Ответ

4 голосов
/ 18 июня 2020

Ваш пост очень большой и содержит множество элементов, которые можно комментировать по-разному. Я обращусь к ним один за другим и объясню, что сделал, чтобы сделать эти элементы более доступными. Обратите внимание, что этот выбор состоит из второстепенных элементов в ваших кодах, в основном cosmeti c, которые никоим образом не меняют семантику ваших определений. Я начну с того, что дам вам правильный код в деталях, после чего я отвечу на вопросы.

Детальный правильный код

Давайте начнем с очистки этого импорта до минимально необходимого : 

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

С этого момента 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)

Ответы на вопросы, не связанные с доказательством

  1. О предикатах и ​​функциях возвращая типы, вы спросили:

Я реализовал evalFSA не как предикат, а как функцию, и меня смущает, было ли это правильным или неправильным выбором

На этот вопрос нет хорошего ответа. Обе идеи возможны, и на этом сайте часто обсуждаются другие вопросы. Я лично всегда использую предикаты, когда это возможно, но у других есть аргументы в пользу функций, возвращающих ⊤ или ⊥. И, как вы заметили, можно доказать, что вы хотели, используя свою реализацию.

О странном выделении, вы спросили:

он выделяет строку ниже синим цветом. что это значит

Насколько я знаю, это баг. Какая-то странная окраска, подобная этой, стала иногда случаться и со мной в последнее время, но они, видимо, ничего не значат.

Ответьте на ваш вопрос, связанный с проверкой

Вы задали следующий вопрос:

почему я не могу применить рекурсивный вызов в 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!}

На вопрос 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₀' по определению не является e qual to S₂ (и на самом деле не равны), что означает, что эти типы не равны, и невозможно сразу сделать вывод.

Как показано в моем коде, сопоставление с образцом в x позволяет agda еще больше уменьшить цель, что позволяет нам сделать вывод.

Аналогичное рассуждение используется для доказательства completeM

...