agda-mugen icon indicating copy to clipboard operation
agda-mugen copied to clipboard

Study the "wrong" Fractal

Open favonia opened this issue 2 years ago • 0 comments

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?

favonia avatar Nov 27 '23 04:11 favonia