diff options
Diffstat (limited to 'readme.md')
| -rw-r--r-- | readme.md | 26 |
1 files changed, 26 insertions, 0 deletions
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 |