Is free group a "recursive type"?

Stream: general

[Kenny Lau]

A "recursive type" is a type defined as the smallest solution (smallest in the sense of universal property) of some type equation, e.g. nat is the solution of T = 1+T and list A is the smallest solution of T=1+AxT.

The free magma generated by a type A, can be defined as the smallest solution of T=A+TxT.

The free semigroup generated by a type A can be defined as the smallest solution of T=A+AxT (sidenote: 1+T satisfies 1+T = 1+A+AxT = 1+Ax(1+T), i.e. 1+T is list A).

The free monoid generated by a type can be defined as list A, which is mentioned above.

Is the free group generated by a type also a recursive type? I believe not, but I don't have a proof.

(Also, this question would need to be phrased properly, in terms of what the allowed operations can be, because by cardinality argument list A would work as the free group over a type)

[Kenny Lau]

@Mario Carneiro you might have a quick answer / reference

[Kenny Lau]

I believe the proper notation is nat = μT.1+T

[Kenny Lau]

list A = μT.1+AxT, free_magma A = μT.A+TxT, free_semigroup A = μT.A+AxT

[Mario Carneiro]

The most natural presentation of free semigroups and such is not as a recursive type, but as a quotient of a recursive type

[Mario Carneiro]

Any free algebraic variety is a quotient of a recursive type

[Kenny Lau]

yeah but it works; whereas I don't think there's one that works for free groups

[Mario Carneiro]

you take all the expressions in the language and quotient by all the equalities and congruences defined for the variety

[Mario Carneiro]

In some cases, it turns out to be equivalent to a recursive type, like the free monoid and list

[Mario Carneiro]

I believe free groups are also such things, but you have to get tricky with a definition of reduced word

[Simon Hudon]

Looks strangely like a QPF

[Mario Carneiro]

yep

[Simon Hudon]

Or rather the fixed point of a QPF

[Mario Carneiro]

all free algebraic varieties are QPFs

[Simon Hudon]

Did Jeremy think of that when he came up with QPFs?

[Kenny Lau]

Can someone loop me in as to what on earth QPF stands for?

[Mario Carneiro]

quotient of a polynomial functor

[Kenny Lau]

I'm not very convinced that free group is equivalent to a polynomial

[Simon Hudon]

Quotient of Polynomial Functors. It's a way of generating arbitrary inductive and coinductive type that we're about to publish

[Kenny Lau]

now I'm not convinced and Mario is convinced, and there is no way to go on because how would I have a proof :P

[Mario Carneiro]

In this case you are asking when we can drop the "quotient" part, and I say in groups you can do it

[Kenny Lau]

right, and I'm not convinced

[Mario Carneiro]

You already know that the set of reduced words is isomorphic with a free group

[Mario Carneiro]

but perhaps you doubt this can be defined as an inductive type

[Kenny Lau]

I hope your solution won't be doing funny things like including a Prop in the inductive type

[Mario Carneiro]

of course it will

[Kenny Lau]

is that a polynomial?

[Kenny Lau]

can I restrict your language to μAT1+x.?

[Reid Barton]

is that even going to be a functor?

[Mario Carneiro]

the functor here is that the whole construction is functorial in the base type A

[Reid Barton]

I think the free group functor is probably not polynomial but I'm not sure how to prove it

[Mario Carneiro]

There is a way to do it with an indexed inductive too

[Kenny Lau]

@Reid Barton well free_group would definitely be a functor, and I think it is independent of construction?

[Mario Carneiro]

you just need to track which words end in what letter so that you prevent constructing non-reduced words

[Kenny Lau]

what is an indexed inductive?

[Mario Carneiro]

inductive foo : X -> Type

[Mario Carneiro]

actually you don't even need to keep track if you are just going for abstractly isomorphic

[Mario Carneiro]

it's just a tree with 2A branches at the root and 2A-1 branches everywhere else

[Kenny Lau]

on an unrelated note I've proved 2 instances of lawful traversable and 1 instance of lawful bitraversable, and I still have no idea what it is

[Kenny Lau]

I'm not sure I'm very comfortable with 2A-1

[Kenny Lau]

my first thought is, it can't be a polynomial; and my second thought is, what if A=0

[Mario Carneiro]

if A=0 then the 2A branches at the root end it right then

