Skip to content

Commit

Permalink
docs(README): update links and point out the missing parts
Browse files Browse the repository at this point in the history
  • Loading branch information
@favonia
favonia committed Nov 28, 2023
1 parent f134d5c commit f6b44b8
Showing 1 changed file with 25 additions and 21 deletions.
46 changes: 25 additions & 21 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
<!--- vim: set nowrap: --->

# ♾ mugen 無限 in Agda

This is a formalization of the displacement algebras, their properties, and part of meta-theoretic analysis found in our POPL 2023 paper [“An Order-Theoretic Analysis of Universe Polymorphism”.](https://favonia.org/files/mugen.pdf) The accompanying OCaml implementation is at <https://github.com/RedPRL/mugen/>.
Expand All @@ -8,32 +10,34 @@ This is a formalization of the displacement algebras, their properties, and part

### Displacement Algebras

| Displacements | Paper Section | Agda Module | OCaml Module(s) |
| :------------------------------------ | :------------ | :---------------------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| Natural numbers | 3.3.1 | [Nat](src/Mugen/Algebra/Displacement/Nat.agda) | [Nat](https://redprl.org/mugen/mugen/Mugen/Shift/Nat) and [Nat](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Nat) |
| Integers | 3.3.1 | [Int](src/Mugen/Algebra/Displacement/Int.agda) | [Int](https://redprl.org/mugen/mugen/Mugen/Shift/Int) and [Int](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Int) |
| Non-positive integers | 3.3.1 | [NonPositive](src/Mugen/Algebra/Displacement/NonPositive.agda) | [NonPositive](https://redprl.org/mugen/mugen/Mugen/Shift/NonPositive) and [NonPositive](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NonPositive) |
| Constant displacements | 3.3.2 | [Constant](src/Mugen/Algebra/Displacement/Constant.agda) | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant) |
| Binary products | 3.3.3 | [Product](src/Mugen/Algebra/Displacement/Product.agda) | [Product](https://redprl.org/mugen/mugen/Mugen/Shift/Product) and [Product](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Product) |
| Lexicographic binary products | 3.3.4 | [Lexicographic](src/Mugen/Algebra/Displacement/Lexicographic.agda) | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic) |
| Infinite products | 3.3.5 | Generalized to [IndexedProduct](src/Mugen/Algebra/Displacement/IndexedProduct.agda) | _(not implementable)_ |
| Nearly constant infinite products | 3.3.5 | [NearlyConstant](src/Mugen/Algebra/Displacement/NearlyConstant.agda) | [NearlyConstant](https://redprl.org/mugen/mugen/Mugen/Shift/NearlyConstant) and [NearlyConstant](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NearlyConstant) |
| Infinite products with finite support | 3.3.5 | [FiniteSupport](src/Mugen/Algebra/Displacement/FiniteSupport.agda) | [FiniteSupport](https://redprl.org/mugen/mugen/Mugen/Shift/FiniteSupport) and [FiniteSupport](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/FiniteSupport) |
| Prefix order | 3.3.6 | [Prefix](src/Mugen/Algebra/Displacement/Prefix.agda) | [Prefix](https://redprl.org/mugen/mugen/Mugen/Shift/Prefix) |
| Fractal displacements | 3.3.7 | [Fractal](src/Mugen/Algebra/Displacement/Fractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) |
| Opposite displacements | 3.3.8 | [Opposite](src/Mugen/Algebra/Displacement/Opposite.agda) | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite) |
| Endomorphisms | 3.4 | [Endomorphism](src/Mugen/Algebra/Displacement/Endomorphism.agda) | _(not implementable)_ |
| Displacements | Paper Section | Agda Module | OCaml Module(s) |
| :------------------------------------ | :-------------- | :---------------------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| Natural numbers | 3.3.1 | [Nat](src/Mugen/Algebra/Displacement/Nat.agda) | [Nat](https://redprl.org/mugen/mugen/Mugen/Shift/Nat) and [Nat](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Nat) |
| Integers | 3.3.1 | [Int](src/Mugen/Algebra/Displacement/Int.agda) | [Int](https://redprl.org/mugen/mugen/Mugen/Shift/Int) and [Int](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Int) |
| Non-positive integers | 3.3.1 | [NonPositive](src/Mugen/Algebra/Displacement/NonPositive.agda) | [NonPositive](https://redprl.org/mugen/mugen/Mugen/Shift/NonPositive) and [NonPositive](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NonPositive) |
| Constant displacements | 3.3.2 | [Constant](src/Mugen/Algebra/Displacement/Constant.agda) | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant) |
| Binary products | 3.3.3 | [Product](src/Mugen/Algebra/Displacement/Product.agda) | [Product](https://redprl.org/mugen/mugen/Mugen/Shift/Product) and [Product](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Product) |
| Lexicographic binary products | 3.3.4 | [Lexicographic](src/Mugen/Algebra/Displacement/Lexicographic.agda) | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic) |
| Infinite products | 3.3.5 | Generalized to [IndexedProduct](src/Mugen/Algebra/Displacement/IndexedProduct.agda) | _(not implementable)_ |
| Nearly constant infinite products | 3.3.5 | [NearlyConstant](src/Mugen/Algebra/Displacement/NearlyConstant.agda) | [NearlyConstant](https://redprl.org/mugen/mugen/Mugen/Shift/NearlyConstant) and [NearlyConstant](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/NearlyConstant) |
| Infinite products with finite support | 3.3.5 | [FiniteSupport](src/Mugen/Algebra/Displacement/FiniteSupport.agda) | [FiniteSupport](https://redprl.org/mugen/mugen/Mugen/Shift/FiniteSupport) and [FiniteSupport](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/FiniteSupport) |
| Prefix order | 3.3.6 | [Prefix](src/Mugen/Algebra/Displacement/Prefix.agda) | [Prefix](https://redprl.org/mugen/mugen/Mugen/Shift/Prefix) |
| Fractal displacements | 3.3.7 | [Fractal](src/Mugen/Algebra/Displacement/Fractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) |
| Opposite displacements | 3.3.8 | [Opposite](src/Mugen/Algebra/Displacement/Opposite.agda) | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite) |
| Endomorphisms | 3.4 (Lemma 3.7) | [Endomorphism](src/Mugen/Algebra/Displacement/Endomorphism.agda) | _(not implementable)_ |

### Other Theorems

| Theorems | Paper Section | Agda Module |
| :------------------------- | :------------ | :-------------------------------------------------------------------------------------------------------------- |
| Validity of McBride monads | 3.1 | [Mugen.Cat.HierarchyTheory](./src/Mugen/Cat/HierarchyTheory/McBride.agda) |
| Embedding of endomorphisms | 3.4 | [Mugen.Cat.HierarchyTheory.Properties](./src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda) |
| Theorems | Paper Section | Agda Module |
| :------------------------------------ | :----------------- | :-------------------------------------------------------------------------------------------------------------------------------------- |
| Validity of McBride monads | 3.1 | [Mugen.Cat.HierarchyTheory.McBride](./src/Mugen/Cat/HierarchyTheory/McBride.agda) |
| Embedding of endomorphisms | 3.4 (Lemma 3.8) | [Mugen.Cat.HierarchyTheory.Universality.EndomorphismEmbedding](./src/Mugen/Cat/HierarchyTheory/Universality/EndomorphismEmbedding.agda) |
| Embedding of small hierarchy theories | 3.4 (Lemma 3.9) | _(TODO)_ |
| Universality of McBride monads | 3.4 (Theorem 3.10) | _(TODO)_ |

## Building

### Docker
### Docker (tested by CI)

Run the following command to check formalization.

Expand All @@ -48,6 +52,6 @@ docker run agda-mugen:edge

2. Compile and install [Agda](https://github.com/agda/agda) at the commit `5c8116227e2d9120267aed43f0e545a65d9c2fe2`. You will have to build Agda from the source.

3. Install [1Lab](https://github.com/plt-amy/1lab) and add the path to its `1lab.agda-lib` to `${AGDA_DIR}/libraries`. This formalization was checked against the commit `ac6f81089a261e9c0d2ce3ede37a4a09764cb2ad` of the 1lab library.
3. Install [1Lab](https://github.com/plt-amy/1lab) and add the path to its `1lab.agda-lib` to `${AGDA_DIR}/libraries`. This formalization was checked against the commit `a84319a523d866afc828535ce669ed114fbb5fd1` of the 1lab library.

4. Type check the formalization by running `make`.

0 comments on commit f6b44b8

Please sign in to comment.