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.

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

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 isbundle and_or_xor_syntax

beginno_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 ==> a*b=b*a

…

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.

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

Hi Peter,

bundle and_or_xor_syntax

beginno_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

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.

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_wordIn 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: Jan 25 2022 at 01:11 UTC