6

自由マグマ (二分葉木)、自由半群 (非空リスト)、自由モノイド (リスト) を表現するのは簡単で、それらが実際に主張しているものであることを証明するのは難しくありません。しかし、無料のグループはもっとトリッキーに思えます。List (Either a)通常の表現を使用するには、少なくとも 2 つのアプローチがあるようです。

  1. その場合とその逆の要件を型にエンコードしLeft a :: Right b :: ...ますNot (a = b)。これらを構築するのは少し難しいようです。
  2. Left a :: Right a :: ...ペアの任意の挿入/削除 (およびその逆)を許可する等価関係に取り組みます。この関係を表現することは、恐ろしく複雑に思えます。

他の誰かがより良いアイデアを持っていますか?

編集

唯一の答えが使用するオプション（1）は、最も一般的な設定では機能しないことに気付きました。特に、決定可能な平等を課すことなく群演算を定義することは不可能になります!

編集 2

私はこれを最初にGoogleに考えるべきでした。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)

もう1つのバリアントは

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 に答える