1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
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.
|
