Re: [isabelle] Quotients of nominal types



Hi Alex, 

On Wednesday, August 7, 2013 at 11:58:18 (+0100), Aleks Kissinger wrote:
 > 
 > 1. Forming a nominal_datatype and taking a quotient. This seems like
 > the obvious choice, but I have a few questions about it. Firstly, in
 > Nominal2, a nominal_datatype is already a quotient. Is this
 > quotient-of-a-quotient setup going to be a pain? If not, what things
 > need to be lifted to the quotient type in order to keep working modulo
 > alpha-equivalence as automatic as possible?

There should be no problem with using quotients of nominal datatypes.
One problem however is that you would have to list/transfer by hand
theorems from the "nominal quotient" to your quotient. This is easy
if the theorems are relatively small, but if you have induction
rules with many constructors, then they are big beasts. You would need
to state them explicitly for your quotient and then use the
lift/transfer machinery to prove them. There is no way, I think, to 
lift/transfer theorems by names (on the non-ML-level). So this can
be quite a bit of work, depending on how large your nominal datatype
is.

 > 2. Forming the nominal_datatype, then defining a new equivalence
 > relation ~~ with the axioms of the algebra, along with any relations
 > between generators. Prove theorems of the form "s ~~ t". Essentially,
 > the the first half of the construction in #1, but don't bother with a
 > quotient type. This seems to come with its own set of problems. For
 > instance, things like "s ~~ t ==> P s ==> P t" would need to be
 > assumed for particular P, rather than being an axiom of HOL (as is the
 > case with "=").

Since your equivalence relation is "only" about an associative and 
commutative multiplication operation, this might be the easiest solution
with the least "start-up" costs. The reasoning about a concrete
alpha-equivalence relation is a pain, because one always has to
rename. The reasoning about your equivalence relation might be
much less painful. Though, I would prove that properties are preserved
under the equivalence relation, not just assume this.

 > 3. Treating A as a "theory" rather than a presentation of a particular
 > algebra. That is, form a locale where the term formers are assumed as
 > functions, then assume relevant equalities, including equivariance
 > properties for the term formers. I think the latter should be tagged
 > [eqvt] so the nominal code knows it can apply them to try and
 > alpha-unify terms in various places. The main downside here is you
 > don't get all the nice scaffolding that is laid down by
 > nominal_datatype, but by having the correct assumptions/theorems in
 > context, a term built from these assumed functions could, at least in
 > theory, be handled in much the same way (though clearly things like
 > injectivity of constructors gets lost, once non-trivial equations are
 > assumed).

In my opinion  you would need to state things in even more 
concrete detail than with the first or second solution. Maybe
an expert in locales can chip in and give an opinion whether
this can be made to work smoothly.

Hope this helps,
Christian





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