From e474e89339047bd370ec423da75f7be2768b7a1b Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Wed, 15 Apr 2026 16:31:13 +0200 Subject: add readme --- readme.md | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 readme.md diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..00f3c89 --- /dev/null +++ b/readme.md @@ -0,0 +1,26 @@ +# Nominal Sets in Lean 4 + +WIP formalization of nominal sets in Lean 4. +The formalization is mostly based on: +- Pitts, A. M. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science 57. Cambridge University Press, 2013. +- Wißmann, Thorsten. Nominal Sets. Skript zur Vorlesung. FAU Erlangen-Nürnberg, October 11, 2024. https://www8.cs.fau.de/ext/teaching/sose2024/nominal-sets/nominal-sets-wissmann-skript.pdf. + +The library is structured as follows: +- `Nominal.Permutations`: + Definition of the subgroup `FPerm` of finitely supported permutations and of `PermSet`s (i.e., sets on which `FPerm` operates). +- `Nominal.Support`: + Definition of support, nominal sets, the least finite support, and some helpers. +- `Nominal.Equivariance`: + Definition of equivariant functions, sets, and relations and some helper lemmas about them. +- `Nominal.Category`: + Definition of the `Nom` category. +- `Nominal.Instances.Basic`: + Some basic instances of nominal sets: discrete nominal sets, the set of atoms, products, coproducts, finitary functions, quotient types, and subtypes. +- `Nominal.Instances.Abstraction`: + Definition of name abstractions and alpha-equivalence, followed by the name abstraction functor. +- `Nominal.Instances.Finsupp`: + Definition of subsets of `PermSet`s with finite support, especially finitely supported sets and functions. +- `Nominal.LambdaCalculus.Preterms`: + Lambda terms as an example of nominal sets, showing that `supp` corresponds to the variables in a term. +- `Nominal.LambdaCalculus.Terms`: + Lambda terms modulo alpha-equivalence as an example, showing that `supp` corresponds to the free variables in a term. \ No newline at end of file -- cgit v1.3.1