[draft] Polynomial #2821
[draft] Polynomial #2821
Conversation
|
Zeroth thoughts:
First thoughts:
Second thought:
Third thought:
Fourth thoughts:
|
| x≈ε⇒x⁻¹≈ε {x} x≈ε = begin | ||
| x ⁻¹ ≈⟨ ⁻¹-cong x≈ε ⟩ | ||
| ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ | ||
| ε ∎ |
There was a problem hiding this comment.
I wasn't sure if
- this lemma met the Fairbairn threshhold (moreover, it's used only once in this PR)
- this proof was the most 'efficient', compared to
x≈ε⇒x⁻¹≈ε = identityˡ-unique _ _ ∘ trans (inverseˡ _) ∘ sym
which uses only a Loop property beyond the basic IsGroup axiomatisation.
| x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin | ||
| x ≈⟨ ⁻¹-involutive x ⟨ | ||
| x ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈ε ⟩ | ||
| ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ | ||
| ε ∎ |
There was a problem hiding this comment.
Ditto, only more so:
x⁻¹≈ε⇒x≈ε = identityʳ-unique _ _ ∘ trans (inverseˡ _) ∘ symThere was a problem hiding this comment.
Alternatively, you could bootstrap
| x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin | |
| x ≈⟨ ⁻¹-involutive x ⟨ | |
| x ⁻¹ ⁻¹ ≈⟨ ⁻¹-cong x⁻¹≈ε ⟩ | |
| ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ | |
| ε ∎ | |
| x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = begin | |
| x ≈⟨ ⁻¹-involutive x ⟨ | |
| x ⁻¹ ⁻¹ ≈⟨ x≈ε⇒x⁻¹≈ε x⁻¹≈ε ⟩ | |
| ε ∎ |
which is 'just'
x⁻¹≈ε⇒x≈ε = trans (sym (¹-involutive _)) ∘ x≈ε⇒x⁻¹≈ε
|
I've been working on a slightly different implementation of this. Let me find what I've done and compare - notably, I used lists rather than vectors, and didn't have a notion of degree |
I think you need commutativity of multiplication to show that polynomial evaluation preserves multiplication |
| data _≈_ : (Poly m) → (Poly n) → Set (ℓ₁ L.⊔ ℓ₂) where | ||
| []≈ : (q : Poly n) → IsZero q → [] ≈ q | ||
| ≈[] : (p : Poly m) → IsZero p → p ≈ [] | ||
| cons : (a ≈A b) → (p ≈ q) → (a ∷ p) ≈ (b ∷ q) |
There was a problem hiding this comment.
This particular definition has two separate proofs that [] is equal to []... not necessarily the end of the world, but it bothers me
Hmmm. https://math.stackexchange.com/questions/806119/do-polynomials-make-sense-over-non-commutative-rings Otherwise could we even speak about polynomials over rings such as square matrices (for the Cayley-Hamilton theorem, for example, even if that's usually only considered for matrices over commutative rings, such matrices don't enjoy commutative multiplication... while for any polynomial and its values, it is the case that powers of an element do commute...)? I think the real issue is making sure that multiplication is defined correctly... see also https://en.wikipedia.org/wiki/Monoid_ring |
|
Non-commutative polynomial rings certainly do make sense and are useful. See for examples the skew polynomials that arise when modeling various kinds of operators. Axiom does allow polynomials over coefficients rings like square matrices. |
|
For reference, here's my implementation of polynomials: https://gist.github.com/Taneb/3257f47436ec6b11de403d839d7c413b |
|
Thank you for the detailed feedback and the comments and I apologize for the delayed response. Although it will take some time, I will try implement the changes using the semiring instead of the commutative ring and eventually prove the universal property of polynomial rings. Since this is only a draft which I should have made it clear, any further comments or suggestions are welcome. |
| open import Data.Vec.Base as Vec using ([]; _∷_) | ||
| import Level as L | ||
|
|
||
| module Algebra.Polynomial.Base1 |
There was a problem hiding this comment.
Base1 is quite a rotten name. I'm sure we can help find a better name, once we know the intent?
| -- Types | ||
|
|
||
| record Polynomial : Set ℓ₁ where | ||
| constructor _,_ |
There was a problem hiding this comment.
I strongly object to overloading _,_ for this constructor!
| record Polynomial : Set ℓ₁ where | ||
| constructor _,_ | ||
| field | ||
| degree : ℕ |
There was a problem hiding this comment.
There should be a comment here that the "degree" is off-by-one from the usual notion of the degree of a polynomial. It is more like a length than a degree.
| --------------------------------------------------- | ||
| -- Operations | ||
|
|
||
| -- Multiply the polynomial by a factor of x |
There was a problem hiding this comment.
I'd say "by x" rather than "by a factor of x", as I wondering "what factor?"
And why not implement `shift :: ℕ → Polynomial → Polynomial instread?
| open import Data.Vec.Base as Vec using ([]; _∷_) | ||
| import Level as L | ||
|
|
||
| module Algebra.Polynomial.Base2 |
There was a problem hiding this comment.
Same comment about the name
| module PolynomialRingMorphism | ||
| {ℓ₃ ℓ₄} | ||
| (B : CommutativeRing ℓ₃ ℓ₄) | ||
| (β : CommutativeRing.Carrier B) |
There was a problem hiding this comment.
Why are Homomorphisms always scaled? This seems like an odd choice.
| eval-equiv {ℕ.zero} [] = B.refl | ||
| eval-equiv {suc m} (a ∷ p) = begin | ||
| ⟦ a ⟧ +B β *B eval-p p | ||
| ≈⟨ B.+-congˡ (B.*-congˡ (eval-equiv p) ) ⟩ |
There was a problem hiding this comment.
There's no point in using equational reasoning when the proof is exactly 1 inference.
| eval-p (a ∷ p) = ⟦ a ⟧ +B (β *B eval-p p ) | ||
|
|
||
|
|
||
| eval : Polynomial → CommutativeRing.Carrier B |
There was a problem hiding this comment.
Bad name: it took me a while to figure out that this "evaluate at 1 scaled by β" or equivalently "evaluate at β". The evaluation point should be a (local) parameter, not a module parameter.
| eval (m , p) +B eval (n , q) | ||
| ∎ | ||
|
|
||
| eval-p-1#-homomorphic : eval-p (A1# ∷ []) ≈B 1# |
There was a problem hiding this comment.
Inlining the definition of a constant polynomial makes this definition harder to read. Plus this is true for any member of the ground ring.
| ∎ | ||
| where | ||
| step1 = begin | ||
| β *B -B eval-p p |
There was a problem hiding this comment.
This seems like a special case of commutativity of scalars.
This draft pull request introduces a new way to represent a polynomial over commutative ring -- as a vector over the commutative ring -- and a proof that polynomials themselves make up a commutative ring.