# 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.

## Key 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.