Re: [isabelle] Remarks on the further development work of "Types-To-Sets"



Dear René Thiemann,

I believe that, once again, I left your very useful remark without a
comment - please accept my sincere apologies. Unfortunately, both times,
your remarks were submitted to the mailing list after I nearly abandoned
the threads and, somehow, were left unnoticed in my inbox. Therefore, I did
not get a chance to explicitly thank you for providing the references to
your articles in one of your previous replies to one of my threads about
Types-To-Sets. Most certainly, I appreciate all the help that I receive
from the users of the mailing list and I strive to give appropriate
attribution.

However, my claims with regard to the relativisation of constants may have
been slightly misleading. It is rather unlikely that I will provide a
framework for the completely automated relativisation of all specification
elements that exist in Isabelle before attempting to submit the extension
of Types-To-Sets to the AFP. The scope of the planned work includes
synthesizing the specification of the relativized constants for definitions
and merely synthesizing the statements of the parametricity relations for
all specification elements, not, necessarily, proving them. I believe that
these improvements will be much more beneficial to the new users, rather
than those who are already familiar with the framework.

Thank you

On Thu, Jun 27, 2019 at 9:41 AM Thiemann, René <Rene.Thiemann at uibk.ac.at>
wrote:

> Dear anonymous,
>
> > 1). As I mentioned in my original post, I have every intention to
> provide a
> > framework for the relativization of constants. My goal is to develop a
> > command that, given a constant, would automatically generate its
> > unoverloaded counterpart, its relativization and provide a parametricity
> > relation for the unoverloaded constant and the relativization. You have
> > already automated the process of unoverloading constants and the
> functions
> > developed for the command tts_relativize should do most of the work
> > associated with the relativization. Conservatively, I expect to make this
> > functionality available publicly before the end of July. At this stage, I
> > will probably need to spend another month on software engineering,
> > refinement and documentation.
> > I believe that once the relativization of constants is automated, the
> > framework will become user-friendly: it will not require almost any
> > knowledge of the algorithm for the vast majority of the routine
> > relativization tasks. Of course, there will always remain certain
> > borderline cases that will require more advanced knowledge, but this can
> be
> > said about almost every software. The important subjective aspect is that
> > one will not need to know almost anything about Isabelle/HOL to 'try out'
> > Types-To-Sets on simple definitions/theorems. Then, once the first steps
> > are made, given a sufficient amount of examples and documentation, the
> user
> > can continuously educate himself/herself towards achieving the mastery of
> > the framework.
>
>
> from my side, such a command is highly welcome, having defined several
> unoverloaded
> constants manually and proved the transfer-relations in easy but tedious
> proofs.
>
> So, I’m looking forward to see your finalized work in the AFP, where
> afterwards
> I can try to get rid of my manual definitions and proofs. If you’re
> interested, I
> might also be able to test your infrastructure before submission.
>
> With best regard,
> René
>
>

-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.