Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] RC5: Syntactic class bit_operations is gone


view this post on Zulip Email Gateway (Feb 12 2021 at 13:52):

From: Peter Lammich <lammich@in.tum.de>
Hi List.

In 2020, there used to be a purely syntactic class for bitwise
operations:

HOL/Word/Bits.bit_operations

This class is gone in RC5, and the closest match seems to be the class
semiring_bit_operations in Library/Bit_Operations.thy, but this has
axioms.

This new class binds the infix syntax for (AND), (OR), (XOR) to these
axioms.

I thought it would be standard to define syntactic type classes for
infix syntax first, and then add the axioms.

In my application, I cannot use the semiring_bit_operations class, as I
cannot define a mask function. However, I'd like to use the convenient
syntax, which is now somewhat blocked.

view this post on Zulip Email Gateway (Feb 12 2021 at 20:17):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

In 2020, there used to be a purely syntactic class for bitwise
operations:

HOL/Word/Bits.bit_operations

This class is gone in RC5, and the closest match seems to be the class
semiring_bit_operations in Library/Bit_Operations.thy, but this has
axioms.

This new class binds the infix syntax for (AND), (OR), (XOR) to these
axioms.

In my application, I cannot use the semiring_bit_operations class, as I
cannot define a mask function. However, I'd like to use the convenient
syntax, which is now somewhat blocked.

With Isabelle2021 you will be able to mixin bundles at every logically
relevant position, so the canonical solution for re-using mixfix syntax is

bundle and_or_xor_syntax
begin

no_notation "and" …
notation "and" …

end

Beyond that, what is your particular instance such that a mask operation
would not be definable?

I thought it would be standard to define syntactic type classes for
infix syntax first, and then add the axioms.

No. In ancient times this was the only possibility, and hence there are
many syntactic type classes in HOL like plus, minus, times etc.

Sometimes they are necessary to accomplish a particular hierarchy, AFAIR
for gcd, lcm etc.

Syntax type classes typically forces many manual type constraints. You
can see the traces e.g. in the upcoming AFP, entry Word_Lib, theory
Word_Syntax.thy

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Feb 12 2021 at 20:43):

From: Peter Lammich <lammich@in.tum.de>
Hi Florian,

thanks for the response and pointers to the AFP word developments.

With Isabelle2021 you will be able to mixin bundles at every
logically
relevant position, so the canonical solution for re-using mixfix
syntax is

bundle and_or_xor_syntax
begin

no_notation "and" …
notation "and" …

So this will effectively build a linear stack that puts the syntax in
order. Such a bundle will only work if the conflicting theory that
fixes the syntax in the typeclass is also loaded.

Another point against bundles is, that some notations like + or * are
overloaded many times, with different axioms holding on them.
For example, in our separation logic for IMP/HOL, we use * as
separating conjunction, that only fulfills the axioms when the two
operators are, additionally, disjoint, e.g.: a##b ==> ab=ba

end

Beyond that, what is your particular instance such that a mask
operation
would not be definable?

My llvm formalization uses words of variable but fixed bit-length.
I have the operation width :: ll_word => nat, that gives the width, and
operations are only defined between words of the same width ... but
this is deeply embedded, rather than shallowly in the type system, such
that I can store those words in my deeply embedded LLVM value model.

I had instantiated all the syntactic word classes, but now, I cannot
define mask :: nat => ll_word, as it would have to 'guess' a width.
Also, I doubt that the axioms hold unconditionally.

view this post on Zulip Email Gateway (Feb 13 2021 at 09:19):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

bundle and_or_xor_syntax
begin

no_notation "and" …
notation "and" …

So this will effectively build a linear stack that puts the syntax in
order. Such a bundle will only work if the conflicting theory that
fixes the syntax in the typeclass is also loaded.

I don't get this point. What is the »conflicting theory«?

Another point against bundles is, that some notations like + or * are
overloaded many times, with different axioms holding on them.
For example, in our separation logic for IMP/HOL, we use * as
separating conjunction, that only fulfills the axioms when the two
operators are, additionally, disjoint, e.g.: a##b ==> ab=ba

That's a different story. I definitely don't argue to eliminate the
traditional syntactic type classes from HOL.

