(About a pre-print by Patrik Jansson & Wouter Swierstra)

What is a finite permutation? In Agda, you might be tempted to define one as a function Fin n → Fin n. That's a fine mathematical object, but a poor representation: nothing in the type stops you from writing a non-bijective function.

In our new pre-print, "niFite semPurtatoni" (Finite permutations in Agda), we study a first-order representation instead. A Permutation n is built inductively, picking one remaining position at a time — the same shape as a Lehmer code or a factorial-number-system digit sequence. Every value of the type denotes a bijection by construction: there is no separate proof obligation, and no way to write down a non-permutation.

Two small functions turn out to carry the whole development: skip, which inserts a gap into a function's codomain, and pinch, which closes one back up. They are approximate inverses of each other, and once you notice that, composition, inversion, and even the classical "counting inversions" description of Lehmer codes all fall out of the same recursive shape.

The pearl builds identity, composition and inversion for Permutation, proves each one correct against the naive function-space semantics, relates the representation to Lehmer codes, and ends with a decision procedure: given any two vectors, decide whether one is a permutation of the other — and if so, produce the witnessing Permutation.

The paper is submitted to the Journal of Functional Programming; we'll update this post once there is a reviewed/published version. In the meantime:

• 📝 Pre-print (HAL): https://hal.science/hal-05746158
• 💻 Code: https://github.com/DSLsofMath/PermutationLehmer : the whole development is one literate Agda file, Permutation.lagda.

Related posts:

• For more on literate Agda files that double as both paper source and executable code, see the earlier post Agda-ventures with PolyP.

• This pearl is the "Algebraic Permutations" strand of the FunPACT project — in fact it's the very paper that post listed as "forthcoming".