Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Fixed-Length Vectors

view this post on Zulip Email Gateway (Aug 20 2023 at 08:16):

From: Dmitriy Traytel <traytel@di.ku.dk>
Greetings from a new AFP editor.

Here is another small new entry, by Lars Hupel, titled Fixed-Length Vectors with the following abstract:

This theory introduces a type constructor for lists with known length, also known as "vectors". Those vectors are indexed with a numeral type that represent their length. This can be employed to avoid carrying around length constraints on lists. Instead, those constraints are discharged by the type checker. As compared to the vectors defined in the distribution, this definition can easily work with unit vectors. We exploit the fact that the cardinality of an infinite type is defined to be 0: thus any infinite length index type represents a unit vector. Furthermore, we set up automation and BNF support.

You can find the entry here: https://www.isa-afp.org/entries/Fixed_Length_Vector.html

Having BNF support means that the new type is ready for usage in (co)datatypes (with nested recursion through the vector).

Enjoy!
Dmitriy

view this post on Zulip Email Gateway (Aug 20 2023 at 08:43):

From: Gergely Buday <cl-isabelle-users@lists.cam.ac.uk>
How is this different from dependently typed vectors where you give the
length bv a number? Is it more difficult to handle this, based on a numeral
type?

Dmitriy Traytel <traytel@di.ku.dk> ezt írta (időpont: 2023. aug. 20., Vas
9:16):

view this post on Zulip Email Gateway (Aug 21 2023 at 07:53):

From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Gergely,

That’s an interesting question. I guess you can find an experience report on the usability of vector types in John Harrison’s TPHOLs 2005 paper (https://www.cl.cam.ac.uk/~jrh13/papers/hol05.html), which introduced the numeral trick AFAIK. Harrison’s vector type exists in HOL-Analysis. The below entry introduces a variant that supports the unit vector (of length 0) and is integrated with datatypes via the BNF infrastructure, i.e., allows you to define funnily shaped trees such as:

datatype 'a tree = Leaf 'a | Node "'a tree ^ 42"

Best wishes,
Dmitriy

Last updated: Jan 04 2025 at 20:18 UTC