Re: [isabelle] Permutations



On 06/23/2016 12:24 PM, Florian Haftmann wrote:
> Hi all,
> 
> Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
>> It is not clear to me at all how these things can be unified. The
>> notions of permutations as âall lists with elements of a given
>> set/multiset/listâ and permutations as âa bijection from a finite sets
>> to itselfâ are clearly related, but how can this relation be formalised
>> in the best way?
> 
> what I have in mind is a clarification of terminology here: permutations
> as functions and list permutations should be introduced in separate
> theories, where I guess that multisets as quotient type of permutated
> lists can absorb a lot of the latter.
> 
> If an application needs this relation, it can still formalize it.  I did
> not see any example for that in the theories.
> 
> Am 23.06.2016 um 10:02 schrieb Manuel Eberl:
>> After dabbling with permutations a bit, I think that one may even want
>> to have a type of permutations, implemented with Mappings by default.
> 
> Am 23.06.2016 um 11:01 schrieb Johannes HÃlzl:
>> The type "'a bij" would be nice.
> 
> Note that a bijection is not necessarily a permutation: in a
> permutation, each element a has a finite order, ie. some n > 0 such that
> (f ^^ n) a = a.
> 
> Am 23.06.2016 um 12:01 schrieb Christian Sternagel:
>> And in IsaFoR in
>>
> http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/968059663689/thys/Auxiliaries/Renaming.thy
>>
>> definition perms :: "('a \<Rightarrow> 'a) set"
>> where
>>   "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
>>
>> typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
>> by standard (auto simp: perms_def)
>>
>> where permutations have a type parameter and thus we have local-based
>> application of permutations instead of type-class-based (but otherwise I
>> got everything from the Nominal2 development, thanks).
> 
> I don't quite understand the last paragraph.  Which type-class are you
> referring to?

I was referring to Nominal(2) and the type-class of "permutation-types"
(i.e., types whose inhabitants allow application of permutations). So
this is not strictly about permutations but just about a specific
application of them.

cheers

chris

> 
> Cheers,
> 	Florian
> 
>> In any case, any kind of change here will probably lead to a lot of
>> adjustments in every work that uses permutations. This reform will not
>> be an easy task.
>>
>>
>> Cheers,
>>
>> Manuel
>>
>>
>> On 23/06/16 09:47, Florian Haftmann wrote:
>>> Hi all,
>>>
>>> recently I did a full text search concerning permutations and I found
>>> that the existing material is quite dispersed.
>>>
>>>> * Predicates for permutations (functions)
>>>>     * Library/Permutations.thy
>>>>         * Permutations.permutation :: "('a â 'a) â bool"
>>>>         * Permutations.permutes :: "('a â 'a) â 'a set â bool"
>>>> * Representation as swaps
>>>>     * Library/Permutations.thy
>>>>         * Permutations.swapidseq :: "nat â ('a â 'a) â bool"
>>>>         * Permutations.evenperm :: "('a â 'a) â bool"
>>>>         * Permutations.sign :: "('a â 'a) â int"
>>>>     * Planarity_Certificates/Planarity/Permutations_2.thy
>>>>         * Permutations_2.funswapid :: "'a â 'a â 'a â 'a"
>>>>         * Permutations_2.perm_swap :: "'a â 'a â ('a â 'a) â 'a â 'a"
>>>>         * Permutations_2.perm_rem :: "'a â ('a â 'a) â 'a â 'a"
>>>>     * Jordan_Normal_Form/Missing_Permutations.thy
>>>>         * Missing_Permutations.signof :: "(nat â nat) â 'a"
>>>> * Representation as cycles
>>>>     * Planarity_Certificates/Planarity/Executable_Permutations.thy
>>>> * Permuting lists
>>>>     * Library/Permutations.thy
>>>>         * Permutations.permute_list :: "(nat â nat) â 'a list â 'a list"
>>>>     * Library/Permutation.thy
>>>>         * Permutation.perm :: "'a list â 'a list â bool"
>>>>             * btw that equivalence relation would be expressed better
>>>> as Âmset xs = mset ys anyway
>>>> * Derangements
>>>>     * Derangements/Derangements.thy
>>>>         * Derangements.derangements :: "nat set â (nat â nat) set"
>>>>         * Derangements.count_derangements :: "nat â nat"
>>>> * Representation as association lists
>>>>     * Library/Permutations.thy
>>>>         * Permutations.list_permutes :: "('a à 'a) list â 'a set â bool"
>>>>         * Permutations.permutation_of_list :: "('a à 'a) list â 'a â 'a"
>>>>         * Permutations.inverse_permutation_of_list ::  "('a à 'a)
>>>> list â 'a â 'a"
>>>> * Various theorems
>>>>     * Jordan_Normal_Form/Missing_Permutations.thy
>>>>     * Completeness/PermutationLemmas.thy
>>>
>>> In the mid-run there is clearly room for improvement here. I would
>>> suggest one theory Library/Permutation.thy which introduces the basics
>>> (predicates, swaps, cycles) consistently with all available
>>> corresponding theorems. The more specialized things (association lists
>>> etc) could go to separate theories. But this rough sketch has still time
>>> for consideration.
>>>
>>> Cheers,
>>>     Florian
>>>
>>> (For the curious, I stumbled over that issue as follows: first, I
>>> inspected the sources for occurrences of Âno_notation since these are
>>> possible candidates to user syntax bundles; one of these has been the
>>> infix syntax Â_ choose _Â for binomial coefficients, which lead me to
>>> reconsider other combinatorial coefficients (Stirling numbers) as well;
>>> hence the interest in permutations.)
>>>
>>
> 

Attachment: signature.asc
Description: OpenPGP digital signature



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