I recently wanted to understand the Parquet binary format so I attempted to write a specification for it in Kaitai Struct. Kaitai Struct is a declarative binary format specification language, embedded in YAML. After writing such specification for a format one can generate parsers for it in several supported languages. Another thing that one can use such specification for is to visualize various elements of the format in the Kaitai Web IDE, which shows output somewhat similar to what Wireshark shows for network protocols. That’s what I want to use (if I ever finish the spec).
One stumbling block that I encountered was related to the way a SchemaElement is encoded in Parquet. A SchemaElement is a struct with a couple of fields selected from a fixed collection. The fields have numerical identifiers which are not provided directly but through deltas between their values. To obtain actual field id one has to compute the sum of the deltas provided (as 4-bit integers) in the file. For a while it was unclear if there is a way to encode such sum in Kaitai Struct and there was an issue about it on Kaitai GitHub repository opened more that four years ago. However, some three weeks ago cher-nov came up with a solution to this problem and posted it to the issue linked above. In this post I want to present an application of this solution to a toy format as another example that one can look at.
Read the rest of this entry »
is a family of uniform covers of 
then the following collection 
of subsets of 
is a (diagonal) uniformity:
. 
.
. A collection 
of subsets of 
. 
and a collection of 
of subsets of 
in 
.
we say that the cover 
is a star-refinement of the cover 
and write 
if for every 
we can find a 
such that 
is contained in 
.
, 
and 
we can find a cover 
that is a star-refinement of both 
is a member of 
.
as 
one needs to find a set 
such that 
(here 
is the composition of relation 
with itself). For that, I found the following identity useful:
if and only if 
and 
. The “if and only if” is worth noting here as this is different from the ordered group definition where one-sided implications are sufficient (I lost a couple of hours working with a wrong definition). 
, then we can define the left and right inverses of a loop element 
as the only solutions to the equations 
and 
. In a loop these inverses do not have to be the same in general. If the loop operation is associative then we get a group and the left and right inverses unify to become the group inverse.
or 
has a unique solution. So, a quasigroup is like a group except we do not require associativity or existence of a neutral element. If we denote those solution as 
and 
respectively we get the identities 
and 
by definition and, with the uniqueness, we get 
and 
, which may serve as an alternative definition of quasigroup. 
being a metric and one stating that the collection of unions of open disks is a topology on reals.
and 
, very important in mathematics based on set theory) were replaced by some placeholder symbol. Errors related to LaTeX are difficult to debug in Isabelle (at least for me), but this time I was lucky. The Isabelle2021 release notes contained information that the “The standard LaTeX engine is now lualatex, according to settings
that satisfies the conditions 
, 
and 
for all 
. This is sufficient to prove that the collection of subsets of 
) is a topology, making this metric space a topological space. If we replace the interval 
in the definition of pseudo-metric by the nonnegative set of a linearly ordered, abelian, Archimedean group then we are not changing anything as such group is isomorphic to a subgroup of the additive group of real numbers. I was curious: what is really needed to get a topological space from a pseudo-metric space this way? Do we really need the group to be Archimedean? Does the group operation have to be commutative? Do we need the order to be total? Amusingly, the answer to these questions is “no”. The group does not have to be abelian and the Archimedean property is not needed. The linear order condition can be relaxed by assuming that the positive set is a meet semi-lattice (every two-element subset has a greatest lower bound) under the group order relation. I don’t know if this is useful to know, but surely my personal curiosity got satisfied.
the set 
is also a subgroup. These theorems turned out not to be in the Mizar Mathematical Library, but Roland Coghetto posted formalization of those 
Formalized Mathematics 