Re: [isabelle] Permutations



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

I see.

My conclusion is that an abstract type of permutations

	Abs_perm :: ('a => 'a) => 'a perm
	apply :: 'a perm => 'a => 'a
	affected :: 'a perm => 'a set
	  where "a in affected p <--> apply p a != a"

makes really sense.  E.g. it is easy to define the order of an element:

	order :: 'a perm => 'a => nat
	order p a =
          Min {0 < n <= Suc (card (affected p)). (f ^^ n) a = a}

Cheers,
	Florian


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

-- 

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.