Zulip Chat Archive

Stream: new members

Topic: clone formalization


view this post on Zulip Miroslav Olšák (Oct 23 2018 at 10:57):

Hello everybody, we tried a testing formalization of a simple proposition about clones in several ITP's for comparison. LEAN seems pretty nice so far. However, I believe that there should be a better approach to certain parts the proof (if we just knew LEAN better).
You can see the task description, together with my complains (/ TODO) under the link.
http://atrey.karlin.mff.cuni.cz/~mirecek/formal-math/clones.lean

view this post on Zulip Johan Commelin (Oct 23 2018 at 11:28):

@Miroslav Olšák I'm having trouble with certain symbols. I think unicode is being messed up or something. Could you post your code again with correct encoding? Maybe as a Github Gist, or something... (Don't know if you use github...)

view this post on Zulip Bryan Gin-ge Chen (Oct 23 2018 at 12:53):

In Firefox you can set the text encoding manually to unicode (View... Text Encoding...) and then the page displays properly. Apparently that feature no longer exists in Chrome.

view this post on Zulip Miroslav Olšák (Oct 23 2018 at 18:43):

All right, there it is on GitHub:
https://github.com/mirefek/clones-lean/blob/master/clones.lean
Any suggestions to the code? Is there a better way for case analysis through fin 3? Or a tactic that can do all the rewrite at the end of the code?

view this post on Zulip Mario Carneiro (Oct 23 2018 at 18:45):

I think you should use ternary functions rather than arrays

view this post on Zulip Mario Carneiro (Oct 23 2018 at 18:46):

or products, but curried will be nicer

view this post on Zulip Miroslav Olšák (Oct 23 2018 at 19:15):

I think you should use ternary functions rather than arrays

Definitely not. Sure, it suffices for this simple example but it does not correspond to the definition of clone at all.

view this post on Zulip Miroslav Olšák (Oct 23 2018 at 19:16):

or products, but curried will be nicer

Show me.

view this post on Zulip Miroslav Olšák (Oct 23 2018 at 19:27):

@Mario Carneiro What do you mean by curried products?

view this post on Zulip Johan Commelin (Oct 23 2018 at 19:29):

You can write a function X × Y → Z as X → Y → Z.

view this post on Zulip Johan Commelin (Oct 23 2018 at 19:29):

This is known as "currying"

view this post on Zulip Kenny Lau (Oct 23 2018 at 19:29):

aka product is left-adjoint of hom

view this post on Zulip Kenny Lau (Oct 23 2018 at 19:30):

(sorry)

view this post on Zulip Miroslav Olšák (Oct 23 2018 at 19:33):

I see.
But how to define the general composition for operations written like this?
I really think it is better to interpret them as functions A^n -> A, in the case of clones, as mathematicians usually do.

view this post on Zulip Johan Commelin (Oct 23 2018 at 19:34):

I tend to agree (I'm also a mathematician). But these CS people have really crazy operators that will do what you want.

view this post on Zulip Johan Commelin (Oct 23 2018 at 19:35):

And they can explain the benefits. (The disadvantage is that it no longer looks like what you are used to, although you can prove it is the same thing.)

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 23 2018 at 19:35):

I guess the advantage of the CS approach is that you can just give a single input and get a function.

view this post on Zulip Johan Commelin (Oct 23 2018 at 19:36):

I don't know what a clone is exactly, but what I saw on wiki looks like it is related operads. @Miroslav Olšák Is that right?

view this post on Zulip Reid Barton (Oct 23 2018 at 19:46):

nlab claims clones are analogous to operads but I think the relationship is less obvious than it looks at first glance

view this post on Zulip Reid Barton (Oct 23 2018 at 19:46):

The composition operation for operads takes a kk-ary operation and kk operations of arity n1n_1, ..., nkn_k and gives you an operation of arity n1++nkn_1 + \cdots + n_k

view this post on Zulip Reid Barton (Oct 23 2018 at 19:47):

where the picture is that the kk operations each have access to disjoint subsets of the input variables

view this post on Zulip Reid Barton (Oct 23 2018 at 19:48):

here, each of the composed operations has access to all the input variables. I guess maybe it is the same thing as saying that you have the power to duplicate variables.

view this post on Zulip Miroslav Olšák (Oct 23 2018 at 19:49):

I understand the advantages of functional programming, but not in this case. If anybody feels that defining a clone by curried functions would be better, it would be nice to see such an approach.

Concerning to operads, I don't know them very well. From what I see on Wiki right now, operads are more general than abstract clones since they does not have projections (and also, operads don't glue variables). I think Reid Barton is right, just faster than me :-)

view this post on Zulip Mario Carneiro (Oct 24 2018 at 03:44):

The fact that you can partially apply a curried function is not actually that important in this case, it's just the way lean naturally deals with n-ary functions

view this post on Zulip Mario Carneiro (Oct 24 2018 at 03:57):

@Miroslav Olšák Okay, I see now. I thought that you only had to deal with ternary functions, but now I see that the statement involves membership in a clone, which involves arbitrary arity functions

view this post on Zulip Mario Carneiro (Oct 24 2018 at 03:59):

In this case, I will point you to nat.primrec', which is somewhat similar in needing to deal with collections of n-ary functions and n-ary composition. I use functions of type vector n A -> A, and n-ary composition is λ a, f (of_fn (λ i, g i a))

view this post on Zulip Miroslav Olšák (Oct 24 2018 at 09:14):

Interesting. Do you think that vectors behave in Lean better than arrays in general? (even though they are mathematically the same).


Last updated: May 08 2021 at 19:11 UTC