What's a good way to represent free groups?

6
votes

It's easy to represent free magmas (binary leaf trees), free semigroups (non-empty lists), and free monoids (lists), and not hard to prove that they actually are what they claim to be. But free groups seem a lot trickier. There seem to be at least two approaches to using the usual List (Either a) representation:

  1. Encode in a type the requirement that if you have Left a :: Right b :: ... then Not (a = b) and the other way around. It seems likely to be a bit tough to build these.
  2. Work over an equivalence relation allowing arbitrary insertion/deletion of Left a :: Right a :: ... pairs (and the other way around). Expressing this relation seems horrifyingly complicated.

Anyone else have a better idea?

Edit

I just realized that option (1), which the sole answer uses, simply cannot work in the most general setting. In particular, it becomes impossible to define the group operation without imposing decidable equality!

Edit 2

I should've thought to Google this first. It looks like Joachim Breitner did it in Agda a few years ago, and from his introductory description, it looks like he started with option 1, but ultimately chose option 2. I guess I'll attempt it myself, and if I get too stuck I'll look at his code.

1
agdadependent-typeidris

1 Answers

1
votes

As a first approximation I would define this data type as

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)

One another variant is

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)

but this double prepending doesn't look promising to me.