Skip to content

Commit

Permalink
docs: rename "incorrect fractal" to "weird fractal" and update README
Browse files Browse the repository at this point in the history
  • Loading branch information
@favonia
favonia committed May 31, 2024
1 parent ce97db7 commit 1c541f7
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 18 deletions.
31 changes: 16 additions & 15 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,21 +12,22 @@ This is a formalization of the displacement algebras, their properties, and part

🚧 The links are currently broken.

| 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)_ |
| Displacements | Paper Section | Agda Module | OCaml Module(s) |
| :------------------------------------ | :-------------- | :----------------------------------------------------------------------------- | :------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| Natural numbers | 3.3.1 | [Nat](src/Mugen/Algebra/Displacement/Instances/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/Instances/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/Instances/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/Instances/Constant.agda) | [Constant](https://redprl.org/mugen/mugen/Mugen/Shift/Constant) |
| Binary products | 3.3.3 | [Product](src/Mugen/Algebra/Displacement/Instances/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/Instances/Lexicographic.agda) | [Lexicographic](https://redprl.org/mugen/mugen/Mugen/Shift/Lexicographic) and [Lexicographic](https://redprl.org/mugen/mugen/Mugen/ShiftWithJoin/Lexicographic) |
| Indexed products | 3.3.5 | [IndexedProduct](src/Mugen/Algebra/Displacement/Instances/IndexedProduct.agda) | _(not implementable)_ |
| Nearly constant infinite products | 3.3.5 | [NearlyConstant](src/Mugen/Algebra/Displacement/Instances/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/Instances/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/Instances/Prefix.agda) | [Prefix](https://redprl.org/mugen/mugen/Mugen/Shift/Prefix) |
| Fractal displacements | 3.3.7 | [Fractal](src/Mugen/Algebra/Displacement/Instances/Fractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) |
| Opposite displacements | 3.3.8 | [Opposite](src/Mugen/Algebra/Displacement/Instances/Opposite.agda) | [Opposite](https://redprl.org/mugen/mugen/Mugen/Shift/Opposite) |
| Weird frarctal displacements | 3.3.9 | [WeirdFractal](src/Mugen/Algebra/Displacement/Instances/WeirdFractal.agda) | [Fractal](https://redprl.org/mugen/mugen/Mugen/Shift/Fractal) |
| Endomorphisms | 3.4 (Lemma 3.7) | [Endomorphism](src/Mugen/Algebra/Displacement/Instances/Endomorphism.agda) | _(not implementable)_ |

### Other Theorems

Expand Down
4 changes: 2 additions & 2 deletions ...placement/Instances/IncorrectFractal.agda → .../Displacement/Instances/WeirdFractal.agda
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
module Mugen.Algebra.Displacement.Instances.IncorrectFractal where
module Mugen.Algebra.Displacement.Instances.WeirdFractal where

open import Mugen.Prelude
open import Mugen.Algebra.Displacement
Expand All @@ -11,7 +11,7 @@ variable
o r : Level

--------------------------------------------------------------------------------
-- "Incorrect" Fractal Displacements from our previous incorrect Agda
-- Weird Fractal Displacements from our previous incorrect Agda
-- formalization of Section 3.3.7 of the POPL 2023 paper. They come with
-- a different composition operator. Miraculously, it leads to a valid
-- (but different) displacement algebra.
Expand Down
2 changes: 1 addition & 1 deletion src/Mugen/Everything.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ import Mugen.Algebra.Displacement.Action
import Mugen.Algebra.Displacement.Instances.Constant
import Mugen.Algebra.Displacement.Instances.Endomorphism
import Mugen.Algebra.Displacement.Instances.Fractal
import Mugen.Algebra.Displacement.Instances.IncorrectFractal
import Mugen.Algebra.Displacement.Instances.IndexedProduct
import Mugen.Algebra.Displacement.Instances.Int
import Mugen.Algebra.Displacement.Instances.Lexicographic
Expand All @@ -19,6 +18,7 @@ import Mugen.Algebra.Displacement.Instances.Opposite
import Mugen.Algebra.Displacement.Instances.Prefix
import Mugen.Algebra.Displacement.Instances.Product
import Mugen.Algebra.Displacement.Instances.Support
import Mugen.Algebra.Displacement.Instances.WeirdFractal
import Mugen.Algebra.Displacement.Subalgebra
import Mugen.Algebra.OrderedMonoid
import Mugen.Cat.HierarchyTheory
Expand Down

0 comments on commit 1c541f7

Please sign in to comment.