Support for abstract vector spaces. #1781

capn-freako · 2022-06-17T21:41:59Z

This PR introduces Algebra.Linear.VectorSpace, an abstract vector space.

The purpose of this new type is to provide the familiar metaphor/interface of "vector/matrix" that people are used to using in their client code, without locking the back-end implementation into arrays (more generally, n-tuples).
In this way, we hope to decouple the capture of design intent from design implementation, for architectures based on the concepts of linear algebra, such as machine learning networks.

commit d298d8b7b3f11c62b244db05970e8ba454baa9be Author: David Banas <capn.freako@gmail.com> Date: Sat May 28 09:22:06 2022 -0700 Final commit to `vector-space-foldr` branch. The experiment w/ right folds worked beautifully and will be merged back into `vector-space`. - Reverted `Data.List.Properties`, as I no longer need all the left fold accoutrements. commit 8845ac79817c39423edb20ba87b0e75a8d0265c2 Author: David Banas <capn.freako@gmail.com> Date: Sat May 28 08:20:58 2022 -0700 Clean-up pass. commit d3b3256e88152d7d9820a99be2a584ae0135ad21 Author: David Banas <capn.freako@gmail.com> Date: Sat May 28 07:35:29 2022 -0700 Cleanup of `VectorSpace.Properties`. commit 06e69efbcce0c2a7fcd32936d0b2bb1fdff5f348 Author: David Banas <capn.freako@gmail.com> Date: Sat May 28 07:13:50 2022 -0700 First successful compilation of `T-oS<=>v-dot`.

capn-freako · 2022-08-17T01:39:22Z

Anyone know why the Ubuntu build / test-stdlib (pull_reuest) test failed?

guilhermehas · 2022-08-19T14:07:33Z

