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

Question

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

(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

Answer 1

有很多不同的问题；如果您 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

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

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

types

agda

type-theory

decidable