A Computational Definition of the Notion of Vectorial Space
Pablo Arrighi, Gilles Dowek · Electronic Notes in Theoretical Computer Science · 2005
We usually define an algebra by a set, some operations defined on this set and some propositions that the algebra must validate. In some cases, we can replace these propositions by an algorithm on terms constructed upon these operations that the algebra must validate. We show in this note that this is the case for the notion of vectorial space and bilinear function.