niFite semPurtatoni
Patrik Jansson, Wouter Swierstra · HAL (Le Centre pour la Communication Scientifique Directe) · 2026
Finite permutations have numerous applications in both mathematics and computing, from the classification of finite groups to sorting algorithms. This pearl studies a first-order representation of finite permutations in the dependently typed programming language Agda (Norell 2007). This representation is precise, encoding exactly the bijective functions between finite sets; yet it supports a direct definition of composition, inversion, and identity. This pearl constructs these operations, proves their correctness, and presents a decision procedure that computes this first-order representation of permutations from any pair of vectors, if it exists.