Théo Zimmermann (Jun 24 2020 at 11:20): Théo Zimmermann (Jun 24 2020 at 11:20):This is the topic to ask questions on the talk "Developing sequence and tree fintypes in MathComp".
Cyril Cohen (Jul 06 2020 at 08:45):Are you aware of the type tree here https://github.com/math-comp/math-comp/blob/e71aecf4fbb829accba495e2e7cdba1a1ddc836a/mathcomp/ssreflect/choice.v#L156 ?
Inductive tree := Leaf of T | Node of nat & seq tree.
@Cyril, can you make the question more self-contained (explain the link)?
Cyril Cohen (Jul 06 2020 at 08:47):Yves Bertot said:
@Cyril, can you make the question more self-contained (explain the link)?
I am pointing to the definition of tree finType in mathcomp.
Enrico Tassi (Jul 06 2020 at 08:48):This would be the doc of that tree: https://github.com/math-comp/math-comp/blob/e71aecf4fbb829accba495e2e7cdba1a1ddc836a/mathcomp/ssreflect/choice.v#L40-L46
(* GenTree.tree T == generic n-ary tree type with nat-labeled nodes and *)
(* T-labeled leaves, for example GenTree.Leaf (x : T), *)
(* GenTree.Node 5 [:: t; t']. GenTree.tree is equipped *)
(* with canonical eqType, choiceType, and countType *)
(* instances, and so simple datatypes can be similarly *)
(* equipped by encoding into GenTree.tree and using *)
(* the mixins above. *)
@Cyril Cohen the doc does not talk about finiteness
Cyril Cohen (Jul 06 2020 at 08:52):Enrico Tassi said:
Cyril Cohen the doc does not talk about finiteness
Ah true, it handles choice and count but not finite, my mistake...
Cyril Cohen (Jul 06 2020 at 08:52):I am thinking It could be extended in the same way as tuples...
Enrico Tassi (Jul 06 2020 at 08:53):Agree, maybe you should formulate that as a question/suggestion for Yves to read ;-)
Reynald Affeldt (Jul 06 2020 at 08:57):We needed trees with bounded degree when developing error-correcting codes (https://github.com/affeldt-aist/infotheo/blob/master/ecc_modern/degree_profile.v#L212-L215)
Cyril Cohen (Jul 06 2020 at 08:57):OK I have a suggestion rather than a question: in the same way Blist would be easier defined as a sub type, {s | size s <= n}, the current tree implementation could be generalized to have an arbitrary datatype for nodes and have Btree be {t | width t w} where w : A -> nat gives the arity of each node.
Reynald Affeldt (Jul 06 2020 at 08:58):(bounded trees were important to be able to take about finite sets of trees)
Reynald Affeldt (Jul 06 2020 at 09:00):the height is bounded with a dependent type
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:00):Wouldn't blist just 'I_n.-tuple A ?
Reynald Affeldt (Jul 06 2020 at 09:00):so it is both bounded in height and in degree
Cyril Cohen (Jul 06 2020 at 09:00):Emilio Jesús Gallego Arias said:
Wouldn't blist just
'I_n.-tuple A?
because it's an inequality of size (not an equality)
Christian Doczkal (Jul 06 2020 at 09:01):I needed length bounded lists at some point and I {s : seq T | size s < n} naturally injects into {'I_n & n.-tuple A}, which is finite by construction.
Cyril Cohen (Jul 06 2020 at 09:01):Cyril Cohen said:
OK I have a suggestion rather than a question: in the same way
Blistwould be easier defined as a sub type,{s | size s <= n}, the current tree implementation could be generalized to have an arbitrary datatype for nodes and haveBtreebe{t | width t w}wherew : A -> natgives the arity of each node.
@Pierre-Léo Bégay did you see my suggestion?
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:01):Not a question, but a comment, but I guess the way I'd go proving finitiness of the tree is to have the bound be itself a tree of the corresponding ordinals
Reynald Affeldt (Jul 06 2020 at 09:02):we also needed a type such as {s | size s <= n} to represent codewords (so my point is that such datatypes are useful for error-correcting code in particular)
Cyril Cohen (Jul 06 2020 at 09:05):I think @affeldt-aist using a dependent type in the signature could be done using a finfun nowadays.
Pierre-Léo Bégay (Jul 06 2020 at 09:07):Cyril Cohen said:
OK I have a suggestion rather than a question: in the same way
Blistwould be easier defined as a sub type,{s | size s <= n}, the current tree implementation could be generalized to have an arbitrary datatype for nodes and haveBtreebe{t | width t w}wherew : A -> natgives the arity of each node.
1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.
2) That's obviously a better way to defined Btrees. However, as "quick'n dirty" as it sounds, we really just needed a clearly finite tree type to use as a support to the more interesting type Utree.
Cyril Cohen (Jul 06 2020 at 09:08):Can you share a pointer to your source code. I already forgot the definition of Utree
Pierre-Léo Bégay (Jul 06 2020 at 09:08):affeldt-aist said:
(bounded trees were important to be able to take about finite sets of trees)
Yes, for us also! (the semantics of Datalog is defined as a set of facts, so we wanted to defined the trace semantics as a set of traces)
Reynald Affeldt (Jul 06 2020 at 09:11):To be more precise, our application is a theorem about some class of error-correcting codes (see Sect. VI of https://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf)
Pierre-Léo Bégay (Jul 06 2020 at 09:11):Emilio Jesús Gallego Arias said:
Not a question, but a comment, but I guess the way I'd go proving finitiness of the tree is to have the bound be itself a tree of the corresponding ordinals
I'm not sure I get what you mean, you mean a tree of 'I_n where n is the maximal degree? How is that finite?
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):The bound can be a choiceType tree itself
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):then the bound implies finiteness by induction
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):I think
Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):just an idea
Christian Doczkal (Jul 06 2020 at 09:13):Pierre-Léo Bégay said:
1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.
I ran into this a while ago, one can use pickle/unpickle to encode the type at hand into the fixed node type.
Pierre-Léo Bégay (Jul 06 2020 at 09:13):Cyril Cohen said:
Can you share a pointer to your source code. I already forgot the definition of
Utree
It's not online yet (and there are legal issues (thèse CIFRE)), but I can send you the sources.
Pierre-Léo Bégay (Jul 06 2020 at 09:16):Christian Doczkal said:
Pierre-Léo Bégay said:
1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.
I ran into this a while ago, one can use
pickle/unpickleto encode the type at hand into the fixed node type.
Yup, I realized that when writing my message, I was unfortunately unaware of this at the time. But it feels weird to have to rely on this rather than just be able to simply use any choiceType. Even considering this option, I'm not sure if putting nat as the node type of tree was a design decision.
Pierre-Léo Bégay (Jul 06 2020 at 09:18):affeldt-aist said:
To be more precise, our application is a theorem about some class of error-correcting codes (see Sect. VI of https://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf)
It somehow feels great too hear that we were not the only ones missing such a structure, and that it was used for something so different from what we have done, thanks for the pointer, I'll look into that more closely later!
Cyril Cohen (Jul 06 2020 at 09:26):Pierre-Léo Bégay said:
Christian Doczkal said:
Pierre-Léo Bégay said:
1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.
I ran into this a while ago, one can use
pickle/unpickleto encode the type at hand into the fixed node type.Yup, I realized that when writing my message, I was unfortunately unaware of this at the time. But it feels weird to have to rely on this rather than just be able to simply use any choiceType. Even considering this option, I'm not sure if putting nat as the node type of tree was a design decision.
The initial (and only current real use) of tree is to encode other datatypes to show eqType, countType, choiceType, etc
Christian Doczkal (Jul 06 2020 at 09:27):Yes, I just checked my own (old) code and indeed I only use the "nat" part for enumerating constructors. But my syntax does not carry data on internal nodes, some other syntaxes may.
Pierre-Léo Bégay (Jul 06 2020 at 09:29):@Cyril Cohen , I just sent you the code via email.
Pierre-Léo Bégay (Jul 06 2020 at 09:30):Cyril Cohen said:
The initial (and only current real use) of
treeis to encode other datatypes to show eqType, countType, choiceType, etc
Ok, that makes more sense in that case, thanks.
Cyril Cohen (Jul 06 2020 at 09:33):Pierre-Léo Bégay said:
Cyril Cohen , I just sent you the code via email.
OK, I will take a look later
Pierre-Léo Bégay (Jul 06 2020 at 09:33):Emilio Jesús Gallego Arias said:
just an idea
Ok, I think I see what you mean, it looks more intricate than what I would come up with myself, thanks for the feedback!
Last updated: Jun 01 2023 at 11:01 UTC