[Mario Carneiro]

the point is it's a tree

[Kenny Lau]

also I'm not very sure that you can define multiplication on that type

[Kenny Lau]

what is a * a^-1?

[Mario Carneiro]

1

[Kenny Lau]

yeah but will it be computable?

[Mario Carneiro]

I didn't say anything about computability

[Mario Carneiro]

but in this case yes you can do it

[Mario Carneiro]

if A has decidable eq

[Kenny Lau]

yeah that's the problem

[Kenny Lau]

what if I wanted to define the free group on nat -> bool

[Mario Carneiro]

It's easy to prove that it's necessary

[Kenny Lau]

it's easy to prove that it's necessary if you use that construction?

[Mario Carneiro]

No, with any construction

[Kenny Lau]

the construction in mathlib doesn't need decidable equality

[Mario Carneiro]

If it's not a quotient

[Kenny Lau]

define "not a quotient"

[Mario Carneiro]

using only inductive types

[Mario Carneiro]

like the sort you've been talking about

[Kenny Lau]

could you prove it?

[Mario Carneiro]

First, you have to show that in the construction w = 1 is decidable

[Kenny Lau]

seems very fishy to me

[Kenny Lau]

(because once w=1 is decidable, the whole type has decidable equality)

[Mario Carneiro]

1 has to be obtained by applying some constructors

[Kenny Lau]

interesting

[Mario Carneiro]

and they can't be the same constructors as for constructing w of positive length

[Mario Carneiro]

That's certainly enough for your restricted grammar. For lean inductives there are several other effects you have to eliminate

[Kenny Lau]

thanks

[Reid Barton]

I figured out how to prove the free group functor is not a polynomial--it's kind of the same as what Mario just wrote.
Any polynomial functor is the coproduct, as a functor, of the "constant term" and the "nonconstant terms".
If the free group functor was a polynomial, it would have to be the disjoint union of the constant functor on a singleton (representing the identity element) and the functor of nonidentity elements. But the nonidentity elements don't actually form a functor, because substituting for the symbols in a word of a free group can cause cancellation to the identity.

[Kenny Lau]

nice

[Reid Barton]

But there should be other nonexamples like the free commutative monoid, and I'm not sure how to handle those

[Kenny Lau]

on another note, if a magma has decidable equality, does its quotient by the associator (i.e. the free semigroup) also have decidable equality?

[Kevin Buzzard]

Let me just remark that mathematicians claimed the phrase "algebraic variety" about 100 years ago

[Mario Carneiro]

I'm using the mathematician's terminology, or so I thought

[Mario Carneiro]

that thing from universal algebra where you have a set and a bunch of universal equations on it

[Mario Carneiro]

it's a generalization of ring, group, monoid and so on

[Mario Carneiro]

but not field, because there is a disequality

[Mario Carneiro]

that's why there is no free field

[Reid Barton]

"variety of algebras" but related terms will inevitably collide

[Mario Carneiro]

However, it's not like you have to ask things to be distinct in a free construction. You can just drop that axiom and the free object for that thing will be the free field if it exists

[Kevin Buzzard]

Algebraic variety is some algebraic geometry thing, the zeros of finitely many polynomials in affine or projective space. One interesting thing about learning CS is the new language and new ways of thinking about old things

[Mario Carneiro]

I guess the notions are related, although the universal algebra version seems to be some vast generalization of that

[Mario Carneiro]

(note that asking for a polynomial to be zero is a universal equational constraint of the same sort as in universal algebra)

[Jesse Michael Han]

i've always found the terminology confusing (i think of a universal algebraic variety as a collection of many models, while an algebraic variety is a single model)

[Patrick Massot]

Can someone loop me in as to what on earth QPF stands for?

So young, and he already sleeps during talks...

[Simon Hudon]

@Patrick Massot:
So young, and he already sleeps during talks...

Are those tears of pride?

[Kevin Buzzard]

It's an obscure abbreviation! It's "quotients of polynomial functors" as in Jeremy's talk in Amsterdam. Didn't you guys only just invent it??

[Reid Barton]

But there should be other nonexamples like the free commutative monoid, and I'm not sure how to handle those

I happened to come across https://mathoverflow.net/questions/302631/what-is-the-polynomial-functor-for-the-bag-monad