A computational definition of the notion of vectorial space

TL;DR

This paper proposes a computational approach to defining vector spaces by replacing traditional propositions with algorithms, offering a new perspective on algebraic structures and their validation.

Contribution

It introduces a method to define vector spaces and bilinear operations using algorithms instead of propositions, bridging algebra and computation.

Findings

Replaces propositions with algorithms for defining vector spaces

Applies rewrite systems to algebraic structures

Provides a foundation for semantics in quantum and probabilistic programming

Abstract

We usually define an algebraic structure by a set, some operations defined on this set and some propositions that the algebraic structure must validate. In some cases, we can replace these propositions by an algorithm on terms constructed upon these operations that the algebraic structure must validate. We show in this note that this is the case for the notions of vectorial space and bilinear operation. KEYWORDS: Rewrite system, vector space, bilinear operation, tensorial product, semantics, quantum programming languages, probabilistic programming languages.