如何在 Agda 中定义归纳定义类型的子公式?

How to define a subformula of an inductively defined type in Agda?

我试图定义一个简单的谓词来确定公式是否是给定形式的子公式,而不是简单的归纳定义的语法。我 运行 遇到了一些可能很简单的问题。

(i) 我宁愿使用具有给定类型 A 的参数化模块。在 A 具有可决定的相等性的意义上,如何导入 A 是一个集合的信息?如果无法做到这一点,有哪些解决方法?这就是我改用 Nat 的原因。

(ii) t1 ≡ (t2 // t3)(和类似定义的)谓词 isSubFormula 是处理相等子公式的正确方法吗?如果不是,人们还能如何轻松地做到这一点?我还考虑过为 equalFmla 编写一个谓词,然后使用 isSubFormula ⊎ equalFmla 创建一个全局子公式谓词,但我不确定这是否如此干净。

(iii) 当我在第一行内部进行模式匹配时,为什么最后三行突出显示为蓝色?我该如何解决这个问题

(iv) 为什么下面的 {!Data.Nat._≟_ n1 n2 !} 不细化?

module categorial1 (A : Set) where

open import Data.Nat using (ℕ)
open import Data.Empty
open import Data.Sum
open import Relation.Binary.PropositionalEquality

-- type symbols
data tSymb : Set where
  -- base : A → tSymb
  base : ℕ → tSymb
  ~ : tSymb → tSymb
  _\_ : tSymb → tSymb → tSymb
  _//_ : tSymb → tSymb → tSymb

-- A needs a decideable notion of equality
isSubFormula : tSymb → tSymb → Set
-- isSubFormula y (base x) = {!!}
isSubFormula (base n1) (base n2) = {!Data.Nat._≟_ n1 n2 !}
isSubFormula (~ t1) (base x) = ⊥
isSubFormula (t1 \ t2) (base x) = ⊥
isSubFormula (t1 // t2) (base x) = ⊥
isSubFormula t1 (~ t2) = t1 ≡ (~ t2) ⊎ isSubFormula t1 t2
isSubFormula t1 (t2 \ t3) = t1 ≡ (t2 \ t3) ⊎ isSubFormula t1 t2 ⊎ isSubFormula t1 t3
isSubFormula t1 (t2 // t3) = t1 ≡ (t2 // t3) ⊎ isSubFormula t1 t2 ⊎ isSubFormula t1 t3

有很多不同的问题;如果您 post 分别回答每个问题,Stack Overflow 的效果会更好。

不过,这里有一些答案:

(i) I'd rather use a parameterized module with a given type A. How can one import the information that A is a set, in the sense that A has decideable equality?

您可以通过决策程序对您的模块进行参数化,即像这样:

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module categorical1 {A : Set} (_≟_ : Decidable (_≡_ {A = A})) where

请注意,我们在 模块 之前导入 Relation.Binary(对于 Decidable)和 R.B.PropositionalEquality(对于 _≡_ =55=],因为我们模块的参数类型依赖于这些定义。

(iii) Why do the last three lines highlight blue when I pattern match internal to the first one? How can I fix this

这是 Agda 警告你这些子句在定义上不成立,因为它们依赖于与 t1 不匹配的先前子句。

(iv) Why won't the {!Data.Nat. n1 n2 !} refine below?

因为isSubFormula returns一个Set,但是n1 ≟ n2 returns一个Dec _≡_.

我认为您的代码混淆了 isSubFormula 应该是命题还是决策程序。如果它returns一个Set,就说明它是一个命题。您可以在没有可判定相等性的情况下编写,因为没有什么可判定的——两个 base 值的 isSubFormula-ness 意味着它们相等:

isSubFormula : tSymb → tSymb → Set
isSubFormula (base n1) (base n2) = n1 ≡ n2

如果你想要一个决策过程,你可以通过写 isSubFormula : tSymb → tSymb → Bool 来实现“boolean-blindly”,或者将 isSubFormula 作为命题并写​​成 decSubFormula : Decidable isSubFormula .

另请注意,如果您要决定 isSubFormula,则只需要 A 上的可判定相等性,因此您可以

module categorical1 (A : Set) where

... 

isSubFormula : tSymb → tSymb → Set

decSubFormula : Decidable (_≡_ {A = A}) → Decidable isSubFormula
decSubFormula _≟A_ = ? -- You can use _≟A_ here to decide equality of A values