6

表示自由岩浆（二叉叶树）、自由半群（非空列表）和自由幺半群（列表）很容易，并且不难证明它们实际上就是它们声称的那样。但自由团体似乎要棘手得多。似乎至少有两种使用通常List (Either a)表示的方法：

  1. 编码类型的要求，如果你有Left a :: Right b :: ...那么Not (a = b)和反之亦然。构建这些似乎有点困难。
  2. 处理允许任意插入/删除对（反之亦然）的等价关系Left a :: Right a :: ...。表达这种关系似乎非常复杂。

还有人有更好的主意吗？

编辑

我刚刚意识到唯一答案使用的选项（1）在最一般的设置中根本无法工作。特别是，如果不施加可判定的相等性，就不可能定义组操作！

编辑 2

我应该首先想到谷歌。看起来 Joachim Breitner几年前在 Agda 做过，从他的介绍性描述来看，他似乎从选项 1 开始，但最终选择了选项 2。我想我会自己尝试，如果我太卡住了我看看他的代码。

4

1 回答 1

1

作为第一个近似值，我将此数据类型定义为

open import Relation.Binary.PropositionalEquality
open import Data.Sum
open import Data.List

infixr 5 _∷ᶠ_

invert : ∀ {α} {A : Set α} -> A ⊎ A -> A ⊎ A
invert (inj₁ x) = inj₂ x
invert (inj₂ x) = inj₁ x

data Consable {α} {A : Set α} (x : A ⊎ A) : List (A ⊎ A) -> Set α where
  nil  : Consable x []
  cons : ∀ {y xs} -> x ≢ invert y -> Consable x (y ∷ xs)

data FreeGroup {α} {A : Set α} : List (A ⊎ A) -> Set α where
  []ᶠ  : FreeGroup []
  _∷ᶠ_ : ∀ {x xs} -> Consable x xs -> FreeGroup xs -> FreeGroup (x ∷ xs)

另一种变体是

data FreeGroup {α} {A : Set α} : List (A ⊎ A) -> Set α where
  Nil   : FreeGroup []
  Cons1 : ∀ x -> FreeGroup (x ∷ [])
  Cons2 : ∀ {x y xs} -> x ≢ invert y -> FreeGroup (y ∷ xs) -> FreeGroup (x ∷ y ∷ xs)

但是这种双重前置对我来说看起来并不乐观。

于 2015-05-22T07:57:36.990 回答