My llvm formalization uses words of variable but fixed bit-length.
I have the operation width :: ll_word => nat, that gives the width, and
operations are only defined between words of the same width ... but
this is deeply embedded, rather than shallowly in the type system, such
that I can store those words in my deeply embedded LLVM value model.

I had instantiated all the syntactic word classes, but now, I cannot
define mask :: nat => ll_word, as it would have to 'guess' a width.
Also, I doubt that the axioms hold unconditionally.

Note that mask is logically a plain definition in this type class (see
the Guide.thy in AFP session Word_Lib for the rationale behind). So, it
might be sufficient for a formal definition without a semantic
meaningful content.

But the main issue seems to me indeed the quasi-partiality of AND OR
XOR. I don't see a way to make this compatible to the class specification.

So, the bundle seems the way to go for now. Since there is some
rationale to put the most important bit operations into HOL-Main, I once
thought to organize all infix syntax on bits in bundles anyway, to not
clutter the syntactic space of HOL-Main. If this is once accomplished
after the release, the infix syntax is completely free.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Feb 13 2021 at 09:38):

From: Peter Lammich <lammich@in.tum.de>

order. Such a bundle will only work if the conflicting theory that

fixes the syntax in the typeclass is also loaded.

I don't get this point. What is the »conflicting theory«?

A theory that defines a bundle for its syntax, starting with
no_notation ... to erase potential conflicting syntax, automatically
depends on the theory declaring the conflicting syntax, even if they
are logically independent. Otherwise, the user will be responsible to
do such a declaration at the merge point of two theories declaring
conflicting syntax.

So, the bundle seems the way to go for now. Since there is some
rationale to put the most important bit operations into HOL-Main, I
once
thought to organize all infix syntax on bits in bundles anyway, to
not
clutter the syntactic space of HOL-Main. If this is once
accomplished
after the release, the infix syntax is completely free.

Also, the bundling approach prevents you from using the same syntax for
the two related concepts, e.g., I can no longer write the statement:

width a = width b ==> int_of (a AND b) = int_of a AND int_of b
for a b :: ll_word

In my solution, I now went for introducing a similar looking syntax,
i.e., a llAND b. But this approach will lead to cluttering the syntax
space with many variations of the same syntax, just b/c you cannot
share it where it would feel natural to share.

It seems like there is no fits-everything solution to this question
yet.

view this post on Zulip Email Gateway (Feb 25 2021 at 16:40):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,

A theory that defines a bundle for its syntax, starting with
no_notation ... to erase potential conflicting syntax, automatically
depends on the theory declaring the conflicting syntax, even if they
are logically independent. Otherwise, the user will be responsible to
do such a declaration at the merge point of two theories declaring
conflicting syntax.

I don't see that point. The syntax woule be totally organized in
bundles and hence there are no conflicts at theory merges.

So, the bundle seems the way to go for now. Since there is some
rationale to put the most important bit operations into HOL-Main, I
once
thought to organize all infix syntax on bits in bundles anyway, to
not
clutter the syntactic space of HOL-Main. If this is once
accomplished
after the release, the infix syntax is completely free.

Also, the bundling approach prevents you from using the same syntax for
the two related concepts, e.g., I can no longer write the statement:

width a = width b ==> int_of (a AND b) = int_of a AND int_of b
for a b :: ll_word

In my solution, I now went for introducing a similar looking syntax,
i.e., a llAND b. But this approach will lead to cluttering the syntax
space with many variations of the same syntax, just b/c you cannot
share it where it would feel natural to share.

It seems like there is no fits-everything solution to this question
yet.

Ok, now I understand that these operations are inherently partial and
hence there are no unguarded properties.

In the current state of affairs most lemmas

"… AND … OR … XOR … = …"

are valid without any type annotation due to the algebraic foundation
of the underlying type class. This should eliminate the felt need for
yet another infix syntax for word types only as seen in
Word_Lib/Word_Syntax.thy (which, by the way, is not found in typical
programming languages). Hence I want to maintain that.

A compromise could be to have a syntactic class but by default a
stronger constraint. I will investigate that in the future.

Cheers,
Florian
signature.asc


Last updated: Dec 05 2021 at 22:18 UTC