From Wikipedia (https://en.wikipedia.org/wiki/Vector_space), I think that Vector Space is defined over a Field and not from a Commutative Ring.

MatthewDaggitt · 2022-08-23T10:24:34Z

Anyone know why the Ubuntu build / test-stdlib (pull_reuest) test failed?

Not your fault (#1804)

From Wikipedia (https://en.wikipedia.org/wiki/Vector_space), I think that Vector Space is defined over a Field and not from a Commutative Ring.

Thanks @Taneb and @guilhermehas for the heads up! I'd totally missed that. It's a good point. @capn-freako I think they're right that we should stick to the standard definition. May I ask where you go the current definition from?

capn-freako · 2022-08-27T16:10:15Z

Thanks @Taneb and @guilhermehas for the heads up! I'd totally missed that. It's a good point. @capn-freako I think they're right that we should stick to the standard definition. May I ask where you go the current definition from?

Admittedly, I "cheated" when I didn't find Field available among the other standard algebraic definitions.
Shall I take a whack at defining Field and, then, redefining VectorSpace to use it, instead of CommutativeRing?
I think we'll need division eventually, anyway, when working most generally w/ vector spaces, even abstractly.

JacquesCarette · 2022-08-27T17:25:44Z

You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.

capn-freako · 2022-08-27T19:41:49Z

You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.

Thanks, Jacques! Have you been down that particular road before?

I like this concise summary of Field (from the Wikipedia page):

Even more summarized: a field is a commutative ring where 0 ≠ 1 and all nonzero elements are invertible.

capn-freako · 2022-08-28T00:40:24Z

You're likely to want to define R-module over a (commutative?) ring first. That's fully constructive. Vector Space over a Field is... hard.

Oh, shoot! The new multiplicative inverse function must be partial, because 0# must be excluded from its domain.
Is that why you warned me thusly?

capn-freako · 2022-08-28T01:04:19Z

Hey guys, a question about something in Algebra.Structures:
In IsRingWithoutOne, the additive inverse is defined thusly:

+-isAbelianGroup : IsAbelianGroup + 0# -_

while in IsNearring it is defined:

+-inverse   : Inverse 0# _⁻¹ +

What is the significance of this difference?

MatthewDaggitt · 2022-08-30T09:02:04Z

Oh, shoot! The new multiplicative inverse function must be partial, because 0# must be excluded from its domain.
Is that why you warned me thusly?

Yes we haven't quite worked out how we want to handle the partiality. See #1175 for discussion.

MatthewDaggitt · 2022-08-30T09:04:05Z

What is the significance of this difference?

It's an artefact of the order of inheritance. One inherits from IsQuasiring and the other from IsAbelianGroup. In general it's very difficult to come up with a consistent inheritance pattern and is an area of active research how to do it modularly (which we have definitely not achieved in the standard library!)

JacquesCarette · 2022-08-31T08:50:00Z

Have you been down that particular road before?

Not this exact one, but close enough to know that this way lies much pain.

Oh, shoot! The new multiplicative inverse function must be partial, because 0# must be excluded from its domain.
Is that why you warned me thusly?

Yes!

Matthew also said:

In general it's very difficult to come up with a consistent inheritance pattern and is an area of active research how to do it modularly (which we have definitely not achieved in the standard library!)

In my mind, the most general solution requires explicit morphisms between definitions (not just embeddings induced by same-name-same-thing) and a proper notion of pullback/pushout. Agda actually has many of the needed features already, but "closing the gap" still requires quite a lot of work.

Before moving list properties to: `Data.List.Properties.CommutativeRing`.

…erties.CommutativeRing.

MatthewDaggitt · 2022-09-17T13:17:56Z

@capn-freako I'm going to close this PR as I think the current approach needs some rethinking and probably some addition scaffolding first. Feel free to open a new PR if you revisit it later on and think you've fixed the problems!

capn-freako · 2022-09-17T16:17:31Z

Oh, snap! I was just putting the finishing touches on a next push, which I think addresses the concerns and is much more in line w/ the literature.
Any chance you could reopen this PR for one more round?

MatthewDaggitt · 2022-09-17T16:21:33Z

Sure!

capn-freako · 2022-09-18T21:10:54Z

Okay, guys, I think that last push is much more in line with the literature and addresses your previous concerns.
Please, take a look and let me know what you think.

Thanks!
-db

Taneb

On the whole I'm really not happy with the approach taken here. We certainly shouldn't merge this before the imminent release of 2.0, and I don't think this approach will lead to something merits inclusion in the standard library.

I welcome @capn-freako to adapt this into a standalone library and continue developing it.

I suggest for the standard library that we work towards linear algebra in small, well-reasoned chunks building on what we've already implemented. I have in my head a rough roadmap for this (and other things!) that I've been working on for a good while.

Taneb · 2022-09-19T08:14:49Z

src/Algebra/Structures.agda

+
+  field
+    isCommutativeRing : IsCommutativeRing + _*_ - 0# 1#
+    *-inverse         : {x : A} → (p : x ≢ 0#) → (x * ((x ⁻¹) {p})) ≈ 1#


This mixes propositional equality (_≢_) with setoid equality (_≈_), which is a really bad idea. Consider Data.Rational.Unnormalised. This type has many representations of 0 which are propositionally distinct, e.g. mkℚᵘ (+ 0) 0 and mkℚᵘ (+ 0) 1, so instead it uses the equivalence relation _≃_ under which all of these representations of 0 are equivalent.

Taneb · 2022-09-19T08:24:00Z

src/Algebra/Structures.agda

+  _/_ : (x y : A) → {y ≢ 0#} → A
+  (x / y) {p} = x * ((y ⁻¹) {p})
+
+  field


The definition of a field also needs a rule that 0 does not equal 1, or equivalently that every invertible element is nonzero

Taneb · 2022-09-19T08:25:11Z

src/Algebra/Structures.agda

@@ -863,6 +865,21 @@ record IsCommutativeRing
    ; *-isCommutativeMonoid
    )

+record IsField


I'm not sure that definitions of fields should go in Algebra.Structures and Algebra.Bundles, considering that they're not quite algebraic structures. I'm not sure where we should put this definition, but we already have Algebra.Apartness.{Bundles, Structures} containing one notion of a field.

Taneb · 2022-09-19T08:32:37Z

src/Algebra/Linear/Structures.agda

+  record IsVectorSpace : Set (suc (ℓm ⊔ ℓr ⊔ m ⊔ r)) where
+
+    field
+      basis : IsBasis


I think there are vector spaces of interest for which it is very difficult for us to define a basis for, such as the space of functions from ℚ to ℚ.

Taneb · 2022-09-19T08:34:25Z

src/Algebra/Linear/Structures.agda

+    vacc ss vs = foldr _+ᴹ_ 0ᴹ (zipWith (_*ₗ_) ss vs)
+
+    field
+      basisSet         : List V


Having the basis set be a list means we can't define infinite-dimensional vector spaces, such as the space of polynomials over ℚ. An alternative might be to have an indexing set and a function from that set to the vector space, but then we need to decide whether we need to think about levels.

Taneb · 2022-09-19T08:45:17Z

src/Algebra/Bundles.agda

+    -_      : Op₁ Carrier
+    0#      : Carrier
+    1#      : Carrier
+    _⁻¹      : (x : Carrier) → {x ≢ 0#} → Carrier


I think that this operator might be very hard to use in practice. I don't see how the implicit x ≢ 0# parameter would ever be inferred.

Taneb · 2022-09-19T09:10:16Z

src/Algebra/Linear/Structures.agda

+
+  -- An _Inner Product Space_ is a vector space augmented with a function
+  -- that takes two vectors and returns a scalar.
+  record IsInnerProductSpace (f : V → V → S) : Set (suc (ℓm ⊔ ℓr ⊔ m ⊔ r)) where


There really ought to be some laws here.

MatthewDaggitt · 2023-02-23T03:28:12Z

Given @Taneb's feedback and the lack of reply I'm going to close this again for now.

capn-freako added 30 commits May 5, 2022 12:50

Temporary check-in.

27746d8

Last linearity axiom proved.

65989fd

Merge branch 'master' of https://github.com/agda/agda-stdlib

c057439

Final edits before initial pull request.

2d7abea

First checked version of Data.VectorSpace.Core.

5edf18c

WARNING: Non-functional commit! (Pre-branch switch)

4b8bbd7

Second attempt at PR1767.

b6c7519

Merge branch 'master' into vector-space

1502629

Removed some public modifiers and need to back propagate.

f8a4d61

Removed some unneeded publics.

7c205f9

Merge branch 'master' into vector-space

29884e9

Returning to master, to address feedback on PR-1767.

7f22854

Shifted to proof-local reasoning module openning, as per Jacques.

ea73683

Eliminated unneccesary x, as per Jacques.

c9c8798

Reverted to f from semantic brackets, as per Jacques.

c18c68a

Switched to A.<op> notation, as per Jacques.

caabb3a

Merge branch 'master' into vector-space

1826b6e

Changes requested by Matthew Daggitt.

3c11956

Temporary check-in only!

88e5c2a

Changes, as per Matthew Daggitt, re: PR agda#1767

d2da8f0

To bring in recent changes to master only!

9d88ee1

Merge branch 'master' into vector-space

6b5fa24

Non-functional checkpoint, before switching to right fold.

d0c990d

Responding to Jacques feedback.

c5de4d1

Replaced my custom join function w/ Data.Product.<_,_>.

689c06e

Merge branch 'master' into vector-space

410821e

Proved inner product extensional equivalence.

1bad78e

Setoid for linear maps.

a517370

Brought extensional equivalence and linear map into Core.

8e41e8d

Responding to Matthew`s latest comments.

f8d5169

First successful compilation of Algebra.Structures.IsField.

f7315d1

capn-freako added 3 commits September 12, 2022 07:08

First successful compilation of Algebra.Linear.Structures.

995f188

Before moving list properties to: `Data.List.Properties.CommutativeRing`.

Moved list properties from Algebra.Linear.Structures to Data.ListProp…

25ba2bd

…erties.CommutativeRing.

VectorSpace ==> DotProductSpace

35d10ec

MatthewDaggitt added status: won't-merge Decided against merging the PR in. and removed status: being-worked-on labels Sep 17, 2022

MatthewDaggitt closed this Sep 17, 2022

MatthewDaggitt reopened this Sep 17, 2022

capn-freako added 3 commits September 18, 2022 13:22

First successful compile/test of retooled vector-space.

c19b101

Merge branch 'master' of https://github.com/agda/agda-stdlib

316b098

Merge branch 'master' into vector-space

a88bf37

Taneb reviewed Sep 19, 2022

View reviewed changes

MatthewDaggitt closed this Feb 23, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support for abstract vector spaces. #1781

Support for abstract vector spaces. #1781

capn-freako commented Jun 17, 2022 •

edited

Loading

capn-freako commented Aug 17, 2022

guilhermehas commented Aug 19, 2022

MatthewDaggitt commented Aug 23, 2022

capn-freako commented Aug 27, 2022

JacquesCarette commented Aug 27, 2022

capn-freako commented Aug 27, 2022

capn-freako commented Aug 28, 2022

capn-freako commented Aug 28, 2022

MatthewDaggitt commented Aug 30, 2022

MatthewDaggitt commented Aug 30, 2022

JacquesCarette commented Aug 31, 2022

MatthewDaggitt commented Sep 17, 2022

capn-freako commented Sep 17, 2022

MatthewDaggitt commented Sep 17, 2022

capn-freako commented Sep 18, 2022

Taneb left a comment

Taneb Sep 19, 2022

Taneb Sep 19, 2022

Taneb Sep 19, 2022

Taneb Sep 19, 2022

Taneb Sep 19, 2022

Taneb Sep 19, 2022

Taneb Sep 19, 2022

MatthewDaggitt commented Feb 23, 2023

Support for abstract vector spaces. #1781

Support for abstract vector spaces. #1781

Conversation

capn-freako commented Jun 17, 2022 • edited Loading

capn-freako commented Aug 17, 2022

guilhermehas commented Aug 19, 2022

MatthewDaggitt commented Aug 23, 2022

capn-freako commented Aug 27, 2022

JacquesCarette commented Aug 27, 2022

capn-freako commented Aug 27, 2022

capn-freako commented Aug 28, 2022

capn-freako commented Aug 28, 2022

MatthewDaggitt commented Aug 30, 2022

MatthewDaggitt commented Aug 30, 2022

JacquesCarette commented Aug 31, 2022

MatthewDaggitt commented Sep 17, 2022

capn-freako commented Sep 17, 2022

MatthewDaggitt commented Sep 17, 2022

capn-freako commented Sep 18, 2022

Taneb left a comment

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

Taneb Sep 19, 2022

Choose a reason for hiding this comment

MatthewDaggitt commented Feb 23, 2023

capn-freako commented Jun 17, 2022 •

edited

Loading