agda-mugen
agda-mugen copied to clipboard
Study the "wrong" Fractal
There was a bug in the code before the major rewrite 147c8d90f4a3941e547627aac16742d495b5d2bc. It is a valid displacement algebra, though it's different from what's called "Fractal" on paper / in OCaml. The question is---what is it??? @cangiuli @TOTBWF
This was the "wrong" Fractal:
_⊗ᶠ_ : List⁺ ⌞ 𝒟 ⌟ → List⁺ ⌞ 𝒟 ⌟ → List⁺ ⌞ 𝒟 ⌟
[ x ] ⊗ᶠ [ y ] = [ x ⊗ y ]
[ x ] ⊗ᶠ (y ∷ ys) = (x ⊗ y) ∷ ys
(x ∷ xs) ⊗ᶠ [ y ] = (x ⊗ y) ∷ xs
(x ∷ xs) ⊗ᶠ (y ∷ ys) = (x ⊗ y) ∷ (xs ⊗ᶠ ys)
This is the correct one:
_⊗ᶠ_ : List⁺ ⌞ 𝒟 ⌟ → List⁺ ⌞ 𝒟 ⌟ → List⁺ ⌞ 𝒟 ⌟
[ x ] ⊗ᶠ [ y ] = [ x ⊗ y ]
[ x ] ⊗ᶠ (y ∷ ys) = (x ⊗ y) ∷ ys
(x ∷ xs) ⊗ᶠ ys = x ∷ (xs ⊗ᶠ ys)
However, the "wrong" one is a valid displacement algebra. What's this "wrong" one anyway?