This is the topic to ask questions on the talk "Developing sequence and tree fintypes in MathComp".

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)?

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.

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

Enrico Tassi said:

Cyril Cohen the doc does not talk about finiteness

Ah true, it handles choice and count but not finite, my mistake...

I am thinking It could be extended in the same way as tuples...

Agree, maybe you should formulate that as a question/suggestion for Yves to read ;-)

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)

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.

(bounded trees were important to be able to take about finite sets of trees)

the height is bounded with a dependent type

Wouldn't blist just `'I_n.-tuple A`

?

so it is both bounded in height and in degree

Emilio Jesús Gallego Arias said:

Wouldn't blist just

`'I_n.-tuple A`

?

because it's an inequality of size (not an equality)

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 said:

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.

@Pierre-Léo Bégay did you see my suggestion?

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

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)

I think @affeldt-aist using a dependent type in the signature could be done using a finfun nowadays.

Cyril Cohen said:

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.

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.

Can you share a pointer to your source code. I already forgot the definition of `Utree`

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)

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)

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?

The bound can be a choiceType tree itself

then the bound implies finiteness by induction

I think

just an idea

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.

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.

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`

/`unpickle`

to 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.

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!

Pierre-Léo Bégay said:

Christian Doczkal said:

Pierre-Léo Bégay said:

I ran into this a while ago, one can use

`pickle`

/`unpickle`

to 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

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.

@Cyril Cohen , I just sent you the code via email.

Cyril Cohen said:

The initial (and only current real use) of

`tree`

is to encode other datatypes to show eqType, countType, choiceType, etc

Ok, that makes more sense in that case, thanks.

Pierre-Léo Bégay said:

Cyril Cohen , I just sent you the code via email.

OK, I will take a look later

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