422 sort-respecting permutations of atoms. We will use the letters @{text "a, |
422 sort-respecting permutations of atoms. We will use the letters @{text "a, |
423 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for |
423 b, c, \<dots>"} to stand for atoms and @{text "p, q, \<dots>"} to stand for |
424 permutations. The sorts of atoms can be used to represent different kinds of |
424 permutations. The sorts of atoms can be used to represent different kinds of |
425 variables, such as the term-, coercion- and type-variables in Core-Haskell. |
425 variables, such as the term-, coercion- and type-variables in Core-Haskell. |
426 It is assumed that there is an infinite supply of atoms for each |
426 It is assumed that there is an infinite supply of atoms for each |
427 sort. However, in order to simplify the description, we shall restrict ourselves |
427 sort. However, in the intrest of brevity, we shall restrict ourselves |
428 in what follows to only one sort of atoms. |
428 in what follows to only one sort of atoms. |
429 |
429 |
430 Permutations are bijective functions from atoms to atoms that are |
430 Permutations are bijective functions from atoms to atoms that are |
431 the identity everywhere except on a finite number of atoms. There is a |
431 the identity everywhere except on a finite number of atoms. There is a |
432 two-place permutation operation written |
432 two-place permutation operation written |