Zulip Chat Archive

Stream: general

Topic: Is free group a "recursive type"?


Kenny Lau (Feb 17 2019 at 22:23):

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 (Feb 17 2019 at 22:23):

@Mario Carneiro you might have a quick answer / reference

Kenny Lau (Feb 17 2019 at 22:26):

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

Kenny Lau (Feb 17 2019 at 22:27):

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

Mario Carneiro (Feb 17 2019 at 22:30):

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 (Feb 17 2019 at 22:31):

Any free algebraic variety is a quotient of a recursive type

Kenny Lau (Feb 17 2019 at 22:31):

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

Mario Carneiro (Feb 17 2019 at 22:31):

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

Mario Carneiro (Feb 17 2019 at 22:32):

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

Mario Carneiro (Feb 17 2019 at 22:33):

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

Simon Hudon (Feb 17 2019 at 22:33):

Looks strangely like a QPF

Mario Carneiro (Feb 17 2019 at 22:33):

yep

Simon Hudon (Feb 17 2019 at 22:33):

Or rather the fixed point of a QPF

Mario Carneiro (Feb 17 2019 at 22:33):

all free algebraic varieties are QPFs

Simon Hudon (Feb 17 2019 at 22:34):

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

Kenny Lau (Feb 17 2019 at 22:34):

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

Mario Carneiro (Feb 17 2019 at 22:35):

quotient of a polynomial functor

Kenny Lau (Feb 17 2019 at 22:35):

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

Simon Hudon (Feb 17 2019 at 22:35):

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

Kenny Lau (Feb 17 2019 at 22:36):

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 (Feb 17 2019 at 22:36):

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

Kenny Lau (Feb 17 2019 at 22:37):

right, and I'm not convinced

Mario Carneiro (Feb 17 2019 at 22:37):

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

Mario Carneiro (Feb 17 2019 at 22:37):

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

Kenny Lau (Feb 17 2019 at 22:37):

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

Mario Carneiro (Feb 17 2019 at 22:38):

of course it will

Kenny Lau (Feb 17 2019 at 22:38):

is that a polynomial?

Kenny Lau (Feb 17 2019 at 22:38):

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

Reid Barton (Feb 17 2019 at 22:38):

is that even going to be a functor?

Mario Carneiro (Feb 17 2019 at 22:39):

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

Reid Barton (Feb 17 2019 at 22:40):

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

Mario Carneiro (Feb 17 2019 at 22:40):

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

Kenny Lau (Feb 17 2019 at 22:41):

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

Mario Carneiro (Feb 17 2019 at 22:41):

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

Kenny Lau (Feb 17 2019 at 22:41):

what is an indexed inductive?

Mario Carneiro (Feb 17 2019 at 22:41):

inductive foo : X -> Type

Mario Carneiro (Feb 17 2019 at 22:43):

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

Mario Carneiro (Feb 17 2019 at 22:44):

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

Kenny Lau (Feb 17 2019 at 22:45):

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 (Feb 17 2019 at 22:45):

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

Kenny Lau (Feb 17 2019 at 22:46):

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

Mario Carneiro (Feb 17 2019 at 22:47):

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

Mario Carneiro (Feb 17 2019 at 22:48):

the point is it's a tree

Kenny Lau (Feb 17 2019 at 22:49):

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

Kenny Lau (Feb 17 2019 at 22:49):

what is a * a^-1?

Mario Carneiro (Feb 17 2019 at 22:49):

1

Kenny Lau (Feb 17 2019 at 22:49):

yeah but will it be computable?

Mario Carneiro (Feb 17 2019 at 22:49):

I didn't say anything about computability

Mario Carneiro (Feb 17 2019 at 22:50):

but in this case yes you can do it

Mario Carneiro (Feb 17 2019 at 22:50):

if A has decidable eq

Kenny Lau (Feb 17 2019 at 22:50):

yeah that's the problem

Kenny Lau (Feb 17 2019 at 22:50):

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

Mario Carneiro (Feb 17 2019 at 22:50):

It's easy to prove that it's necessary

Kenny Lau (Feb 17 2019 at 22:50):

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

Mario Carneiro (Feb 17 2019 at 22:51):

No, with any construction

Kenny Lau (Feb 17 2019 at 22:51):

the construction in mathlib doesn't need decidable equality

Mario Carneiro (Feb 17 2019 at 22:51):

If it's not a quotient

Kenny Lau (Feb 17 2019 at 22:51):

define "not a quotient"

Mario Carneiro (Feb 17 2019 at 22:51):

using only inductive types

Mario Carneiro (Feb 17 2019 at 22:52):

like the sort you've been talking about

Kenny Lau (Feb 17 2019 at 22:52):

could you prove it?

Mario Carneiro (Feb 17 2019 at 22:53):

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

Kenny Lau (Feb 17 2019 at 22:54):

seems very fishy to me

Kenny Lau (Feb 17 2019 at 22:54):

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

Mario Carneiro (Feb 17 2019 at 22:55):

1 has to be obtained by applying some constructors

Kenny Lau (Feb 17 2019 at 22:56):

interesting

Mario Carneiro (Feb 17 2019 at 22:56):

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

Mario Carneiro (Feb 17 2019 at 22:58):

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

Kenny Lau (Feb 17 2019 at 22:58):

thanks

Reid Barton (Feb 17 2019 at 23:09):

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 (Feb 17 2019 at 23:10):

nice

Reid Barton (Feb 17 2019 at 23:12):

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

Kenny Lau (Feb 17 2019 at 23:14):

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 (Feb 17 2019 at 23:20):

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

Mario Carneiro (Feb 17 2019 at 23:22):

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

Mario Carneiro (Feb 17 2019 at 23:23):

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

Mario Carneiro (Feb 17 2019 at 23:23):

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

Mario Carneiro (Feb 17 2019 at 23:23):

but not field, because there is a disequality

Mario Carneiro (Feb 17 2019 at 23:23):

that's why there is no free field

Reid Barton (Feb 17 2019 at 23:24):

"variety of algebras" but related terms will inevitably collide

Mario Carneiro (Feb 17 2019 at 23:24):

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 (Feb 17 2019 at 23:29):

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 (Feb 17 2019 at 23:30):

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

Mario Carneiro (Feb 17 2019 at 23:31):

(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 (Feb 18 2019 at 14:18):

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 (Feb 18 2019 at 14:48):

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

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

Simon Hudon (Feb 18 2019 at 16:16):

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

Are those tears of pride?

Kevin Buzzard (Feb 18 2019 at 16:34):

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 (Feb 27 2019 at 02:18):

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


Last updated: Dec 20 2023 at 11:08 UTC