Email Gateway (Dec 09 2021 at 10:26): Email Gateway (Dec 09 2021 at 10:26):From: Florian Sextl <sextl@in.tum.de>
Dear all,
I am currently formalizing the base logic of the Iris separation logic
framework in Isabelle and found that some theoretic constructs can be
expressed quite well as semantic subtypes (mostly some specialized
function types). After reading about how to work with subtypes, quotient
types and the lifting/transfer packages as well as experimenting with a
few simple logical extensions to the base logic I am a bit unsure,
whether it would be easier to express the subtype semantics as simple
predicates over the raw type.
My use cases for subtpyes are on the one hand for defining the assertion
language and on the other hand for the underlying generic structure (so
called cameras).
I found that subtypes and lifting seem to be a rather standard technique
for formalizing assertions (e.g. the separation logic of Imperativ HOL
uses them). Yet, this approach requires to also lift many lemmas
necessary for a good automation. This might be even worse than for
Imperative HOL as the Iris assertions contain more custom connectives.
The subtype in question can be found at [1] and a "paper formalization"
of the assertion language can be found at [2] in section 5.
The other use case might be similar to some mathematical constructions.
I defined the camera structure as a type class which requires functions
that are of a specific subtype, see [3]. In this case, the lifting and
lowering seems to only decrease the readability without providing better
usability.
I'd love to hear some opinions on whether these use cases make sense for
semantic subtypes with lifting or whether the necessary overhead could
be too much in the long run. On a related note, what are the experiences
of others with semantic subtpyes and are there any good rules of thumb
for when to use them?
Thanks a lot in advance and sorry for the horrific WIP proofs in other
parts of the work.
smime.p7s
Email Gateway (Dec 09 2021 at 11:33):From: Peter Lammich <lammich@in.tum.de>
Hi Florian,
I agree with your observation that, when using subtypes, a lot of
boilerplate can be generated by having to transfer all necessary
concepts from the base-type. There are two exterme approaches here
(that, of course, can be combined):
1) try to be minimalistic, only lift/transfer the very basic facts, and
prove everything else without breaking the subtype barrier again.
2) prove everything on the rep-type, and then lift/transfer everything.
while 1 definitely causes less boilerplate, setting up automation when
the automation for the rep-type is already well established (like for
sets) can be a pain. On the other hand, for things like separation
logic, there usually is a not-too-big set of basic rules, from which
you can derive the others. This can even be done generically, using
type-classes like in
https://www.isa-afp.org/entries/Separation_Algebra.html (and a few
extensions of that here:
https://www21.in.tum.de/~lammich/isabelle_llvm/Isabelle_LLVM/Sep_Algebra_Add.html
)
Moreover, 1) has the advantage that one gains a better understanding of
the logic one is formalizing, basically finding a minimal (small)
complete set of rules, rather than producing ad-hoc rules from the
underlying rep-type.
Finally, considering the alternative of not using subtypes at all, but
keeping the invariants in predicates: while this may seem to be easier
for proving/developing in an early stage, as it reduces lift/transfer
boilerplate in particular at an early stage of the development,
rules with explicit invariants are much harder to use. So you are
pushing technical debt to later stages of the development, when you
start to use your own rules more frequently.
Thus, while an explicit invariant approach might be the way to get
started quickly and with less overhead (which gives you more
flexibility to play around and try things), at some point you want to
transition to subtypes (ideally when you have your small complete set
of rules). Of course, you can lift/transfer the concepts at this stage
at only boilerplate cost, keeping the initial development intact.
Last updated: Jul 15 2022 at 23:21 UTC