История изменений
Исправление quasimoto, (текущая версия) :
Непорядок
Потому что ты используешь ассоциативность которой нет, потому что я её сломал — (∞ + ∞) + -∞ = 0 != ∞ + (∞ + -∞) = ∞.
Можно починить ассоциативности, оставить коммутативности, идентичности по 0 и 1:
data ℤ∞ : Set where
f : ℤ → ℤ∞
⊥ ∞ -∞ : ℤ∞
_+_ : ℤ∞ → ℤ∞ → ℤ∞
f a + f b = f (a +ℤ b)
f _ + ∞ = ∞
f _ + -∞ = -∞
∞ + f _ = ∞
-∞ + f _ = -∞
∞ + ∞ = ∞
-∞ + -∞ = -∞
_ + _ = ⊥
_*_ : ℤ∞ → ℤ∞ → ℤ∞
f a * f b = f (a *ℤ b)
f (+ 0) * ∞ = f (+ 0)
f (+ _) * ∞ = ∞
f -[1+ _ ] * ∞ = -∞
∞ * f (+ 0) = f (+ 0)
∞ * f (+ _) = ∞
∞ * f -[1+ _ ] = -∞
f (+ 0) * -∞ = f (+ 0)
f (+ _) * -∞ = -∞
f -[1+ _ ] * -∞ = ∞
-∞ * f (+ 0) = f (+ 0)
-∞ * f (+ _) = -∞
-∞ * f -[1+ _ ] = ∞
∞ * ∞ = ∞
∞ * -∞ = -∞
-∞ * ∞ = -∞
-∞ * -∞ = ∞
_ * _ = ⊥
но сломать дистрибутивность — 0 * (∞ + -∞) = ⊥ != 0 * ∞ + 0 * -∞ = 0, можно попробовать:
- _ * _ = ⊥
+ f (+ 0) * ⊥ = f (+ 0)
+ ⊥ * f (+ 0) = f (+ 0)
+ _ * _ = ⊥
но тогда ⊥ * (-a + a) = 0 != ⊥ * -a + ⊥ * a = ⊥.
И в любом случае ещё сломаны обратные — ∞ + -∞ = ⊥ != 0, ⊥ + -⊥ = ⊥ != 0.
С другой стороны — полукольцо ℕ при добавлении символа ∞ легко остаётся полукольцом.
Исходная версия quasimoto, :
Непорядок
Потому что ты используешь ассоциативность которой нет, потому что я её сломал — (∞ + ∞) + -∞ = 0 != ∞ + (∞ + -∞) = ∞.
Можно починить ассоциативности, оставить коммутативности, идентичности по 0 и 1:
data ℤ∞ : Set where
f : ℤ → ℤ∞
⊥ ∞ -∞ : ℤ∞
_+_ : ℤ∞ → ℤ∞ → ℤ∞
f a + f b = f (a +ℤ b)
f _ + ∞ = ∞
f _ + -∞ = -∞
∞ + f _ = ∞
-∞ + f _ = -∞
∞ + ∞ = ∞
-∞ + -∞ = -∞
_ + _ = ⊥
_*_ : ℤ∞ → ℤ∞ → ℤ∞
f a * f b = f (a *ℤ b)
f (+ 0) * ∞ = f (+ 0)
f (+ _) * ∞ = ∞
f -[1+ _ ] * ∞ = -∞
∞ * f (+ 0) = f (+ 0)
∞ * f (+ _) = ∞
∞ * f -[1+ _ ] = -∞
f (+ 0) * -∞ = f (+ 0)
f (+ _) * -∞ = -∞
f -[1+ _ ] * -∞ = ∞
-∞ * f (+ 0) = f (+ 0)
-∞ * f (+ _) = -∞
-∞ * f -[1+ _ ] = ∞
∞ * ∞ = ∞
∞ * -∞ = -∞
-∞ * ∞ = -∞
-∞ * -∞ = ∞
_ * _ = ⊥
но сломать дистрибутивность — 0 * (∞ + -∞) = ⊥ != 0 * ∞ + 0 * -∞ = 0, можно попробовать:
- _ * _ = ⊥
+ f (+ 0) * ⊥ = f (+ 0)
+ ⊥ * f (+ 0) = f (+ 0)
+ _ * _ = ⊥
но тогда ⊥ * (-a + a) = 0 != ⊥ * -a + ⊥ * a = ⊥.
И в любом случае ещё сломаны обратные — ∞ + -∞ = ⊥ != 0, ⊥ + ⊥ = ⊥ != 0.
С другой стороны — полукольцо ℕ при добавлении символа ∞ легко остаётся полукольцом.