Re: [isabelle] Permutations



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?

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.)
>>
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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