Groebner Rings in TH∃OREM∀:
A Case Study in Functors and Categories

Bruno Buchberger
RISC (Research Institute for Symbolic Computation)
Johannes Kepler University
A4232 Castle of Hagenberg, Austria
Bruno.Buchberger@RISC.Uni-Linz.ac.at

Bibliographic Information: SFB Technical Report 2003-49, SFB "Scientific Computing",  Mathematical Institutes, Johannes Kepler University, Linz, Austria, Version 2003-11-15.

Copyright Bruno Buchberger 2003.

Copyright Note: This file can be copied and stored under the following conditions:

-  the file is kept unchanged including the copyright note
- a message is sent to buchberger@risc.uni-linz.ac.at
- if the material is used, please, cite this report appropriately.

Acknowledgement: The research in this paper was sponsored by RICAM (Radon Institute for Computational and Applied Mathematics, Austrian Academy of Science), the Austrian FWF (Austrian Science Foundation, Österreichischer Fonds zur Förderung der Wissenschaftlichen Forschung), Project 1302 in the frame of the SFB (Special Research Area) 013 "Scientific Computing". The paper was written while the author was a visiting researcher at Lamar University, Computer Science Department, Beaumont, Texas sponsored by an NSF Project "Efficient Groebner Basis Computations",  CCR-0333746,  of Dr. Quoc-Nam Tran and sponsored by the Radon Institute for Computational and Applied Mathematics of the Austrian Academy of Science, Linz, Austria.

Introduction

The Objectives of This Paper

This paper has two objectives:

provide a major case study for the use of categories and functors in Theorema, introduced in [Buchberger  1996],

provide a formulation of the main algorithms in Groebner bases theory in a generic way based on (a new variant of) the notion of reduction ring introduced in [Buchberger 1984].

All the Theorema functor programs contained in this notebook are executable within a Mathematica session. Thus, starting from this notebook the reader can execute various computational experiments and can also add new functors, construct new domains, and compute in these domains.

Domains, Functors, and Categories

Functors are an elegant tool for making algorithms domain-independent.  In our view, a functor is a function that takes domains as arguments and produces other domains. (A domain is a carrier together with a couple of operations on the carrier.) This has a computational aspect and a reasoning aspect:

The computational aspect of functors: A functor takes the carriers and the operations of the input domains and defines the carrier and the operations of the resulting domain in terms of the carriers and the operations of the input domains. In the case where the definitions of the operations in the functor are algorithmic, the operations in the resulting domain are algorithmic if the operations in the input domains are algorithmic.

The reasoning aspect of functors: A functor can also be understood as a mechanism that transforms properties of the input domains into properties of the resulting domain. We call a collection of formulae that describe properties of domains a "category description". A category is the collection of all domains (taken from some universe of domains) that satisfy a given category description. For a given  functor F, we can formulate "conservation theorems". These are theorems that of the following structure:

If domains U, V, ... are in the categories 𝒞, 𝒟, ... then F[ U, V, ...] is in category ℋ.

(Example of a typical conservation theorem: If C is a ring then the polyonomial domain over C  is also a ring.)

Our Theorema setting of the functor view and methodology  is very similar to the view and methodology of functors in SML, see [Milner et al. 1997], but it differs in two important respects:

It is more general because it allows much more general constructions of carrier sets and operations including nonalgorithmic constructions using all definition mechanisms of mathematics.

It allows the formulation of categories and conservation theorems within the same language, namely Theorema, and also aims at providing automated reasoning facilities for conservation theorems (as part of a general methodology for automated proofs).

Technically, there are many different ways of defining domains. In most algebra books, a domain is a tuple consisting of a carrier set and a couple of operations (functions and predicates) on the carrier. However, for Theorema, we adopted a slightly different representation, which we found advantageous for the formulation of certain more advanced concepts like, for example, the isomorphism of two domains. This representation, in a certain respect, follows the concept of "interpretion" of model theory. (An interpretation assigns operations, i.e. functions and predicates, to operations symbols, i.e. function symbols and predicate symbols, respectively.) In more detail, we say that a domain D can be applied to an operation f yielding an operation that now can be applied to a couple of arguments, e.g. x and y:

D[f][x, y].

It is clear that, for this formulation of domains, we need the possibility of "Currying" in our language: D[f] is a function that can be applied to arguments x, y. Furthermore, we introduce the abbreviating notation

(Underscript[f, D])[x, y]

for

D[f][x, y].

Also, we characterize the "carrier" of a domain not by a set but by a unary decision predicate that yields true or false depending on whether or not the input belongs to the carrier of D. Often, we denote this decision predicate by ϵ, i.e.

(Underscript[ϵ, D]) [x]

yields true or false depending on whether or not the input x belongs to D. (Note that we use the Greek letter 'ϵ' and not the set theory element symbol '∈' for this purpose! In fact, arbitrary symbols can be used for characterizing carriers. In particular, it is well possible that a domain has several carriers.)

Note that functors, in addition to arguments that are domains may also have a couple of other input argurments as, for example the number n of indeterminates for the functor that constructs the n-ary Cartesian product of a domain, etc.

An Example of a Functor

Let's formulate, in Theorema notation, the functor CP that takes a domain D with operation + and forms the "Cartesian product" of D with D

Cartesian–Product[D]=Functor[N,any[X, x1, x2, y1, y2],
	({{𝕤 = ⟨+∶N\[Cross]N -> N⟩}, {({{(Underscript[ϵ, N])[
                          X] ⇔ (is–tuple[
                              X] ∧ (\[LeftBracketingBar]X\[RightBracketingBar] = 2) ∧ (Underscript[ϵ, D])[(Subscript[X, 1])] ∧ (Underscript[ϵ, D])[
                              (Subscript[X, 2])])}, {\(⟨x1, 
                            x2⟩\( + \+N\)⟨y1, 
                            y2⟩ = ⟨x1\( + \+D\)y1, x2\( + \+D\)y2⟩\)}})}})
	]

This shold  be understood as follows: Assume that we have a domain D with the unary decision predicate (Underscript[ϵ, D])  and a binary function \(+\+D\). Then Cartesian–Product[D], the application of the functor C to D, gives us a new domain, let's call it N for the moment, such that

(Underscript[∀ , X])((Underscript[ϵ, N])[
            X] ⇔ (is–tuple[
                X] ∧ (\[LeftBracketingBar]X\[RightBracketingBar] = 
                  2) ∧ (Underscript[ϵ, D])[(Subscript[X, 1])] ∧ (Underscript[ϵ, D])[
                (Subscript[X, 2])]))

where is–tuple is a fixed predicate that decides whether a given object is a tuple, i.e. an object of the form ⟨a1,...,an⟩ and |X | denotes the length of tuple X. In words: (Underscript[ϵ, N])[X], i.e. X  belongs to N, iff X is a tuple of length 2 and (Underscript[ϵ, D])[(Subscript[X, 1])], i.e. the first component of X belongs to D, and also (Underscript[ϵ, D])[(Subscript[X, 2])], i.e. the second component of X belongs to D. The information 𝕤= ⟨+∶ N×N->N⟩ tells us that + is a binary function on N, i.e. it provides the "signature" of the domain. In fact, this information is not really necessary. Consider it as an embellishment at the moment. You may also leave it out and, in fact, in this paper, we will not use this information. (The information is, however, necessary if one formulates functors that refer, for example, to "all unary functions" of the input domain etc.). If you introduce a signature information, do not believe, however, that an information like +∶N×N->N is a guarantee that the function  \(+\+N\) is indeed a binary function, i.e. maps objects satisfying (Underscript[ϵ, N]) to objects satisfying (Underscript[ϵ, N]). (Such a guarantee needs a proof like the proof of any other property you assert about the operations defined in N, see below.)

The definition

\(⟨x1, 
          x2⟩\( + \+N\)⟨y1, 
          y2⟩ = ⟨x1\( + \+D\)y1, 
        x2\( + \+D\)y2⟩\)

describes the fact that the operation \(+\+N\) in the new domain N is defined on tuples and is defined component-wised using the operation \(+\+D\) in D on the components. Note that the operation \(+\+N\) is intended to be defined on objects satisfying  (Underscript[ϵ, N]). However, as it stands, the operation will also give values on objects not satisfying (Underscript[ϵ, N]) but, typically, it will not be possible to prove anything on these values because, typically, nothing will be known on the values of \(x1\( + \+D\)y1\) and \(x2\( + \+D\)y2\) in case x1, y1, x2, y2 do not satisfy (Underscript[ϵ, D]).

Note that the Theorema functor construct can be conceived as an abbreviation of a predicate logic formula with a "such a quantifier" so that no new inference rules for fucntors are necessary. For example, the functor definition above can be conceived as an abbreviation of the following formula:

Cartesian–Product[D]=such an N that
∧{({{(Underscript[∀ , X])((Underscript[ϵ, N])[
                          X] ⇔ (is–tuple[
                              X] ∧ (\[LeftBracketingBar]X\[RightBracketingBar] = 2) ∧ (Underscript[ϵ, D])[(Subscript[X, 1])] ∧ (Underscript[ϵ, D])[
                              (Subscript[X, 2])]))}, {\(∀ \+\(x1, x2, y1, y2\)\((⟨x1, 
                            x2⟩\( + \+N\)⟨y1, 
                            y2⟩ = ⟨x1\( + \+D\)y1, x2\( + \+D\)y2⟩)\)\)}}) .

The 'X', 'x1', 'x2', 'y1', 'y2' are listed in the functor heading indicating that these variables are actually universally quantified over all formulae in the functor body.

Computing with the Functor

In Theorema, unsing defintions of operations and, in particular, defintions of functors, one can compute either in the frame of a "computational session" or in the frame of a "standard session". Computational sessions are organized very much in the way as Mathematica session, i.e. one enters definitions successively in input cells and the definitions are accumulated and used automatically, without any explicit indication, in all subsequent computations. In computational sessions, like in Mathematica sessions, one can only evaluate expressions using the previously entered definitions but one cannot call the Theorema provers for proving propositions. In contrast, in Theorema standard sessions, one can computer and prove and one has explicit control over the "knowledge bases" (i.e. the collection of formulae assumed to be true) used in evaluating and proving expressions.

We illustrate now for the above example functor, how one can call the functor in a typical computation in the frame of a Theorema standard session. (In the current version of Theorema, functors are not yet available in computational sessions.)

First of all, we have to initialize Theorema by executing (within Mathematica)

Needs["Theorema`"]

Now, we have to make available the functor definition for further use by giving it a label. This can be done by entering the  following Theorema construct into a Mathematica input cell:

Definition["Cartesian Product",any[D],
Cartesian–Product[D]=Functor[N,any[X, x1, x2, y1, y2],
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[
                              X] ⇔ (is–tuple[
                                  X] ∧ (\[LeftBracketingBar]X\[RightBracketingBar] = 2) ∧ (Underscript[ϵ, D])[(Subscript[X, 1])] ∧ (Underscript[ϵ, D])[
                                  (Subscript[X, 2])])}, {\(⟨x1, 
                                x2⟩\( + \+N\)⟨y1, 
                                y2⟩ = ⟨x1\( + \+D\)y1, x2\( + \+D\)y2⟩\)}})}})
	]]

Definition["Cartesian Product"]

Note that the "any[D]" construct declares 'D' as a variable.

We want to call now the functor for a concrete input domain. As an example, we compose the domain of integers by a degenerate functor with no input domain by entering:

Definition["Integer Numbers" ,any[],
Integer–Numbers[]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[x] ⇔ 
                            is–integer[x]}, {\(x\( + \+N\)y = x + y\)}})}})
	]]

Here, 'is–integer' and '+' should refer to the Mathematica operations 'IsInteger' and '+'. For enforcing this, we have the 'Built-in' construct in Theorema, which allows to access functions programmed in Mathematica from within Theorema in a controlled way. This means that, in any computation or proof, Theorema uses exclusively those operations that are either explicitly defined by a Theorema definition or are explicitly mentioned in a 'Built-in' declaration.

Now, we can compose the knowledge bases, which we need for enabling us to do computations in the Cartesian product of the domain of integers. For example, this can be organized as follows: Enter

Definition["Domains",
({{ℤ = Integer–Numbers[]}, {ℙ = 
                Cartesian–Product[ℤ]}})]

Next, we compose a knowledge base consisting of all the definitions relevant for computing in the domain of integers and in the Cartesion product thereof. This can be done by entering

Theory["T",
({{Definition["Cartesian Product"]}, {Definition["Integer Numbers"]}, {Definition["Domains"]}})]

Now we can evaluate arbitrary expressions over ℤ and ℙ using this theory and the built-in operations on (integer) numbers, tuples and propositional connectives. For example, if we enter

\(Compute[2\( + \+ℤ\)3, 
      using -> ⟨Built–in["Numbers"], 
          Built–in["Tuples"], Built–in["Connectives"], 
          Theory["T"]⟩]\)

we obtain

Also, entering

Compute[(Underscript[ϵ, ℤ])[3], 
      using -> ⟨Built–in["Numbers"], 
          Built–in["Tuples"], Built–in["Connectives"], 
          Theory["T"]⟩]

yields

Compute[(Underscript[ϵ, ℤ])[3.5], 
      using -> ⟨Built–in["Numbers"], 
          Built–in["Tuples"], Built–in["Connectives"], 
          Theory["T"]⟩]

\(Compute[ϵ\+ℤ[
        2\( + \+ℤ\)3], 
      using -> ⟨Built–in["Numbers"], 
          Built–in["Tuples"], Built–in["Connectives"], 
          Theory["T"]⟩]\)

\(Compute[⟨4, 
          7⟩\( + \+ℙ\)⟨2, 14⟩, 
      using -> ⟨Built–in["Numbers"], 
          Built–in["Tuples"], Built–in["Connectives"], 
          Theory["T"]⟩]\)

Of course, when the knowledge base which we want to use doese not change over a number of evaluations, it is quite inconvenient to mention the knowledge base explicitly in every evaluation. Therefore, we also have the possibility in Theorema to declare, in a standard session, that a certain knowledge base should be used in all the subsequent computations until a different knowledge base is declared:

Use[⟨Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Connectives"], 
        Theory["T"]⟩]

Now,

\(Compute[2\( + \+ℤ\)3]\)

and also

Compute[(Underscript[ϵ, ℤ])[3]]

Compute[(Underscript[ϵ, ℤ])[3.5]]

\(Compute[ϵ\+ℤ[
        2\( + \+ℤ\)3]]\)

\(Compute[⟨4, 
          7⟩\( + \+ℙ\)⟨2, 14⟩]\)

\(Compute[\((⟨4, 
              7⟩\( + \+ℙ\)⟨2, 
              14⟩)\)\( + \+ℙ\)⟨2, 
          2\( + \+ℤ\)3⟩]\)

Compute[(Underscript[ϵ, ℙ])[⟨-7, 
          18⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨-7, 
          18.5⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨-7, 
          18, 3⟩]]

Let's also try

Compute[(Underscript[ϵ, ℙ])[⟨x, 
          18⟩]]

Note that the answer is just a simplified version of

(is–tuple[⟨x, 
            18⟩] ∧ (\[LeftBracketingBar]⟨x, 18⟩\[RightBracketingBar] = 
            2) ∧ (Underscript[ϵ, ℤ])[⟨x, 18⟩_1] ∧ (Underscript[ϵ, ℤ])[⟨x, 18⟩_2])

for the constant x about which we have no knowledge: is–tuple[⟨x,18⟩] can be simplified to true also without any knowledge on x, also  ( |⟨ x, 18⟩| = 2) can be simplified to true without any knowledge on x. However, determining the truth value of  (Underscript[ϵ, D])[⟨x, 18⟩_1] needs the answer to the question whether (Underscript[ϵ, ℤ])[x], i.e. whether is–integer[x], which internally in Mathematica leads to calling IsInteger[x]. This cannot be decided because nothing is known about x.

Another Parameter Domain

Now let's define another domain by

Definition["Strange Numbers" ,any[],
Strange–Numbers[]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[x] ⇔ 
                            is–integer[x]}, {\(x\( + \+N\)y = x*y\)}})}})
	]]

and feed this domain into the functor Cartesian–Product for studying the dependence of the domain generated by a functor from the input domain.

Definition["Domains",
({{𝕊 = Strange–Numbers[]}, {ℙ = 
                Cartesian–Product[𝕊]}})]

Theory["T",
({{Definition["Cartesian Product"]}, {Definition["Strange Numbers"]}, {Definition["Domains"]}})]

Use[⟨Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Connectives"], 
        Theory["T"]⟩]

Now study and explain the results of each of the following evaluations:

\(Compute[2\( + \+𝕊\)3]\)

Compute[(Underscript[ϵ, 𝕊])[3]]

Compute[(Underscript[ϵ, 𝕊])[3.5]]

\(Compute[⟨4, 
          7⟩\( + \+ℙ\)⟨2, 14⟩]\)

\(Compute[\((⟨4, 
              7⟩\( + \+ℙ\)⟨2, 
              14⟩)\)\( + \+ℙ\)⟨2, 
          2\( + \+𝕊\)3⟩]\)

An Example Category and Conservation Theorem

Now let's define a trivial category in Theorema:

Definition["Commutid",any[D, ∘],
is–commutid[
              D, ∘]⇔∧{({{(Underscript[∀ , (Underscript[ϵ, D])[x, y]])(Underscript[ϵ, D])[
                      x(Underscript[∘, D])y]}, {(Underscript[∀ , (Underscript[ϵ, D])[x, y]])(x(Underscript[∘, D])y = y(Underscript[∘, D])x)}})} ]

In words: D is a "commutid" w.r.t. the operation ∘ in D iff, for all objects x and y belonging to D, x(Underscript[∘, D])y belong also to D and, for all objects x and y belonging to D, x(Underscript[∘, D])y is equal to y(Underscript[∘, D])x. Note again that, in this definition, 'D' and '∘' are free variables whereas 'is–commutatid' is a constant.

For getting acquainted with the underscript notation for operations in domains it is telling to look at

Definition["Commutid"]

which produces the definition in the internal prefix form of Theorema as a nested (Mathematica expression)

Note that, as range description of a quantifier, we can use (Underscript[ϵ, D])[x, y] as an abbreviation for (Underscript[ϵ, D])[x],(Underscript[ϵ, D])[y].

Now we can formulate, for example, the following conservation theorem:

Theorem["Cartesian Products of Commutids",any[D,∘],
is–commutid[D,∘]\[Implies]is–commutid[
            Cartesian–Product[D], ∘]]

It is the ultimate goal of Theorema to support the automated proof of such theorems (as any other theorems). Of course, the difficulty of such proofs depends on the semantic complexity of the formulae in the functors and category descriptions. Typically, the operations in (algorithmic) functors are defined by induction and the operations in algebraic categories, by definition, are expressed by equalities. However, in a general build-up of mathematics by functors and categories, the definitions of operations in category description may be arbitrary formulae. Hence, one has to expect that the (automated) proof of conservation theorems can be arbitrarily complex.

In fact, in the dissertation of my former PhD student Elena Tomuta, see [Tomuta 1998], the proof of simple conservation theorems on algebraic categories and simple functors were already generated automatically within Theorema. However, the implementation done in this dissertation is not any more integrated into the current version of Theorema. A new, expanded proof system for categories and functors, which at least sets up all the subproofs necessary for proving a conservation theorem and calls the appropriate subprovers, will soon be available in Theorema.

For explaining the typical structure of proofs of conservation theorems, let us do the proof of the Theorem["Cartesian Products of Commutids"] by hand:

Assume

is–commutid[D,∘],

i.e.

({{(Underscript[∀ , (Underscript[ϵ, D])[x, y]])(Underscript[ϵ, D])[
              x(Underscript[∘, D])y],, (A1)}, {(Underscript[∀ , (Underscript[ϵ, D])[x, y]])(x(Underscript[∘, D])y = 
                y(Underscript[∘, D])x),, (A2)}})

let

P = Cartesian–Product[D],

and show

is–commutid[P,∘],

i.e.

({{(Underscript[∀ , (Underscript[ϵ, P])[x, y]])(Underscript[ϵ, P])[
              x(Underscript[∘, P])y],, (G1)}, {(Underscript[∀ , (Underscript[ϵ, P])[x, y]])(x(Underscript[∘, P])y = 
                  y(Underscript[∘, P])x)., (G2)}})

Now assume

({{(Underscript[ϵ, P])[x],}, {(Underscript[ϵ, P])[y],}})

i.e. for certain x1, x2, y1, y2

({{x = ⟨x1, x2⟩,}, {(Underscript[ϵ, D])[x1],}, {(Underscript[ϵ, D])[x2],}, {y = ⟨y1, y2⟩,}, {(Underscript[ϵ, D])[x1],}, {(Underscript[ϵ, D])[x2],}})

and show

(Underscript[ϵ, P])[x(Underscript[∘, P])y].

Now,

(Underscript[ϵ, P])[x(Underscript[∘, P])y]  ↔ (Underscript[ϵ, P])[⟨x1, 
            x2⟩(Underscript[∘, P])⟨y1, 
            y2⟩]  ↔ (Underscript[ϵ, P])[⟨x1(Underscript[∘, D])y1, 
          x2(Underscript[∘, D])y2⟩]  ↔({{is–tuple[⟨x1(Underscript[∘, D])y1, 
                x2(Underscript[∘, D])y2⟩]}, {\[LeftBracketingBar]⟨x1(Underscript[∘, D])y1, x2(Underscript[∘, D])y2⟩ = 2\[RightBracketingBar]}, {(Underscript[ϵ, D])[x1(Underscript[∘, D])y1]}, {(Underscript[ϵ, D])[x2(Underscript[∘, D])y2]}})   (Overscript[↔ , by (A1)]) true.

Similarly, (G2) can be proved.

The Reduction Ring Approach to Groebner Bases

We introduced reduction rings as an approach to a Groebner bases theory that lends itself naturally to a domain / category / functor approach as early as 1983, see [Buchberger 1984]. An executable formulation of this approach is possible only now in Theorema, [Buchberger et al. 1997, 2000].

The main idea of the reduction ring approach to Groebner bases is the following: Instead of simply proving that Groebner bases can be computed in polyonomial rings over various coefficient domains (and then using Groebner bases for the solution of various fundamental problems in ideal theory as, for example, the ideal membership problem), we pursue an axiomatic approach. We add three operations to rings, namely a partial noetherian ordering >, a binary operation "reducing multiplier", and a binary operation "least common reducible". We call such rings "reduction rings". Then we show that all the operations necessary for constructing Groebner bases as, for example, partial and total reduction of ring elements, critical pairs and, finally, the critical pairs / completion (CPC) algorithm for constructing Groebner bases can be defined in terms of the ring operations and the three additional operations. Furthermore, we aim at proving that, if these operations satisfy certain axioms (i.e. belong to the category of "Groebner rings") then the CPC algorith, in fact, computes Groebner bases in the given ring (Groebner Ring Extension Theorem). Finally, we try to prove conservation theorems for various functors, i.e. we show that if certain rings are Groebner rings then the rings obtained from them by applying certain functors as, for example, the polynomial domain functor, are also Groebner rings.

This research program, so far, is only partially carried through and much work is still waiting to be done in this area. However, at least, it can be shown that arbitrary fields and the integers are Groebner rings and that the functor that generates polynomials with coefficients from a Groebner ring is also a Groebner ring.

In this paper, we carry this approach through in all details, as far as the computational aspect is concerned, using the functor mechanism of Theorema. Thus, the definitions in this notebook are executable. For a proof of a Groebner Ring Extension Theorem and a few conservation theorems see [Buchberger 1984] and  [Stifter 1987]. It is the aim of the Theorema projects that such proofs can be generated automatically or at least computer-supported in the future.

The three operations, that are added in reduction rings to the ordinary ring operations, have the following objective and significance:

The predicate >: This should be a Noetherian (partial) ordering (i.e. an ordering with no infinite descending chains), which interacts with the "reduction" process in the ring in such a way that the result of a reduction step yields a ring element which is < the ring element on which the recuction was applied.

The operation rdm "reducing multiplier": This is a binary function that, given two ring elements x and y, yields a ring element rdm[ x, y] such that x - rdm[ x, y] * y < x iff x is reducible modulo y. Here, '*' denotes multiplication in the ring. For everybody who is familiar with the basics of Groebner bases theory it should be clear that the operation rdm abstracts, for a very general class of rings, the essence of what happens in one reduction step in the important case of polynomial rings. In fact, rdm leaves a lot of freedom for organizing the reduction process and encompasses the essence of all possible reduction strategies.

The operation lcrd "least common reducible": This is the most important and subtle operation of the three. It extracts the essence of the construction of "S-poynomials" for rings whose elements are not necessarily polynomials. People who are familiar with the basics of Groebner bases theory know that the notion of S-polynomial is the crux of making Groebner bases theory algorithmic. Thus, the abstract notion of "least common reducible" is meant to formulate the key idea of algorithmic Groebner bases theory in quite general and abstract terms: Given two ring elements x and y, the least common reducible lcrd[ x, y] is such a common reducible of x and y that no smaller (w.r.t. to <) common reducible of x and y exists. A common reducible of x and y is a ring element z such that z is reducible both modulo x and modulo y, i.e.  z - rdm[ z, x] * x < z and  z - rdm[ z, y] * y < z. Thus, Z: = lcrd[ x, y] is an element that provides a chance for being reduced to irreduble elements in two essentially different ways, namely by going from Z to (Subscript[Z, 1]):= Z - rdm[ Z, x] * x and then further on to an irreducible element a and by going from Z to (Subscript[Z, 2]) := Z - rdm[ Z, y] * y and then further on to an irreducible element b. Then, the check whether a = b is the crucial check in the Groebner basis algorithm. (Equivalently, one can start from the "S-element" (Subscript[Z, 1]) - (Subscript[Z, 2]) and check whether it reduces to 0.) In fact, the above sketch of the intuition behind the notion of "least common reducible" is not really general enough to encompass all interesting cases: Before forming the "least common reducible" one has to single out the "non-trivial common reducibles". The details of this are quite subtle and we have to refer the reader to the paper [Buchberger 1984] in which this approach has been introduced.

It is interesting to analyze what lcrd[ x, y] is in the important case of polynomials: It turns out that, given two monic polynomials, lcrd[ x, y]  is exactly the least common multiple of the leading power products of x and y. In case the polynomials are not monic, lcrd[ x, y] is the least common multiple of the leading power products of x and y multiplied with the least common reducible of the leading coefficients of x and y.  Thus, in the case of polynomial rings, lcd[ r, y] is the expected well-known first step in the construction of the "S-polynomial" of x and y. (All this is true only if we first dismiss the "trivial common reducibles" of two power products, which would be just the sum of the two power products!)

It is even also interesting  to analyze what lcrd[ x, y] is in the case of the integers: We will discuss this subtle question in the section on the domain of reduction integers, where we expand the ring of integers by the three appropriate operations <, rdm, and lcrd. (Note that for '<' we can not take the ordinary less relation, which would not be Noetherian!)

It is relatively easy to analyze what lcrd[ x, y] is in the case of fields: Here, the operation rdm is particularly simple because every field element can be reduced modulo any other (non-zero) element to 0 in one step. For the details, see the section on reduction fields.

Preparation of Theorema

The Objective of this Section

In this section, we carry out a couple of technical steps for preparing Theorema for the tasks to be carried out in this notebook. First of all, start with a new Mathematica kernel by quitting the kernel using the appropriate line in the Mathematica menu.

A Word on Computation and Complexity in Theorema

The Theorema language, which is essentially a version of predicate logic, contains as a part a programming language. All the algorithms and the functors (bundles of algorithms) contained in this notebook can therefore be read as both predicate logic statements and also as executable programs. The execution can be viewed as the application of the substitution and replacement inference rules of predicate logic plus straight-forward computational interpretations of the bounded quantifiers like (Underscript[∀ , i = 1,  ... , n])...  etc.

It is important to know that Theorema is implemented in the Mathematica language and, hence, we can not expect that algorithms expressed in Theorema can be executed faster than what would be possible with the corresponding algorithms expressed in Mathematica. As a matter of fact, it is known that algorithms expressed and executed in Mathematica are very slow, roughly a factor 1000 slower than the equivalent algorithms in, say, C or Java, see [Buchberger 1991] for some timing experiments. (This should not be misunderstood as saying that the functions like 'Factor' available in the Mathematica library are slow. The library functions of Mathematica are written in C and not in the Mathematica language and,  therefore, these algorithms are fast. What we say here is that functions programmed by the Mathematica user in the Mathematica language have high execution times. For example, write a little Mathematica program that adds two lists componentwise and compare the execution time with that of the built-in addition on lists and you will see what we mean here.)

As a result, we cannot expect that the functors and algorithms in the functors which we compose in this notebook are meant for practical problem solving. The goal of this paper is not computational efficiency but a clear logic analysis of the possibility to have, within the same logic and language and system frame,

generality, structuredness and elegance of towers of domains and executable algorithms

and the possibility of proving properties of these algorithms.

Thus, don't be shocked if even very simple examples like the computation of greatest common divisors of tuples of integers by the Groebner basis algorithm in the general, functor oriented description in this paper may take a couple of seconds instead of a few milliseconds in the C implemetation of Euclid's algorithm within Mathematica or any other system.

We will consider speed in a later stage of the Theorema project when we will have clarified the logical frame of domain oriented and provenly correct computation within the current, slow Theorema system. Of course, for speeding the system up, we will have to give up the idea of using Mathematica as an implementation language for the computational part of Theorema. We may still want to keep Mathematica as the implementation language for the logic part of Theorema, i.e. the implementation of provers, solvers, and simplifiers.

Additional Mathematica Functions

Clear[PFInverse, PFQuotient]
PFInverse[x_, 
        p_] := ExtendedGCD[x, p][[2, 1]]
PFQuotient[x_, y_, p_] := Mod[x PFInverse[y, p], p]

PFQuotient[1, 1, 5]

PFQuotient[1, 2, 5]

PFQuotient[1, 3, 5]

PFQuotient[1, 4, 5]

PFQuotient[2, 1, 5]

PFQuotient[2, 2, 5]

PFQuotient[2, 3, 5]

PFQuotient[2, 4, 5]

PFQuotient[3, 1, 5]

PFQuotient[3, 2, 5]

PFQuotient[3, 3, 5]

PFQuotient[3, 4, 5]

PFQuotient[4, 1, 5]

PFQuotient[4, 2, 5]

PFQuotient[4, 3, 5]

PFQuotient[4, 4, 5]

Start Theorema

Now we start Theorema again by executing

Needs["Theorema`"]

Correction

In the current version of Theorema, the following Mathematica function defintion must be entered

\[LeftBracketingBar]⟨x___?
            IsSequenceFree⟩\[RightBracketingBar] := 
      Length[{x}]

for completing a definition in the Theorema package.

Make Mathematica Functions Accessible

The following Theorema command attaches certain Theorema names to certain Mathematica functions and makes them available for calls from within Theorema. (Note that all other functions from the Mathematica function library are hidden from Theorema. If you want more Mathematica functions to be accessible from within Theorema you should introduce them by a similar "Built-in" command.)

Built–in["Mathematica general functions",
({{is–even -> EvenQ}, {is–odd -> OddQ}, {mod -> Mod}, {gcd -> GCD}, {lcm -> LCM}, {sign -> Sign}, {maximum -> Max}, {quotient -> Quotient}, {pf–inverse -> PFInverse}, {pf–quotient -> PFQuotient}})]

Some Basic Functions Programmed in Theorema

The following function 'pairs' computes a list consisting of all pairs of elements in a given list:

Definition["Theorema general functions",\(any[a, x, x\&_]\),
({{pairs[⟨⟩] = ⟨⟩}, {\(pairs[⟨x, 
                    x\&_⟩] = ⟨\(⟨x, ⟨x\&_⟩\_i⟩\)\( \[VerticalSeparator] \+\(i = 
                            1, …, \[LeftBracketingBar]⟨x\&_⟩\[RightBracketingBar]\)\)⟩ ≍ 
                  pairs[⟨x\&_⟩]\)}})]

For example

Use[⟨Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Connectives"], 
        Built–in["Quantifiers"], 
        Definition["Theorema general functions"]⟩]

Compute[ pairs[⟨⟩]]

Compute[ pairs[⟨1⟩]]

Compute[ 
      pairs[⟨1, 2, 3, 4, 5⟩]]

Compute[ 
      pairs[⟨1, 2, 1, 1, 2⟩]]

The Rationals in Decimal Representation as Field

Informal Explanation

We define a functor "rational numbers field" that constructs the domain of rational numbers in decimal notation in Theorema. From which material can we construct the operations in the resulting domain? We could do this by starting from nothing, i.e. from only predicate logic, by introducing some version of the natural numbers (from a constant 0 and a successor function s), then by defining (by a functor) pairs of natural numbers (with pairs defined in predicate logic) equipped with componentwise operations and a congruence relation, then by defining the integers (by applying a residue domain functor), then by defining (by a functor) pairs of integers equipped with componentwise operations and a congruence relation, then by defining the rationals (by applying again a residue domain functor).

Alternatively, in this paper, we start from material which is already available in the underlying Mathematica: The rational numbers in decimal notation together with the arithmetical operations. In order to make these Mathematica operations accessible from within Theorema we have the "Built-in" construct in Theorema that does not only allow to assign Theorema names to individual Mathematica functions as we have seen in the previous section but allows also to access, under one label, whole groups of Mathematica operations, as for example all Mathematica operations on all types of numbers. For example, the following constructs

Built–in["Numbers"]

Built–in["Tuples"]

Built–in["Sets"]

Built–in["Quantifiers"]

Built–in["Connectives"]

refer to boundles of operations on numbers, on tuples, and on sets, and also to the evaluation of quantifiers with bounded ranges and to the evaluation of the usual propositional connectives.

In order to access these boundles of operations in Theorema, one can start their accessibility by calling them individually like, for example,

\(Use[⟨Built–in["Numbers"]⟩]\)

or collectively, like

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], 
        Built–in["Sets"]⟩]

in which case these operations are available in all subsequent evaluations, i.e. calls of the function Compute[ expression], where 'expression' is the expression to be evaluated. Alternatively, one can make groups of Mathematica operations accessible by including a 'using ->' optional parameter into the Compute call. For example,

Compute[ 2 + 3,  
      using -> Built–in["Numbers"]]

or

Compute[ ⟨2 + 3, 3 + 4⟩,  
      using -> ⟨Built–in["Numbers"], 
          Built–in["Tuples"]⟩]

If you want to see which Mathematica functions are accessible by Built–in["Numbers"] just evaluate

Built–in["Numbers"]

and you get the list of all functions in that bundle:

Definition

The following functor defines now all the operations for the domain of rational number in the usual decimal representation of Mathematica considered as a field. Hence, it just takes the constants 0 and 1 and the operations +, -, *, /. Also, we define the unary characterization predicate ϵ which refers to a Theorema built–in function 'is–rational' that decides whether or not a Mathematica expression denotes a rational number with enumerator and denominator in decimal representation.

Definition["rational numbers field" ,any[],
rational–numbers–field[]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                              x] ⇔ 
                            is–rational[x]}, {(Underscript[0, N]) = 0}, {(Underscript[1, N]) = 1}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {(Underscript[inverse, N])[x] = 1/x}, {\(x\(/\+N\)y = x/y\)}})}})
	]]

Examples

Theory

Definition["ℚ0", ℚ0 = 
        rational–numbers–field[]]

Note that the constant denoting the result of applying the functor 'rational–numbers–field' is, of course, completely arbitrary. Whe chose here the constant 'ℚ0' instead of the usual 'ℚ' because we want to emphasize that ℚ0 denotes the domain of rationals equipped with only the field opertaions.

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["ℚ0"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Field Operations

Compute[(Underscript[ϵ, ℚ])0[2.0005]]

Compute[(Underscript[ϵ, ℚ])0[2/5]]

Compute[(Underscript[0, ℚ])0]

Compute[(Underscript[1, ℚ])0]

\(Compute[5/2\( + \+ℚ0\)3]\)

\(Compute[\(-\+ℚ0\(-2\)\)/3]\)

\(Compute[3\( - \+ℚ0\)\(-2\)/3]\)

\(Compute[5\(*\+ℚ0\)3/4]\)

Compute[(Underscript[inverse, ℚ])0[3/4]]

\(Compute[\(7/
          5\)\(/\+ℚ0\)\((\(-2\)/3)\)]\)

\(Compute[\(7/5\)\(/\+ℚ\)\((\(-2\)/3)\)]\)

Domains Modulo a Prime as Fields

Definitions

Definition["prime field" ,any[p],
prime–field[p]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                                  x]⇔∧{({{is–integer[x]}, {0 ≤ x}, {x < p}})} }, {(Underscript[0, N]) = 0}, {(Underscript[1, N]) = 1}, {\(x\( + \+N\)y = mod[x + y, p]\)}, {\(\(-\+N x\) = mod[\(-x\), p]\)}, {\(x\( - \+N\)y = mod[x - y, p]\)}, {\(x\(*\+N\)y = mod[x*y, p]\)}, {(Underscript[inverse, N])[x] = pf–inverse[x, p]}, {\(x\(/\+N\)y = pf–quotient[x, y, p]\)}})}})
	]]

Remark on the operations in the functor: (Underscript[inverse, N]) and \(\(/\+N\)\) refer to the function pf–inverse and pf–quotient, respectively, which we linked to the Mathematica function PFInverse and PFQuotient by the 'Built-in' construct. PFInverse and PFQuotient were defined in the section "Preparation of Theorema".

Examples

Theory

Definition["𝔽5", 𝔽5 = 
        prime–field[5]]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["prime field"]}, {Definition["𝔽5"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Arithmetic

Compute[(Underscript[ϵ, 𝔽])5[0]]

Compute[(Underscript[ϵ, 𝔽])5[4]]

Compute[(Underscript[ϵ, 𝔽])5[5]]

Compute[(Underscript[ϵ, 𝔽])5[-1]]

Compute[(Underscript[0, 𝔽])5]

Compute[(Underscript[1, 𝔽])5]

\(Compute[4\( + \+𝔽5\)1]\)

\(Compute[\(-\+𝔽5\((2)\)\)]\)

\(Compute[1\( - \+𝔽5\)\((2)\)]\)

\(Compute[4\(*\+𝔽5\)3]\)

Compute[(Underscript[inverse, 𝔽])5[3]]

\(Compute[4\(/\+𝔽5\)3]\)

Reduction Fields

Informal Explanation

We now start from an arbitrary field and extend it by three additional operations >, rdm, and lcrd in order to make a reduction ring out of the field. How can this be done?

First of all note that in a field an element x≠0 can be reduced to 0 by any element y (≠0) by subtracting  (x / y) * y. Hence, the appropriate rdm can be defined by rdm[ x, y] := x / y. Now, the result  0 = x - rdm[ x, y] * y should be smaller, w.r.t. >, than x. Hence, the appropriate definition of > is that x > y iff ( x ≠0 and y=0). Note that, in the case of the rationals, this > is different from the usual > and that this new > is trivially Noetherian whereas the usual > is not Noetherian. Finally, we have to invent the appropriate lcrd: Given two rationals x and y, both ≠0, any rational z≠0 can be reduced to 0 by x as well as by y and no smaller z' (w.r.t. to our new >) has the same property. Hence, we can take any rational ≠0 as the lcrd[ x, y]. We choose lcrd[ x, y] := 1.

We also use the extension functor for getting rid of the multiplicative inverse and quotient because, in the context of reduction rings, we consider the domain as a ring only.

For extending a domain by new operations, in principle, we have an extra language construct in Theorema, the "extension functors". However, in the current version, this construct is not working properly. Therefore, in this notebook, we use the general functors for effecting extensions: We just carry over the characteristic predicate ϵ of the domain and all the operations of the old domain D to the new domain N by definitions of the form

\(x\( + \+N\)y = x\( + \+D\)y\)

and then we define the new operations in N in terms of the known operations in D.

Definition

Definition["reduction field" ,any[D],
reduction–field[D]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                              x] ⇔ (Underscript[ϵ, D])[
                              x]}, {(Underscript[0, N]) = (Underscript[0, D])}, {(Underscript[1, N]) = (Underscript[1, D])}, {\(x\( + \+N\)y = x\( + \+D\)y\)}, {\(\(-\+N x\) = \(-\+D x\)\)}, {\(x\( - \+N\)y = x\( - \+D\)y\)}, {\(x\(*\+N\)y = x\(*\+D\)y\)}, {\(\(x\( > \+N\)y ⇔ \((\((x ≠ 0\+D)\) ∧ \((y = 0\+D)\))\)\)\(
\)
                          \)}, {(Underscript[rdm, N])[x, y]     ={({{\(x\(/\+D\)y\), ⇐, x ≠ 
                                        (Underscript[0, D]) ∧ y ≠ (Underscript[0, D])}, {(Underscript[0, D]), ⇐, otherwise}})} }, {(Underscript[lcrd, N])[x, y]    ={({{(Underscript[1, D]), ⇐, x ≠ 
                                        (Underscript[0, D]) ∧ y ≠ (Underscript[0, D])}, {(Underscript[0, D]), ⇐, otherwise}})}}})}})
	]]

Remarks on the operations in the functor: (Underscript[rdm, N]) is defined for all field elements x and y. For the inputs x and y for which no reduction is possible (Underscript[rdm, N])[ x, y] is defined to be zero. By this, it is guaranteed that x is reducible modulo y iff x - (Underscript[rdm, N])[ x, y] * y \(TraditionalForm\`\( < \+N\)\) x. Similarly, (Underscript[lcrd, N])[x, y] is defined for all field elements x and y.

Examples

Theory

Definition["Domains",
({{ℚ0 = 
                rational–numbers–field[]}, {ℚ△ = 
                reduction–field[ℚ0]}, {𝔽5 = prime–field[5]}, {𝔽5△ = 
                reduction–field[𝔽5]}})]

Again, the constant denoting the result of applying the functor rdrat is, of course, completely arbitrary. We chose here the constant 'ℚ△' instead of the usual 'ℚ' because we want to emphasize that ℚ△ denotes the domain of rationals viewed as a reduction ring and not the ordinary domain of rationals viewed as a field.

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["prime field"]}, {Definition["reduction field"]}, {Definition["Domains"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Ring Operations

Compute[(Underscript[ϵ, ℚ])0[2.0005]]

Compute[(Underscript[ϵ, ℚ])△[
        2.0005]]

Compute[(Underscript[ϵ, ℚ])△[
        2/3]]

Compute[(Underscript[ϵ, 𝔽])5[6]]

Compute[(Underscript[ϵ, 𝔽])5△[
        4]]

Compute[(Underscript[0, ℚ])△]

Compute[(Underscript[0, 𝔽])5△]

Compute[(Underscript[1, ℚ])△]

Compute[(Underscript[1, 𝔽])5△]

\(Compute[
      5/2\( + \+ℚ△\)3]\)

\(Compute[
      4\( + \+𝔽5△\)3]\)

\(Compute[\(-\+ℚ△\(-2\)\)/
        3]\)

\(Compute[
      5/2\( - \+ℚ△\)3]\)

\(Compute[
      2\( - \+𝔽5△\)3]\)

\(Compute[
      5\(*\+ℚ△\)3/4]\)

\(Compute[4\(*\+𝔽5△\)4]\)

\(Compute[
      5\(/\+ℚ△\)\(3/4\)]\)

The operation / is not any more available in the reduction ring ℚ△ !

\(Compute[3\(/\+𝔽5△\)2]\)

Additional Operations

\(Compute[
      5/2\( > \+ℚ△\)3]\)

\(Compute[
      5/2\( > \+ℚ△\)0]\)

\(Compute[
      0\( > \+ℚ△\)0]\)

\(Compute[
      4\( > \+𝔽5△\)3]\)

\(Compute[
      4\( > \+𝔽5△\)0]\)

Compute[
      (Underscript[rdm, ℚ])△[3, 2]]

Compute[
      (Underscript[rdm, 𝔽])5△[3, 2]]

Compute[
      (Underscript[rdm, 𝔽])5△[0, 2]]

Compute[
      (Underscript[rdm, 𝔽])5△[3, 0]]

Compute[
      (Underscript[lcrd, ℚ])△[3, 2]]

Compute[
      (Underscript[lcrd, 𝔽])5△[3, 2]]

Compute[
      (Underscript[lcrd, 𝔽])5△[3, 0]]

The Integers Viewed as a Reduction Ring

Informal Explanation

The ordinary integers in decimal representation are a ring. We add three operations >, rdm, and lcrd in order to make a reduction ring out of the integers. We now the informal ideas behind the formal definitions of these three operations.

The usual > relation in the integers is not Noetherian. We define, therefore a new relation > by saying that y > x if the absolute value of x is greater (in the ordinary sense) than the absolute value of x. Note that the new ordering is Noetherian but only partial.

Now it is clear that, for positive x and y, rdm[ x, y] can be chosen 1 if |x| ≥ |y| . Thus, for example, 17 can be reduced to 12 modulo 5. However, for example, 2 cannot be reduced any further modulo 5, i.e. we will take rdm[ 2, 5] := 0. (We take rdm[ x, y] = 0 iff x cannot be reduced modulo y. With this setting rdm[ x, y] can also be used as an irreducibility test!) For arbitrary (positive and negative) x and y we set rdm[ x, y] = sign[ x] sign[ y] rdm[ |x|, |y|].

lcrd[ x, y] for positive integers is just the maximum of x and y.

Of course, in the case of the integers in decimal representation (or a representation in any positional system), we can take as rdm[ x, y] the quotient of x and y.  The quotient is nothing else than the number of repeated subtraction steps until we reach an irreducible element. This is of course much more efficient than repeating the subtraction steps. We will implement both approaches. (The approach using subtraction instead of the quotient is more general because, when reducing an integer modulo a tuple of integers, it allows to use various reducing integers in a mixed strategy.)

In fact, whenever we have a reduction ring with some operation rdm[ x, y], we always could go over to another reduction ring having the same operations except that a new rdm'[ x, y] could be defined that produces an irreducible element in just one step. We might consider this construction as a functor but it should be clear that, by doing this, we loose generality for the reduction process modulo several y.

Definition

Definition["reduction integers" ,any[],
reduction–integers[]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[x] ⇔ 
                            is–integer[x]}, {(Underscript[0, N]) = 0}, {(Underscript[1, N]) = 1}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {\(\(x\( > \+N\)y ⇔ \[LeftBracketingBar]x\[RightBracketingBar] > \[LeftBracketingBar]y\[RightBracketingBar]\)\(
\)
                          \)}, {(Underscript[rdm, N])[x, y]   (* 
                              a reduction multiplier of x modulo y  *)   = sign[x] sign[ y] 
                              rdmp[\[LeftBracketingBar]x\[RightBracketingBar], \[LeftBracketingBar]y\[RightBracketingBar]]

                           }, {rdmp[x, y]     =
{({{1, ⇐, ∧{({{x ≥ y}, {y > 0}})} }, {0, ⇐, otherwise}})
} }, {(Underscript[lcrd, N])[x, y]  (* 
                              the least common reducible of x and y  *)  =maximum[\[LeftBracketingBar]x\[RightBracketingBar], \[LeftBracketingBar]y\[RightBracketingBar]] }})}})

	]]

Some remarks on the operations in this functor:

Note that the functions rdmp and lrd are not one of the three additional operations necessary in reduction rings but they are just auxiliary functions on the way to defining (Underscript[rdm, N]) and (Underscript[lcrd, N]). The auxiliary functions do not carry the underscript N and, hence, are not available outside the functor!

Now we define a slightly more restricted but more efficient version of this functor:

Definition["reduction integers by quotient" ,any[],
reduction–integers–by–quotient[]=Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[x] ⇔ 
                            is–integer[x]}, {(Underscript[0, N]) = 0}, {(Underscript[1, N]) = 1}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {\(\(x\( > \+N\)y ⇔ \[LeftBracketingBar]x\[RightBracketingBar] > \[LeftBracketingBar]y\[RightBracketingBar]\)\(
\)
                          \)}, {(Underscript[rdm, N])[x, y]   (* 
                              a reduction multiplier of x modulo y  *)   = sign[x] sign[ y] 
                              rdmp[\[LeftBracketingBar]x\[RightBracketingBar], \[LeftBracketingBar]y\[RightBracketingBar]]

                           }, {rdmp[x, y]     =
{({{quotient[x, y], ⇐, ∧{({{x ≥ y}, {y > 0}})} }, {0, ⇐, otherwise}})
} }, {(Underscript[lcrd, N])[x, y]  (* 
                              the least common reducible of x and y  *)  =maximum[\[LeftBracketingBar]x\[RightBracketingBar], \[LeftBracketingBar]y\[RightBracketingBar]] }})}})

	]]

Examples

Theory

\(Definition["ℤ△", ℤ△ = 
        reduction–integers[]]\)

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["reduction integers"]}, {Definition["ℤ△"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Arithmetic

Compute[(Underscript[ϵ, ℤ])△[
        2]]

Compute[(Underscript[ϵ, ℤ])△[
        2.5]]

Compute[(Underscript[ϵ, ℤ])△[
        2/5]]

Compute[(Underscript[0, ℤ])△]

Compute[(Underscript[1, ℤ])△]

\(Compute[
      5\( + \+ℤ△\)3]\)

\(Compute[\(-\+ℤ△\(-2\)\)]\)

\(Compute[
      5\( - \+ℤ△\)3]\)

\(Compute[5\(*\+ℤ△\)3]\)

Additional Operations

\(Compute[
      4\( > \+ℤ△\)3]\)

\(Compute[
      3\( > \+ℤ△\)3]\)

\(Compute[
      3\( > \+ℤ△\)\(-3\)]\)

\(Compute[\(-3\)\( > \+ℤ△\)3]\)

Compute[-3 = 3]

Hence, 3 and -3 are incomparable w.r.t. \(\( > \+ℤ△\)\).

\(Compute[\(-3\)\( > \+ℤ△\)2]\)

\(Compute[
      2\( > \+ℤ△\)\(-3\)]\)

Compute[
      (Underscript[rdm, ℤ])△[3, 3]]

Compute[
      (Underscript[rdm, ℤ])△[3, 4]]

Compute[
      (Underscript[rdm, ℤ])△[3, -4]]

Compute[
      (Underscript[rdm, ℤ])△[-3, 4]]

Compute[
      (Underscript[rdm, ℤ])△[-3, -4]]

Compute[
      (Underscript[rdm, ℤ])△[2, 4]]

Compute[
      (Underscript[rdm, ℤ])△[2, -4]]

Compute[
      (Underscript[lcrd, ℤ])△[5, 5]]

Compute[
      (Underscript[lcrd, ℤ])△[6, 6]]

Compute[
      (Underscript[lcrd, ℤ])△[6, 5]]

Compute[
      (Underscript[lcrd, ℤ])△[5, -6]]

Compute[
      (Underscript[lcrd, ℤ])△[-5, 6]]

Compute[
      (Underscript[lcrd, ℤ])△[-5, -6]]

Compute[
      (Underscript[lcrd, ℤ])△[-10, -10]]

Compute[
      (Underscript[lcrd, ℤ])△[-10, 5]]

Division Semigroup in Tuples Representation with Lexical Ordering

Informal Explanation

In the preceding sections we built up a couple of basic rings which may play the role of coefficient domains in polynomial domains. Before we can go to describing a functor that builds up polynomial domains from coefficient domains and domains of "power products" ("terms") we introduce two concrete power product domains so that we can consider concrete examples of using the functor that builds up polynomial domains.

On the domain of  power products addition (subtraction) is not defined. Power products do not form a ring. Therefore, there is no natural notion of reduction multiplier in the domain of power products, because we cannot form  x - rdm[x,y]*y ! Hence, it is better not to introduce an extra domain "reduction tuples" but to define the domain reduction polynomials directly from a coefficient domain that is a reduction ring and from a domain of power products which is not a reduction domain but has some other minimal structure. We will see in the section on reduction polynomials, which structure is sufficient for the power product domain. We call this structure a "division semigroup".

We use here a special representation of power products, which is very common in computer algebra: (Subscript[((Subscript[x, 1])^i), 1]) ...  (Subscript[((Subscript[x, n])^i), n])is represented by the tuple of exponents ⟨(Subscript[i, ]),  ... , 
        (Subscript[i, n])⟩. Note, however, that the functor that constructs reduction rings from coefficient domains and division semigroups is completely general and works for all (representations of) division semigroups. This is exactly what we have in mind when we use functors!

Definitions

Definition["tuples division semigroup lexical",any[k, D],
tuples–division–semigroup–lexical[k]   =
Functor[N,\(any[m, m\&_, n, n\&_, x, y, i]\),
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[
                                x]⇔∧{({{is–tuple[x]}, {\[LeftBracketingBar]x\[RightBracketingBar] = k}, {(Underscript[∀ , i = 
                                        1, …, k])∧{({{is–integer[(Subscript[x, i])]}, {(Subscript[x, i]) ≥ 0}})} }})} }, {(Underscript[1, N]) = ⟨0 (Underscript[\[VerticalSeparator] , i = 1, …, k])⟩}, {\(x\(*\+N\)y = ⟨\(x\_i + 
                                  y\_i\)\( \[VerticalSeparator] \+\(i = 
                                      1, …, 
                                    k\)\)⟩\)}, {\(x\(/\+N\)y = ⟨\(x\_i - 
                                  y\_i\)\( \[VerticalSeparator] \+\(i = 
                                      1, …, 
                                    k\)\)⟩\)}, {(x  (Underscript[∣ , N])y)⟺(Underscript[∀ , i = 1, …, k])(Subscript[x, i]) ≤ (Subscript[y, i])}, {(Underscript[lcm, N])[x, y]     = ⟨maximum[(Subscript[x, i]), 
                                  (Subscript[y, i])] (Underscript[\[VerticalSeparator] , i = 
                                      1, …, 
                                    k])⟩}, {\(⟨⟩\( > \+N\)⟨⟩ ⇔ False\)}, {\(⟨m, 
                                m\&_⟩\( > \+N\)⟨n, n\&_⟩\)⇔{({{True, ⇐, m > n}, {\(⟨m\&_⟩\( > \+N\)⟨n\&_⟩\), ⇐, (m = n)}, {False, ⇐, otherwise}})} }, {(Underscript[deg, N])[x]  (* 
                              the degree of x *)  = (∑_(i = 1, …, k))(Subscript[x, i])}})}})
	]]

Note: ' (Underscript[∣ , N])' must be typed '\ [VerticalBar]'.

In the above definition, we use the tuple quantifier \(⟨\(...\)\(\(\(|\)\(\ \)\(...\)\)\+\(i = 1, …, k\)\)⟩\): For example,

⟨maximum[(Subscript[x, i]), 
          (Subscript[y, i])] (Underscript[\[VerticalSeparator] , i = 1, …, 
            k])⟩

is the tuple of length k having the element maximum[(Subscript[x, i]), (Subscript[y, i])] at its i-th position. Note that the tuple quantifier is different from the set quantifier, Thus, for example,

{maximum[(Subscript[x, i]), 
          (Subscript[y, i])] (Underscript[\[VerticalSeparator] , i = 1, …, 
            k])}

may be a set of fewer than k elements (in case some of the maximum[(Subscript[x, i]), (Subscript[y, i])] coincide).

Examples: Length = 3

Theory

Definition[\("𝕋3", 
	𝕋3 = 
        tuples–division–semigroup–lexical[3]\)]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["tuples division semigroup lexical"]}, {Definition["𝕋3"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Operations

Compute[(Underscript[ϵ, 𝕋])3[⟨1, 0, 
          2⟩]]

Compute[(Underscript[ϵ, 𝕋])3[⟨1, 
          0, -2⟩]]

Compute[(Underscript[ϵ, 𝕋])3[⟨1, 0, 
          2, 4⟩]]

Compute[(Underscript[1, 𝕋])3]

\(Compute[⟨1, 2, 
          4⟩\(*\+𝕋3\)⟨2, 0, 2⟩]\)

Compute[⟨0, 0, 
          0⟩ (Underscript[∣ , 𝕋])3⟨0, 0, 0⟩]

Compute[⟨0, 4, 
          1⟩ (Underscript[∣ , 𝕋])3⟨0, 5, 3⟩]

Compute[⟨0, 4, 
          4⟩ (Underscript[∣ , 𝕋])3⟨0, 5, 3⟩]

Compute[⟨0, 5, 
          1⟩ (Underscript[∣ , 𝕋])3⟨0, 5, 0⟩]

\(Compute[⟨55, 2, 
          4⟩\(/\+𝕋3\)⟨2, 0, 2⟩]\)

Compute[
      (Underscript[lcm, 𝕋])3[⟨55, 2, 
          4⟩, ⟨2, 0, 
          2⟩]]

Compute[
      (Underscript[lcm, 𝕋])3[⟨55, 2, 
          4⟩, ⟨2, 20, 
          9⟩]]

\(Compute[⟨55, 2, 
          4⟩\( > \+𝕋3\)⟨2, 0, 2⟩]\)

\(Compute[⟨55, 2, 
          4⟩\( > \+𝕋3\)⟨55, 2, 4⟩]\)

\(Compute[⟨55, 2, 
          4⟩\( > \+𝕋3\)⟨55, 3, 4⟩]\)

\(Compute[⟨55, 3, 
          4⟩\( > \+𝕋3\)⟨55, 3, 3⟩]\)

\(Compute[⟨55, 3, 
          4⟩\( > \+𝕋3\)⟨55, 3, 2342⟩]\)

Compute[
      (Underscript[deg, 𝕋])3[⟨55, 3, 
          4⟩]]

Division Semigroup with Degree Ordering

Informal Explanation

We next define a functor that, given a division semigroup D with an ordering \(TraditionalForm\`\( > \+D\)\) and a degree function (Underscript[deg, D]), changes the ordering into an ordering \(TraditionalForm\`\( > \+N\)\) that first orders by the degree and then uses \(TraditionalForm\`\( > \+D\)\) for ordering within a degree.

Definitions

Definition["division semigroup degree ordered" ,any[D],
division–semigroup–degree–ordered[
              D ]   =
Functor[N,any[x, y],
	({{𝕤 = ⟨⟩}, {
({{(Underscript[ϵ, N])[
                                  x] ⇔ (Underscript[ϵ, D])[
                                  x]}, {(Underscript[1, N]) = (Underscript[1, D])}, {\(x\(*\+N\)y = x\(*\+D\)y\)}, {\(x\(/\+N\)y = x\(/\+D\)y\)}, {x  (Underscript[∣ , N])y ⇔ x  (Underscript[∣ , D])y}, {(Underscript[lcm, N])[x, y] = (Underscript[lcm, D])[x, y]}, {\(x\( > \+N\)y\)⇔where[d = (Underscript[deg, D])[x],e = (Underscript[deg, D])[y], ∨{({{d > e}, {∧{({{d = e}, {\(x\( > \+D\)y\)}})} }})} ]}})}}) 
	]]

Examples

Theory

Definition["𝕋3d",
	({{𝕋3l = 
                tuples–division–semigroup–lexical[3]}, {𝕋3d = 
                division–semigroup–degree–ordered[𝕋3l]}})]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["tuples division semigroup lexical"]}, {Definition["division semigroup degree ordered"]}, {Definition["𝕋3d"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Operations

Compute[(Underscript[ϵ, 𝕋])3d[⟨1, 0, 
          2⟩]]

Compute[(Underscript[ϵ, 𝕋])3d[⟨1, 
          0, -2⟩]]

Compute[(Underscript[ϵ, 𝕋])3d[⟨1, 0, 
          2, 4⟩]]

Compute[(Underscript[1, 𝕋])3d]

\(Compute[⟨1, 2, 
          4⟩\(*\+𝕋3d\)⟨2, 0, 2⟩]\)

Compute[⟨0, 0, 
          0⟩ (Underscript[∣ , 𝕋])3d⟨0, 0, 
          0⟩]

Compute[⟨0, 4, 
          1⟩ (Underscript[∣ , 𝕋])3d⟨0, 5, 
          3⟩]

Compute[⟨0, 4, 
          4⟩ (Underscript[∣ , 𝕋])3d⟨0, 5, 
          3⟩]

\(Compute[⟨55, 2, 
          4⟩\(/\+𝕋3d\)⟨2, 0, 2⟩]\)

Compute[
      (Underscript[lcm, 𝕋])3d[⟨55, 2, 
          4⟩, ⟨2, 0, 
          2⟩]]

\(Compute[⟨1, 2, 
          4⟩\( > \+𝕋3d\)⟨2, 0, 2⟩]\)

\(Compute[⟨1, 2, 
          4⟩\( > \+𝕋3d\)⟨1, 0, 2⟩]\)

\(Compute[⟨1, 2, 
          4⟩\( > \+𝕋3d\)⟨1, 2, 4⟩]\)

\(Compute[⟨1, 2, 
          3⟩\( > \+𝕋3d\)⟨1, 2, 4⟩]\)

\(Compute[⟨0, 0, 
          0⟩\( > \+𝕋3d\)⟨0, 0, 0⟩]\)

\(Compute[⟨0, 5, 
          1⟩\( > \+𝕋3d\)⟨0, 1, 5⟩]\)

\(Compute[⟨3, 5, 
          6⟩\( > \+𝕋3d\)⟨3, 4, 7⟩]\)

\(Compute[⟨3, 5, 
          6⟩\( > \+𝕋3d\)⟨3, 6, 5⟩]\)

Polynomials as Tuples of Coefficient Power Product Pairs

Informal Explanation

We now define a functor that constructs the domain of polynomials with "coefficients" from a given reduction ring C and "power products" from a given division semigroup T in a particular representation as tuples of pairs of coefficients and power products ordered according to the ordering given in the domain T.

Note that there are infinitely many other, isomorphic, representations of the polynomial domain over C and T possible. In abstract algebra, isomorphic representations of domains are not distinguished. In contrast, in algorithmic algebra, the distinction between different representations of domains is of utmost importance because different representations may lead to drastically different complexity of the operations in the domain.

In this functor, we do not only define the ordinary ring operations for polynomials but also the additional operations \(TraditionalForm\`\( > \+N\)\), (Underscript[rdm, N]), and (Underscript[lcrd, N]), that make the ring a reduction ring.

Some more explanations on the definition of the individual operations in the polynomial domain are given after the definition of the functor.

Definitions

Definition["reduction polynomials" ,any[C, T],
reduction–polynomials[C, T]   =

Functor[N,\(any[c, d, i, m, m\&_, n, n\&_, p, q, s, t]\),
	({{𝕤 = ⟨⟩}, {({{(Underscript[ϵ, N])[p]⇔(∧{({{is–tuple[p]}, {(Underscript[∀ , j = 
                                        1, …, \[LeftBracketingBar]p\[RightBracketingBar]])(∧{({{is–tuple[(Subscript[p, j])]}, {\[LeftBracketingBar](Subscript[p, j])\[RightBracketingBar] = 2}, {(Underscript[ϵ, C])[(Subscript[(((Subscript[p, j]))), 1])]}, {(Underscript[ϵ, T])[(Subscript[(((Subscript[p, j]))), 2])]}, {(Subscript[(((Subscript[p, j]))), 1]) ≠ (Underscript[0, C])}})})}, {\(∀ \+\(j = 1, …, \[LeftBracketingBar]p\[RightBracketingBar] - 1\)\((p\_j)\)\_2\( > \+T\)\((p\_\(j + 1\))\)\_2\)}})})
}, {(Underscript[1, N]) = ⟨⟨(Underscript[1, C]), 
                                (Underscript[1, T])⟩⟩}, {(Underscript[0, N]) = ⟨⟩}, {\(⟨⟩\( + \+N\)q = q\)}, {\(p\( + \+N\)⟨⟩ = p\)}, {\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\( + \+N\)⟨⟨d, t⟩, 
                                n\&_⟩\)={({{\(⟨c, 
                                        s⟩⌣\((⟨m\&_⟩\( + \+N\)⟨⟨d, t⟩, n\&_⟩)\)\), ⇐, \(s\( > \+T\)t\)}, {\(⟨d, 
                                        t⟩⌣\((⟨⟨c, s⟩, 
                                        m\&_⟩\( + \+N\)⟨n\&_⟩)\)\), ⇐, \(t\( > \+T\)s\)}, {\(⟨c\( + \+C\)d, 
                                        s⟩⌣\((⟨m\&_⟩\( + \+N\)⟨n\&_⟩)\)\), ⇐, \(c ≠ \(-\+C 
                                        d\)\)}, {\(⟨m\&_⟩\( + \+N\)⟨n\&_⟩\), ⇐, otherwise}})} }, {\(\(-\+N⟨⟩\) = ⟨⟩\)}, {\(\(-\+N⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\) = ⟨\(-\+C c\), 
                                s⟩⌣\((\(-\+N⟨m\&_⟩\))\)\)}, {\(p\( - \+N\)q = p\( + \+N\)\((\(-\+N q\))\)\)}, {\(\(
\)\(⟨⟩\(*\+N\)q = ⟨⟩\)\)}, {\(p\(*\+N\)⟨⟩ = ⟨⟩\)}, {\(\(⟨⟨c, 
                                  s⟩, 
                                m\&_⟩\(*\+N\)⟨⟨d, t⟩, 
                                n\&_⟩ = \((⟨⟨c\(*\+C\)d, 
                                      
                                      s\(*\+T\)t⟩⟩\( + \+N\)⟨⟨c, 
                                        s⟩⟩\(*\+\(\(N\)\(\ \)\)\)⟨n\&_⟩)\)\( + \+N\)⟨m\&_⟩\(*\+\(\(N\)\(\ \)\)\)⟨⟨d, t⟩, 
                                  n\&_⟩\)\(
\)
                          \)}, {\(\((⟨⟩\( > \+N\)p)\) ⇔ False\)}, {\(\((⟨⟨c, 
                                    s⟩, 
                                  m\&_⟩\( > \+N\)⟨⟩)\) ⇔ True\)}, {\((⟨⟨c, 
                                    s⟩, 
                                  m\&_⟩\( > \+N\)⟨⟨d, t⟩, 
                                  n\&_⟩)\)⇔(∨{({{\(s\( > \+T\)t\)}, {∧{({{s = t}, {\(c\( > \+C\)d\)}})} }, {∧{({{s = t}, {c = d}, {\(⟨m\&_⟩\( > \+N\)⟨n\&_⟩\)}})} }})} )}, {(Underscript[rdm, N])[⟨⟩, 
                              p] = (Underscript[0, N])}, {\(rdm\+N[⟨⟨c, 
                                  s⟩, 
                                m\&_⟩, ⟨⟩] = 0\+N\)}, {\(rdm\+N[⟨⟨c, s⟩, 
                                  m\&_⟩, ⟨⟨d, t⟩, 
                                  n\&_⟩]\)    =
{({{\(⟨⟨rdm\+C[c, d], s\(/\+T\)t⟩⟩\), ⇐, ∧{({{(Underscript[rdm, C])[c, d] ≠ (Underscript[0, C])}, {t (Underscript[∣ , T])s}})} }, {(Underscript[0, N]), ⇐, otherwise}})} 
}, {\(lcrd\+N[⟨⟨c, 
                                  s⟩, 
                                m\&_⟩, ⟨⟨d, t⟩, 
                                n\&_⟩]\ \  (*\ 
                              the\ least\ common\ reducible\ of\ ⟨⟨c, s⟩, 
                                  m\&_⟩\ modulo\ ⟨⟨d, t⟩, 
                                  n\&_⟩\ \ *) \  = 
⟨⟨lcrd\+C[c, d], 
                                lcm\+T[s, 
                                  t]⟩⟩\)}})}})
	]]

Some comments on the operations in the functor:

The element predicate (Underscript[ϵ, N]) expressed the fact that polynomials must be tuples of monomials that are ordered by \(TraditionalForm\`\( > \+T\)\). Monomials are tuples of length two with the first element being a non-zero coefficient taken from C and the second element being a "power product" taken from T.

Note that monomials must not have zero coefficients in this representation. Accordingly, the third clause in the definition of \(TraditionalForm\`+\+N\) in the definition checks for \(c ≠ \(-\+C d\)\) in order to avoid monomials with zeros in the sum of two polynomials!

The ordering \(TraditionalForm\`\( > \+N\)\) introduced on the polynomials is only partial even if the ordering \(TraditionalForm\`\( > \+T\)\) in the domain of power products is total.

The reduction multiplier \(TraditionalForm\`\(\(rdm\+N[⟨⟨c, 
              s⟩, 
            m\&_⟩, ⟨⟨d, t⟩, 
            n\&_⟩]\)\([\)\)\) of two non-zero polynomials is the singleton polynomial \(⟨⟨rdm\+C[c, d], 
          s\(/\+T\)t⟩⟩\) that consists of the only monomial \(⟨rdm\+C[c, d], s\(/\+T\)t⟩\) in case t (Underscript[∣ , T])s (t divides s in T). In all other cases we define it to be (Underscript[0, n]) so that in these cases no reduction takes place and, again, reducibility of p w.r.t. q can in all cases be decided by checking whether or not (Underscript[rdm, N])[ p, q] = (Underscript[0, N]).

The least common reducible \(lcrd\+N[⟨⟨c, 
            s⟩, 
          m\&_⟩, ⟨⟨d, 
            t⟩, n\&_⟩]\) is the singletion polynomial ⟨⟨(Underscript[lcrd, C])[c, d], 
          (Underscript[lcm, T])[s, t]⟩⟩ that consists of the only monomial ⟨(Underscript[lcrd, C])[c, d], 
        (Underscript[lcm, T])[s, t]⟩, where we refer to the (Underscript[lcrd, C])[c, d] in the coefficient domain C and to the (Underscript[lcm, T])[s, t] (the least common multiple) in the power product domain T. Of course, this reference to the least common multiple is the essence of Groebner bases construction in polynomial rings!

Attention: The quantifiers in the functor must not have bound variables that are identical to the bound variables in other functors. Hence, in this functor, we use 'j' as a bound variable in the definition of (Underscript[ϵ, N]) and not 'i' because 'i' was used in the functor 'tuples-division-semigroup-lexical'. This is a bug in the current implementation of functors in Theorema. It will be eliminated in the next version of Theorema.

Example: Trivariate Polynomials over the Rationals

Theory

Definition["ℙ",
	({{𝕋03 = 
                tuples–division–semigroup–lexical[3]}, {𝕋3 = 
                division–semigroup–degree–ordered[𝕋03]}, {ℚ0 = 
                rational–numbers–field[]}, {ℚR = 
                reduction–field[ℚ0]}, {ℙ = 
                reduction–polynomials[ℚR, 𝕋3]}})]

Theory["T",
	({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["reduction field"]}, {Definition["tuples division semigroup lexical"]}, {Definition["division semigroup degree ordered"]}, {Definition["reduction polynomials"]}, {Definition["ℙ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Element Operation

Compute[(Underscript[ϵ, ℙ])[⟨⟩]]

Compute[(Underscript[ϵ, ℙ])[
        (Underscript[1, ℙ])]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 11, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 11, 
              4⟩⟩,   ⟨2/3, ⟨5, 2, 
              2⟩⟩, ⟨17, ⟨5, 1, 
              3⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨4, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 0, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨0, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[2]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2.3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 
              2, -2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 2⟩, 
            3⟩,   ⟨-1/
              2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 3, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 2, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,  ⟨-5, ⟨0, 4, 
              0⟩⟩, ⟨-5, ⟨0, 3, 
              0⟩⟩,   ⟨-5, ⟨0, 3, 
              0⟩⟩⟩]]

Constants

Compute[(Underscript[1, ℙ])]

Compute[(Underscript[0, ℙ])]

Addition, Subtraction

\(Compute[⟨⟨2, ⟨3, 
              0, 4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \( + \+ℙ\)
⟨⟨5, ⟨3, 0, 
              3⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨1/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩]\)

\(Compute[⟨⟨2, ⟨3, 
              0, 4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \( - \+ℙ\)\(\(
\)\(⟨⟨5, ⟨3, 0, 
              3⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨1/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\)\)]\)

Multiplication

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 1\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨\(-5\), ⟨2, 2, 
              2⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

Ordering

\(Compute[\ 
      1\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ 
      1\+ℙ\ \ \( > \+ℙ\)\ 
        1\+ℙ]\)

\(Compute[\ 
      0\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ ⟨\(-1\)/2, ⟨0, 1, 
              3⟩⟩, \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 1, 
              3⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 1, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 0, 
              4⟩⟩, \ \ ⟨2/3, ⟨2, 3, 
              2⟩⟩, \ ⟨\(-1\)/2, ⟨0, 1, 
              3⟩⟩, \ \ ⟨\(-5\), ⟨0, 0, 
              0⟩⟩⟩]\)

Reduction Multiplier

Compute[
      (Underscript[rdm, ℙ])[
        (Underscript[0, ℙ]), ⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, 
        (Underscript[0, ℙ])]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨3, 0, 
              3⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 0, 
              2⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Least Common Reducible

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 0, 
              2⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨4, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 0, 
              2⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨4, 0, 
              4⟩⟩,   ⟨2/3, ⟨2, 2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              3⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩, ⟨⟨5, ⟨4, 3, 
              5⟩⟩,   ⟨2/3, ⟨2, 0, 
              2⟩⟩,   ⟨-1/2, ⟨2, 1, 
              0⟩⟩,    ⟨-5, ⟨0, 1, 
              0⟩⟩⟩]]

Groebner Ring Extension

Informal Explanation

We now come to the main construction in this paper: Given a reduction ring D, i.e. a domain D with ring operations plus additional operations \(TraditionalForm\`\( > \+D\)\), (Underscript[rdm, D]), (Underscript[lcrd, D]), we extend the domain with the crucial operations of the Groebner bases method, namely

(Underscript[rd, N])[ x, y] ... the reduction of element x with respect to the element y.

This operation proceeds by calculating (Underscript[rdm, N])[ x, y] and forming x - (Underscript[rdm, N])[ x, y] * y. The element (Underscript[rdm, N])[ x, y] is supposed to be constructed in such a way that x \(TraditionalForm\`-\+N\) (Underscript[rdm, N])[ x, y] \(TraditionalForm\`\(*\+N\)\) y \(TraditionalForm\`\( < \+N\)\) x iff (Underscript[∃ , m]) ( x \(TraditionalForm\`-\+N\) m \(TraditionalForm\`\(*\+N\)\) y \(TraditionalForm\`\( < \+N\)\) x), i.e. (Underscript[rdm, N]) implicitly also contains a test for deciding whether or not x is reducible modulo y. We suppose that (Underscript[rdm, N])[x, y] = (Underscript[0, N]) iff not (Underscript[∃ , m]) ( x \(TraditionalForm\`-\+N\) m \(TraditionalForm\`\(*\+N\)\) y \(TraditionalForm\`\( < \+N\)\) x).

(Underscript[trd, N])[ x, X] ... the total reduction of element x with respect to the elements in the tuple X.

This operation proceeds by iteratively applying (Underscript[rd, N]) using the elements in X as the possible reducing elements until no more reduction is possible.

The operation (Underscript[trd, N]) has a ternary version (Underscript[trd, N])[x, Y, i]: the reduction of x using the i-th element in X. This is an auxiliary operation in the definition of the binary function (Underscript[trd, N]). Note that, in Theorema, we have the possibility to use a function constant with various arities.

(Underscript[cpd, N])[ x, X] ... the critical pair difference of x and y.

This operation gives the abstract version of the "S-polynomials". It is the clue to the construction of Groebner bases.

(Underscript[Gb, N])[X] ... a Groebner basis for the tuple X.

This function describes, in concise and abstract form, the essence of the author's algorithm for constructing a Groebner bases for any tuple X of elements in the given domain. The algorithm proceeds by reducing all the critical pair differences of all pairs of elements in X. Non-zero results of these reductions are added to X and new critical differences are formed until no more non-zero reductions occur.

Note that, in this first version of the functor, we only describe the most elementary form of the Groebner bases algorithm. We do not yet incorporate criteria for the predicting zero reductions and the many other improvements of the algorithm since, in this paper, our focus is on illustrating the use of functors in a non-trivial piece of mathematics.

The definition of (Underscript[Gb, N])[X] refers to a binary version of (Underscript[Gb, N]): Namely, (Underscript[Gb, N])[X, B] carries a list B of pairs of elements whose critical pairs differences still have to be considered.

(Underscript[rdGb, N])[X] ... a reduced Groebner basis for the tuple X.

A reduced Groebner basis for X is obtained from a Groebner basis G for X by "auto–reducing" the Groebner basis, i.e. by reducing all elements in x w.r.t. to all elements in X except X and deleting all (Underscript[0, N]) in the resulting tuple. (Under certain assumptions on the reduction process, which are not generally met by the reduction processes which we admit in this paper, reduced Groebner bases are unique.)

(Underscript[ard, N])[X] ... an auto-reduced version of the tuple X.

(Underscript[tcrd, N])[ x, X] ... the total cofactor reduction of element x with respect to the elements in the tuple X.

This operation extends the functionality of (Underscript[trd, N]). While reducing, it collects the multipliers used in the reduction. This operation is not used in the actual Groebner bases construction. However, it is the clue to using Groebner bases for constructing the "syzygies" (solutions to linear diophantine equations with coefficients and solutions in N), see the literature on Groebner bases.

As a result, for an X = ⟨(Subscript[x, 1]),...,(Subscript[x, n])⟩, (Underscript[tcrd, N])[ x, X] yields a pair ⟨ y, C⟩ where y is reduced w.r.t. X and C is a tuple of elements ⟨(Subscript[c, 1]),  ... , (Subscript[c, n])⟩  such that y = x \(TraditionalForm\`-\+N\) ((Subscript[c, 1])\(*\+N\)(Subscript[x, 1])\( + \+N\)...\( + \+N\) \(TraditionalForm\`c\_n\(*\+N\)x\_n\)).

More explanations of the algorithms defined in the frame of the functor will be given after the definition of the  functor. In particular, some explanations of some special Theorema operations on tuples, as for example  (Subscript[C, i ⇤ a])  (replace the i-the element in tuple C by a) will be necessary.

Definitions

Definition["Groebner extension" ,any[R],
Groebner–extension[R]   =Functor[N,\(any[C, k, p, p\&_, q, q\&_, x, X, y, y\&_, Y]\),
	({{𝕤 = ⟨⟩}, {({{
(Underscript[ϵ, N])[
                              x] ⇔ (Underscript[ϵ, R])[
                              x]}, {(Underscript[0, N]) = (Underscript[0, R])}, {(Underscript[1, N]) = (Underscript[1, R])}, {\(x\( + \+N\)y = x\( + \+R\)y\)}, {\(\(-\+N x\) = \(-\+R x\)\)}, {\(x\( - \+N\)y = x\( - \+R\)y\)}, {\(x\(*\+N\)y = x\(*\+R\)y\)}, {\(x\( > \+N\)y ⇔ 
                            x\( > \+R\)y\)}, {(Underscript[rdm, N])[x, y]    = (Underscript[rdm, R])[x, y]}, {(Underscript[lcrd, N])[x, y]   = 
                            (Underscript[lcrd, R])[x, 
                              y]


                          }, {\(rd\+N[x, y]\ \  = 
                            x\( - \+N\)\(\(rdm\+N[x, 
                                  y]\(*\+N\)y\)\(
\)
                              \)\)}, {(Underscript[( trd), N])[x, Y]   =(Underscript[trd, N])[x, Y, 1] }, {(Underscript[trd, N])[x, Y, k]     =
{({{x, ⇐, k > \[LeftBracketingBar]Y\[RightBracketingBar]}, {where[x1 = (Underscript[rd, N])[x, (Subscript[Y, k])],
{({{(Underscript[trd, N])[x1, Y, 1], ⇐, \(x\( > \+N\)x1\)}, {(Underscript[trd, N])[x, Y, k + 1], ⇐, otherwise}})} ], ⇐, otherwise}})}
}, {\(\(cpd\+N[x, y]\  (*\ 
                              the\ critical\ pair\ difference\ of\ x\ and\ y\ *)  = 
where[lxy = lcrd\+N[x, y], 
                              rd\+N[lxy, x]\( - \+N\)rd\+N[lxy, 
                                  y]]\)\(\ \)\(
\)
                          \)}, {(Underscript[Gb, N])[X]    = (Underscript[Gb, N])[X, pairs[X]]}, {(Underscript[Gb, N])[
                              X, ⟨⟩] = 
                            X}, {\(Gb\+N[
                                X, ⟨⟨x, 
                                    y⟩, 
                                  p\&_⟩]\)=
where[h = (Underscript[trd, N])[(Underscript[cpd, N])[x, y], X],
{({{\(Gb\+N[
                                        X, ⟨p\&_⟩]\), ⇐, h = (Underscript[0, N])}, {\(Gb\+N[
                                        X⌢h, ⟨p\&_⟩ ≍ ⟨\(⟨X\_k, 
                                        h⟩\)\( \[VerticalSeparator] \+\(k = 
                                        1, …, \[LeftBracketingBar]X\[RightBracketingBar]\)\)⟩]\), ⇐, otherwise}})} ]
}, {(Underscript[rdGb, N])[X]     = (Underscript[ard, N])[(Underscript[Gb, N])[X]]}, {(Underscript[ard, N])[⟨⟩] = ⟨⟩}, {\(ard\+N[⟨p, 
                                q\&_⟩] = 
                            ard\+N[⟨⟩, 
                              p, ⟨q\&_⟩]\)}, {(Underscript[ard, N])[X, 
                              p, ⟨⟩]=where[h = (Underscript[trd, N])[p, X],
{({{X, ⇐, h = (Underscript[0, N])}, {X⌢p, ⇐, otherwise}})} ]}, {\(ard\+N[X, 
                              p, ⟨q, 
                                q\&_⟩]\)=where[\(h = 
                                  trd\+N[p, 
                                    X ≍ ⟨q, 
                                        q\&_⟩]\),
{({{\(ard\+N[X, 
                                        q, ⟨q\&_⟩]\), ⇐, h = (Underscript[0, N])}, {\(ard\+N[X⌢p, 
                                        q, ⟨q\&_⟩]\), ⇐, otherwise}})} ]}, {(Underscript[( tcrd), N])[x, Y]  (* 
                              the total cofactor reduction of x modulo tuple Y *)  = (Underscript[tcrd, N])[x, Y, 
                              1, ⟨(Underscript[0, N]) (Underscript[\[VerticalSeparator] , k = 
                                        1, …, \[LeftBracketingBar]Y\[RightBracketingBar]])⟩]}, {(Underscript[tcrd, N])[x, Y, k, C]     =
{({{⟨x, 
                                      C⟩, ⇐, k > \[LeftBracketingBar]Y\[RightBracketingBar]}, {where[c = (Underscript[rdm, N])[x, (Subscript[Y, k])],\(x1 = 
                                        x\( - \+N\)c\(*\+N\)Y\_k\),
{({{\(tcrd\+N[x1, Y, 1, 
                                        C\_\(k ⇤ C\_k\( + \+N\)c\)]\), ⇐, \(x\( > \+N\)x1\)}, {(Underscript[tcrd, N])[x, Y, k + 1, C], ⇐, otherwise}})} ], ⇐, otherwise}})}}})}})
	]]

Some more explanations on the algorithms in the functor:

pairs[X] yields a tuple that consists of all pairs ⟨x,y⟩ of elements x, y  in the tuple X, where x has to occur before y. We defined the function 'pairs' in the section "Preparation of Theorema".

The operation X⌢h appends element h to the tuple X. In Theorema, the append function is a built-in function on tuples.

The operation

\(⟨p\&_⟩ ≍ ⟨\(⟨X\_i, 
            h⟩\)\( \[VerticalSeparator] \+\(i = 
                1, …, \[LeftBracketingBar]X\[RightBracketingBar]\)\)⟩\)

concatenates the tuple \(\(\(⟨p\&_⟩\)\(\ \)\)\)(which in this context is a tuple of pairs) with the tuple of pairs \(⟨\(⟨X\_i, 
            h⟩\)\( | \+\(i = 
                1, …, |X|\)\)⟩\). The concatenation operation '≍' is also a built-in function on tuples in Theorema. Also the length function |..| is built in. Note that here again we use the tuple quantifier of Theorema.

The operation

\(C\_\(k ⇤ C\_k\( + \+N\)c\)\)

replaces the k-th element in the tuple C by \(C\_k\( + \+N\)c\), i.e. the k-th element of C plus c. The replacement operation '⇤' is also a built-in operation in Theorema.

Example: Groebner Bases in the Integers

Informal Explanation

To view the integers as a domain in which we can compute Groebner basis by the general Groebner bases algorithm described in the preceding functor is a completely non-trivial undertaking. In addition to verifying that, of course, the result of the Groebner bases computation for a given tuple X of integers is a tuple containing the greatest common divisor (gcd) of the elements in X, you should trace the computations for understanding what the operation of critical pair difference  does in the integers, which yields the analogue of the S-polynomials. That we can view the process of generating the gcd of the integer elements in X as a Groebner basis computation is interesting because one does not immediately see a structure like "leading monomial" and "remaining monomials" etc. in the integers. It is the notion of "least common reducible" that extracts the essential substance of the Groebner bases construction even in domains in which the elements do not have a "leading part" / "remaining part" structure.

Theory (for Using the Reduction Integers with Subtraction)

Definition["ℤ", ℤ = 
        Groebner–extension[reduction–integers[]]]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["reduction integers"]}, {Definition["Groebner extension"]}, {Definition["ℤ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Arithmetical Operations

Compute[(Underscript[ϵ, ℤ])[-2]]

Compute[(Underscript[ϵ, ℤ])[2.3]]

Compute[(Underscript[0, ℤ])]

Compute[(Underscript[1, ℤ])]

\(Compute[5\( + \+ℤ\)3]\)

\(Compute[\(-\+ℤ\(-2\)\)]\)

\(Compute[5\( - \+ℤ\)3]\)

\(Compute[5\(*\+ℤ\)3]\)

Reduction Ring Operations

\(Compute[\(-3\)\( > \+ℤ\)2]\)

\(Compute[\(-3\)\( > \+ℤ\)3]\)

Compute[(Underscript[rdm, ℤ])[3, 2]]

Compute[(Underscript[rdm, ℤ])[3, -2]]

Compute[(Underscript[rdm, ℤ])[-2, 4]]

Compute[(Underscript[lcrd, ℤ])[-3, -2]]

Compute[(Underscript[lcrd, ℤ])[3, -2]]

Compute[(Underscript[lcrd, ℤ])[-3, -22]]

Reduction

Compute[(Underscript[rd, ℤ])[7, 5]]

Compute[(Underscript[rd, ℤ])[7, -5]]

Compute[(Underscript[rd, ℤ])[-7, 5]]

Compute[(Underscript[rd, ℤ])[-8, -5]]

Compute[(Underscript[rd, ℤ])[-17, 5]]

Total Reduction Modulo a Tuple

Compute[
      (Underscript[trd, ℤ])[
        17, ⟨⟩]]

Compute[
      (Underscript[trd, ℤ])[
        17, ⟨5⟩]]

Compute[
      (Underscript[trd, ℤ])[
        17, ⟨-5⟩]]

Compute[
      (Underscript[trd, ℤ])[
        5, ⟨5⟩]]

Compute[
      (Underscript[trd, ℤ])[
        24, ⟨4⟩]]

Compute[
        (Underscript[trd, ℤ])[
          1289, ⟨123, 13, 10, 8⟩]] // 
      Timing

Compute[
        (Underscript[trd, ℤ])[
          1289, ⟨10, 128, 13, 8⟩]] // 
      Timing

Note that different reductions of a given initial x modulo tuples containing the same elements may lead to different results with very different reduction times as long as these tuples are not yet Groebner bases!

Of course, these reductions take enormous time because we proceed by repeated subtraction instead of application of the integer quotient and also because our algorithms are written in Theorema on top of Mathematica, see the remark in the section on "Preparation of Theorema". However, as explained earlier, the focus of this paper is logic clarity and generality and not efficiency.

Total Cofactor Reduction Modulo a Tuple

Compute[
      (Underscript[tcrd, ℤ])[
        17, ⟨⟩]]

Compute[
      (Underscript[tcrd, ℤ])[
        17, ⟨5⟩]]

This means that 17 - 3 * 5 = 2 and 2 is reduced modulo 5.

Compute[
      (Underscript[tcrd, ℤ])[
        17, ⟨-5⟩]]

This means that 17 - (-3) * (-5) = 2 and 2 is reduced modulo -5.

Compute[
      (Underscript[tcrd, ℤ])[
        5, ⟨5⟩]]

Compute[
      (Underscript[tcrd, ℤ])[
        24, ⟨4⟩]]

Compute[
      (Underscript[tcrd, ℤ])[
        12895, ⟨1230, 130, 10, 
          8⟩]]

This means that 3 = 12895 - 10 *1230 - 4 * 130 - 7 * 10 - 0 * 8.

Critical Pair Difference

Compute[(Underscript[lcrd, ℤ])[15, 19]]

Compute[(Underscript[cpd, ℤ])[15, 19]]

19 reduces modulo 15 to 4. Furthermore, 19 reduces modulo 19 to 0. Hence the critical pair difference is 4 - 0 = 4.

Groebner Basis

Compute[
      (Underscript[Gb, ℤ])[⟨⟩]]

Compute[
      (Underscript[Gb, ℤ])[⟨5, 88, 13, 
          6⟩]]

Compute[
      (Underscript[ard, ℤ])[⟨5, 88, 13, 6, 3, 
          1⟩]]

Compare this with the greatest common divisor of the input integers:

GCD[5, 88, 13, 6]

(Note: One should not normally use Mathematica functions during a Theorema session. The correct working of the Mathematica functions is not guaranteed during Theorema sessions. This has to do with the fact that Theorema changes some of the syntax of Mathematica. However, as in this simple example of the GCD, some of the functionality of Mathematica may well be available during a Theorema session.)

Compute[
        (Underscript[Gb, ℤ])[⟨2091, 2337, 
            2829⟩]]  // Timing

Compute[
      (Underscript[ard, ℤ])[⟨2091, 2337, 2829, 
          246, -123⟩]]

Compute[
      (Underscript[rdGb, ℤ])[⟨2091, 2337, 
          2829⟩]]

Compare this with the greatest common divisor of the input integers:

GCD[2091, 2337, 2829]

Theory (for Using the Reduction Integers with Quotient)

Definition["ℤ", ℤ = 
        Groebner–extension[
          reduction–integers–by–quotient[]]]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["reduction integers by quotient"]}, {Definition["Groebner extension"]}, {Definition["ℤ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Groebner Basis

Compute[
      (Underscript[Gb, ℤ])[⟨⟩]]

Compute[
      (Underscript[Gb, ℤ])[⟨5, 88, 13, 
          6⟩]]

Compute[
      (Underscript[ard, ℤ])[⟨5, 88, 13, 6, 3, 
          1⟩]]

Compute[
        (Underscript[Gb, ℤ])[⟨2091, 2337, 
            2829⟩]]  // Timing

One can observe that the computation is much faster using quotients instead of stepwise subtractions.

Compute[
      (Underscript[ard, ℤ])[⟨2091, 2337, 2829, 
          246, -123⟩]]

Compute[
        (Underscript[rdGb, ℤ])[⟨2091, 2337, 
            2829⟩]] // Timing

Example: Groebner Bases in the Rationals

Informal Explanation

Of course, Groebner bases theory over fields F is trivial: Every tuple of field elements is a Groebner bases. In particular, the tuple ⟨(Underscript[1, F])⟩ is a Groebner basis for every ideal in the field.

However, nevertheless, we compute here Groebner bases in the field of rationals viewed as a reduction ring using the generic functor for Groebner bases computation in reduction rings in order to illustrate how the instantiation of the general functor specializes smoothly and automatically to the situation in fields.

Theory

Definition["ℚ", ℚ = 
        Groebner–extension[
          reduction–field[
            rational–numbers–field[]]]]

Theory["T",
({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["reduction field"]}, {Definition["Groebner extension"]}, {Definition["ℚ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Arithmetic

Compute[(Underscript[0, ℚ])]

Compute[(Underscript[1, ℚ])]

\(Compute[5/3\( + \+ℚ\)3]\)

\(Compute[\(-\+ℚ\(-2\)\)/3]\)

\(Compute[5/7\( - \+ℚ\)3]\)

\(Compute[5\(*\+ℚ\)3/2]\)

Reduction Multiplier

Compute[(Underscript[rdm, ℚ])[3, 2]]

Compute[(Underscript[rdm, ℚ])[3, -2]]

Compute[(Underscript[rdm, ℚ])[-2, 4/3]]

Reduction

Compute[(Underscript[rd, ℚ])[7, 5]]

Compute[(Underscript[rd, ℚ])[7/2, -5/4]]

Total Reduction Modulo a Tuple

Compute[
      (Underscript[trd, ℚ])[
        17, ⟨⟩]]

Compute[
      (Underscript[trd, ℚ])[
        17, ⟨5⟩]]

Compute[
      (Underscript[trd, ℚ])[
        17, ⟨-5⟩]]

Compute[
      (Underscript[trd, ℚ])[
        5, ⟨5⟩]]

Compute[
      (Underscript[trd, ℚ])[
        24/7, ⟨4⟩]]

Compute[
        (Underscript[trd, ℚ])[
          1289, ⟨123, 13, 10, 8⟩]] // 
      Timing

Total Cofactor Reduction Modulo a Tuple

Compute[
      (Underscript[tcrd, ℚ])[
        17, ⟨⟩]]

Compute[
      (Underscript[tcrd, ℚ])[
        17, ⟨5⟩]]

Compute[
      (Underscript[tcrd, ℚ])[
        17, ⟨-5⟩]]

Compute[
      (Underscript[tcrd, ℚ])[
        5, ⟨5⟩]]

Compute[
      (Underscript[tcrd, ℚ])[
        24/7, ⟨4⟩]]

Compute[
        (Underscript[tcrd, ℚ])[
          12895, ⟨1230, 130, 10, 8⟩]] // 
      Timing

Least Common Reducible

Compute[(Underscript[lcrd, ℚ])[-3, -2]]

Compute[(Underscript[lcrd, ℚ])[3, -2/7]]

Critical Pair Difference

Compute[(Underscript[cpd, ℚ])[15/7, 19/3]]

Groebner Basis

Compute[
      (Underscript[Gb, ℚ])[⟨⟩]]

Compute[
      (Underscript[Gb, ℚ])[⟨5, 88, 13, 
          6⟩]]

Compute[
      (Underscript[Gb, ℚ])[⟨2091, 2337, 
          2829⟩]]

Compute[
      (Underscript[rdGb, ℚ])[⟨2091, 2337, 
          2829⟩]]

Compute[
      (Underscript[rdGb, ℚ])[⟨⟩]]

Compute[
      (Underscript[rdGb, ℚ])[⟨2⟩]]

Compute[
      (Underscript[rdGb, ℚ])[⟨2, 3, 
          4⟩]]

Example: Groebner Bases in the Bivariate Polynomials over the Rationals

Theory

Definition["ℙ",
	({{𝕋2 = 
                tuples–division–semigroup–lexical[2]}, {𝕋 = 
                division–semigroup–degree–ordered[𝕋2]}, {ℚ0 = 
                rational–numbers–field[]}, {ℚ = 
                reduction–field[ℚ0]}, {ℙ0 = 
                reduction–polynomials[ℚ, 𝕋]}, {ℙ = 
                Groebner–extension[ℙ0]}})]

Theory["T",
	({{Definition["Theorema general functions"]}, {Definition["rational numbers field"]}, {Definition["reduction field"]}, {Definition["tuples division semigroup lexical"]}, {Definition["division semigroup degree ordered"]}, {Definition["reduction polynomials"]}, {Definition["Groebner extension"]}, {Definition["ℙ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Test of Reduction Rings Operations

Compute[(Underscript[ϵ, ℙ])[⟨⟩]]

Compute[(Underscript[ϵ, ℙ])[
        (Underscript[1, ℙ])]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              7⟩⟩,   ⟨2/3, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[1, ℙ])]

Compute[(Underscript[0, ℙ])]

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩\ \ \( + \+ℙ\)
⟨⟨5, ⟨7, 
              0⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨1/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              1⟩⟩⟩]\)

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩\ \ \( - \+ℙ\)\(\(
\)\(⟨⟨5, ⟨7, 
              0⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨1/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              1⟩⟩⟩\)\)]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 1\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ 
      0\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨0, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨2, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨2/3, ⟨2, 
              2⟩⟩, \ \ ⟨\(-1\)/2, ⟨3, 
              1⟩⟩, \ \ \ ⟨\(-5\), ⟨0, 
              0⟩⟩⟩]\)

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨2/3, ⟨2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 
              1⟩⟩,    ⟨-5, ⟨0, 
              0⟩⟩⟩, ⟨⟨24, ⟨2, 
              1⟩⟩,   ⟨2/3, ⟨2, 
              0⟩⟩,   ⟨-1/2, ⟨1, 
              1⟩⟩,    ⟨-5, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨2/3, ⟨2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 
              1⟩⟩,    ⟨-5, ⟨0, 
              0⟩⟩⟩, ⟨⟨24, ⟨2, 
              5⟩⟩,   ⟨2/3, ⟨2, 
              0⟩⟩,   ⟨-1/2, ⟨1, 
              1⟩⟩,    ⟨-5, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 
              4⟩⟩,   ⟨2/3, ⟨2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 
              1⟩⟩,    ⟨-5, ⟨0, 
              0⟩⟩⟩, ⟨⟨2, ⟨7, 
              2⟩⟩,   ⟨2/3, ⟨2, 
              2⟩⟩,   ⟨-1/2, ⟨2, 
              1⟩⟩,    ⟨-5, ⟨0, 
              0⟩⟩⟩]]

Total Reduction Modulo a Tuple

For test purposes we compute, in the sequel, a couple of test examples using the implementation of our Groebner basis algorithm in Mathematica and compare the results with what we get in Theorema using the above Groebner extension functor.

PolynomialReduce[x (y^2) , {2 x y  - 5}, 
      MonomialOrder -> DegreeLexicographic]

Compute[
      (Underscript[rd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩⟩, ⟨⟨2, ⟨1, 
              1⟩⟩, ⟨-5, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rd, ℙ])[⟨⟨(5/2), ⟨0, 
              1⟩⟩⟩, ⟨⟨2, ⟨1, 
              1⟩⟩, ⟨-5, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[trd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨-5, ⟨0, 
                0⟩⟩⟩⟩]]

PolynomialReduce[
      (x^2) (y^2) + 5  x (y^2) , {2 x y  - 5  x, (x^2) - 2}, 
      MonomialOrder -> DegreeLexicographic]

Compute[
      (Underscript[trd, ℙ])[⟨⟨1, ⟨2, 
              2⟩⟩, ⟨5, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨-5, ⟨1, 
                0⟩⟩⟩, ⟨⟨1, ⟨2, 
                0⟩⟩, ⟨-2, ⟨0, 
                0⟩⟩⟩⟩]]

Total Cofactor Reduction Modulo a Tuple

PolynomialReduce[
      (x^2) (y^2) + 5  x (y^2) , {2 x y  - 5  x, (x^2) - 2}, 
      MonomialOrder -> DegreeLexicographic]

Compute[
      (Underscript[tcrd, ℙ])[⟨⟨1, ⟨2, 
              2⟩⟩, ⟨5, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨-5, ⟨1, 
                0⟩⟩⟩, ⟨⟨1, ⟨2, 
                0⟩⟩, ⟨-2, ⟨0, 
                0⟩⟩⟩⟩]]

Critical Pair Difference

Expand[
      x (x (y^2) - 2  x + 3) - y ((x^2) y + 3  y + 4)]

Compute[
      (Underscript[cpd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩, ⟨-2, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨1, ⟨2, 
              1⟩⟩, ⟨3, ⟨0, 
              1⟩⟩, ⟨4, ⟨0, 
              0⟩⟩⟩]]

Groebner Basis

Compute[
      (Underscript[Gb, ℙ])[⟨⟩]]

GroebnerBasis[{ x - y - 5, x y -  x + 3}, {x, y}, 
      MonomialOrder -> DegreeLexicographic]

Compute[
      (Underscript[Gb, ℙ])[⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨-1, ⟨0, 
                1⟩⟩, ⟨-5, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨1, 
                1⟩⟩, ⟨-1, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

One sees that the Groebner basis contains superfluous elements, which could be reduced modulo the other elements in the basis:

Compute[
      (Underscript[trd, ℙ])[⟨⟨1, ⟨1, 
              1⟩⟩, ⟨-1, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨-1, ⟨0, 
                1⟩⟩, ⟨-5, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨0, 
                2⟩⟩, ⟨-1, ⟨1, 
                0⟩⟩, ⟨5, ⟨0, 
                1⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

This could also be established by applying the auto-reduction function  (Underscript[ard, ℙ]):

Compute[
      (Underscript[ard, ℙ])[⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨-1, ⟨0, 
                1⟩⟩, ⟨-5, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨1, 
                1⟩⟩, ⟨-1, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨0, 
                2⟩⟩, ⟨-1, ⟨1, 
                0⟩⟩, ⟨5, ⟨0, 
                1⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

Alternatively, we could use the (Underscript[rdGB, ℙ]) function:

Compute[
      (Underscript[rdGb, ℙ])[⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨-1, ⟨0, 
                1⟩⟩, ⟨-5, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨1, 
                1⟩⟩, ⟨-1, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

This is not yet what a "complete" reduction yields because the particular reduction multiplier function which we implemented in the Groebner extension functor only reduces the leading monomial!

We could carry out the reduction of the second polynomial in the basis by computing

\(Compute[⟨⟨1, ⟨0, 
              2⟩⟩, ⟨\(-1\), ⟨1, 
              0⟩⟩, ⟨5, ⟨0, 
              1⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩\( + \+ℙ\)⟨⟨1, ⟨1, 
              0⟩⟩, ⟨\(-1\), ⟨0, 
              1⟩⟩, ⟨\(-5\), ⟨0, 
              0⟩⟩⟩]\)

Then we would get the completely reduced Groebner basis

⟨⟨⟨1, ⟨1, 
              0⟩⟩, ⟨-1, ⟨0, 
              1⟩⟩, ⟨-5, ⟨0, 
              0⟩⟩⟩, ⟨⟨1, ⟨0, 
              2⟩⟩, ⟨4, ⟨0, 
              1⟩⟩, ⟨-2, ⟨0, 
              0⟩⟩⟩⟩.

which is identical to the result of the Mathematica computation

{-5 + x + (-1) y, -2 + 4 y + 
          (y^2)}.

Here is another example:

GroebnerBasis[{ x (y^2) - y - 5, (x^2) y -  x + 3}, {x, y}, 
        MonomialOrder -> DegreeLexicographic] // Timing

Compute[
        (Underscript[rdGb, ℙ])[⟨⟨⟨1, ⟨1, 
                  2⟩⟩, ⟨-1, ⟨0, 
                  1⟩⟩, ⟨-5, ⟨0, 
                  0⟩⟩⟩, ⟨⟨1, ⟨2, 
                  1⟩⟩, ⟨-1, ⟨1, 
                  0⟩⟩, ⟨3, ⟨0, 
                  0⟩⟩⟩⟩]] // Timing

Example: Groebner Bases in the Bivariate Polynomials over the Finite Field modulo 5

Theory

Definition["ℙ",
	({{𝕋2 = 
                tuples–division–semigroup–lexical[2]}, {𝕋 = 
                division–semigroup–degree–ordered[𝕋2]}, {𝔽5o = prime–field[5]}, {𝔽5 = 
                reduction–field[𝔽5o]}, {ℙ0 = 
                reduction–polynomials[𝔽5, 𝕋]}, {ℙ = 
                Groebner–extension[ℙ0]}})]

Theory["T",
	({{Definition["Theorema general functions"]}, {Definition["prime field"]}, {Definition["reduction field"]}, {Definition["tuples division semigroup lexical"]}, {Definition["division semigroup degree ordered"]}, {Definition["reduction polynomials"]}, {Definition["Groebner extension"]}, {Definition["ℙ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Test of Reduction Rings Operations

Compute[(Underscript[ϵ, ℙ])[⟨⟩]]

Compute[(Underscript[ϵ, ℙ])[
        (Underscript[1, ℙ])]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              7⟩⟩,   ⟨2/3, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              7⟩⟩,   ⟨3, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[1, ℙ])]

Compute[(Underscript[0, ℙ])]

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( + \+ℙ\)
⟨⟨4, ⟨7, 
              0⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨2, ⟨0, 
              1⟩⟩⟩]\)

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( - \+ℙ\)
⟨⟨4, ⟨7, 
              0⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨2, ⟨0, 
              1⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 1\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ 
      0\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨1, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨3, 
              1⟩⟩, \ \ ⟨1, ⟨1, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              1⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Total Reduction Modulo a Tuple

For test purposes we compute, in the sequel, a couple of test examples using the implementation of our Groebner basis algorithm in Mathematica and compare the results with what we get in Theorema using the above Groebner extension functor.

PolynomialReduce[x (y^2) , {2 x y  + 4}, 
      MonomialOrder -> DegreeLexicographic,  
      Modulus -> 5]

Compute[
      (Underscript[rd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩⟩, ⟨⟨2, ⟨1, 
              1⟩⟩, ⟨4, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[trd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨4, ⟨0, 
                0⟩⟩⟩⟩]]

PolynomialReduce[(x^2) (y^2) + 4  x (y^2) , {2 x y  + x, (x^2) + 3}, 
      MonomialOrder -> DegreeLexicographic, 
      Modulus -> 5]

Compute[
      (Underscript[trd, ℙ])[⟨⟨1, ⟨2, 
              2⟩⟩, ⟨4, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨1, ⟨1, 
                0⟩⟩⟩, ⟨⟨1, ⟨2, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

Total Cofactor Reduction Modulo a Tuple

Compute[
      (Underscript[tcrd, ℙ])[⟨⟨1, ⟨2, 
              2⟩⟩, ⟨4, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨1, ⟨1, 
                0⟩⟩⟩, ⟨⟨1, ⟨2, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

Critical Pair Difference

Expand[-x (x (y^2) + 3  x + 3) + 
        y ((x^2) y + 3  y + 4), Modulus -> 5]

Compute[
      (Underscript[cpd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩, ⟨3, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨1, ⟨2, 
              1⟩⟩, ⟨3, ⟨0, 
              1⟩⟩, ⟨4, ⟨0, 
              0⟩⟩⟩]]

Groebner Basis

Compute[
      (Underscript[Gb, ℙ])[⟨⟩]]

GroebnerBasis[{ x + 4  y + 2, x y + 4 x + 3}, {x, y}, 
      MonomialOrder -> DegreeLexicographic, 
      Modulus -> 5]

Compute[
      (Underscript[Gb, ℙ])[⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨4, ⟨0, 
                1⟩⟩, ⟨2, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨1, 
                1⟩⟩, ⟨4, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

One sees that the Groebner basis contains superfluous elements, which can be canceled by applying the auto-reduction function  (Underscript[ard, ℙ]):

Compute[
      (Underscript[ard, ℙ])[⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨4, ⟨0, 
                1⟩⟩, ⟨2, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨1, 
                1⟩⟩, ⟨4, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨0, 
                2⟩⟩, ⟨4, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                1⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

This is not yet what a "complete" reduction yields because the particular reduction multiplier function which we implemented in the Groebner extension functor only reduces the leading monomial!

We could carry out the reduction of the second polynomial in the basis by computing

\(Compute[⟨⟨1, ⟨0, 
              2⟩⟩, ⟨4, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              1⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩\( - \+ℙ\)\((\ ⟨⟨4, ⟨0, 
                  0⟩⟩⟩\(*\+ℙ\)⟨⟨1, ⟨1, 
                  0⟩⟩, ⟨4, ⟨0, 
                  1⟩⟩, ⟨2, ⟨0, 
                  0⟩⟩⟩)\)]\)

Then we would get the completely reduced Groebner basis

⟨⟨⟨1, ⟨1, 
            0⟩⟩, ⟨4, ⟨0, 
            1⟩⟩, ⟨2, ⟨0, 
            0⟩⟩⟩, ⟨⟨1, ⟨0, 
            2⟩⟩, ⟨2, ⟨0, 
            1⟩⟩⟩⟩

which is identical to the result of the Mathematica computation

Here is another example:

GroebnerBasis[{ x (y^2) + 4  y + 2, (x^2) y + 4 x + 3}, {x, y}, 
        MonomialOrder -> DegreeLexicographic,  Modulus -> 5] // 
      Timing

Compute[
        (Underscript[rdGb, ℙ])[⟨⟨⟨1, ⟨1, 
                  2⟩⟩, ⟨4, ⟨0, 
                  1⟩⟩, ⟨2, ⟨0, 
                  0⟩⟩⟩, ⟨⟨1, ⟨2, 
                  1⟩⟩, ⟨4, ⟨1, 
                  0⟩⟩, ⟨3, ⟨0, 
                  0⟩⟩⟩⟩]] // Timing

Example: Groebner Bases in the Bivariate Polynomials over the Integers

Theory

Definition["ℙ",
	({{𝕋2 = 
                tuples–division–semigroup–lexical[2]}, {𝕋 = 
                division–semigroup–degree–ordered[𝕋2]}, {ℤ = 
                reduction–integers–by–quotient[]}, {ℙ0 = 
                reduction–polynomials[ℤ, 𝕋]}, {ℙ = 
                Groebner–extension[ℙ0]}})]

Theory["T",
	({{Definition["Theorema general functions"]}, {Definition["reduction integers by quotient"]}, {Definition["tuples division semigroup lexical"]}, {Definition["division semigroup degree ordered"]}, {Definition["reduction polynomials"]}, {Definition["Groebner extension"]}, {Definition["ℙ"]}})]

Use[⟨Built–in["Quantifiers"], 
        Built–in["Connectives"], Built–in["Numbers"], 
        Built–in["Tuples"], Built–in["Sets"], 
        Built–in["Mathematica general functions"], 
        Theory["T"]⟩]

Test of Reduction Rings Operations

Compute[(Underscript[ϵ, ℙ])[⟨⟩]]

Compute[(Underscript[ϵ, ℙ])[
        (Underscript[1, ℙ])]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 0, 
              4⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              0⟩⟩⟩]]

Compute[(Underscript[ϵ, ℙ])[⟨⟨2, ⟨3, 
              7⟩⟩,   ⟨-2, ⟨5, 
              2⟩⟩⟩]]

Compute[(Underscript[1, ℙ])]

Compute[(Underscript[0, ℙ])]

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( + \+ℙ\)
⟨⟨4, ⟨7, 
              0⟩⟩, \ \ ⟨\(-3\), ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨2, ⟨0, 
              1⟩⟩⟩]\)

\(Compute[⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( - \+ℙ\)\(\(
\)
        \(⟨⟨4, ⟨7, 
              0⟩⟩, \ \ ⟨\(-3\), ⟨2, 
              2⟩⟩, \ \ ⟨4, ⟨2, 
              1⟩⟩, \ \ \ ⟨2, ⟨0, 
              1⟩⟩⟩\)\)]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ 1\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \(*\+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ 
      0\+ℙ\ \ \( > \+ℙ\)\ 
        0\+ℙ]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨1, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

\(Compute[\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨2, 
              2⟩⟩, \ \ ⟨1, ⟨2, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩\ \ \( > \+ℙ\)\ ⟨⟨2, ⟨3, 
              2⟩⟩, \ \ ⟨3, ⟨3, 
              1⟩⟩, \ \ ⟨1, ⟨1, 
              1⟩⟩, \ \ \ ⟨3, ⟨0, 
              0⟩⟩⟩]\)

Compute[
      (Underscript[rdm, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              1⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨20, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[rdm, ℙ])[⟨⟨20, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              2⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[lcrd, ℙ])[⟨⟨2, ⟨3, 
              2⟩⟩,   ⟨3, ⟨2, 
              2⟩⟩,   ⟨1, ⟨2, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨-3, ⟨2, 
              3⟩⟩,   ⟨3, ⟨1, 
              2⟩⟩,   ⟨1, ⟨1, 
              1⟩⟩,    ⟨3, ⟨0, 
              0⟩⟩⟩]]

Total Reduction Modulo a Tuple

For test purposes we compute, in the sequel, a couple of test examples using the implementation of our Groebner basis algorithm in Mathematica and compare the results with what we get in Theorema using the above Groebner extension functor.

PolynomialReduce[x (y^2) , {2 x y  + 4}, 
      MonomialOrder -> DegreeLexicographic,  
      CoefficientDomain -> Integers]

Compute[
      (Underscript[rd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩⟩, ⟨⟨2, ⟨1, 
              1⟩⟩, ⟨4, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[trd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨4, ⟨0, 
                0⟩⟩⟩⟩]]

PolynomialReduce[8  x (y^2) , {2 x y  + 4}, 
      MonomialOrder -> DegreeLexicographic,  
      CoefficientDomain -> Integers]

Compute[
      (Underscript[rd, ℙ])[⟨⟨8, ⟨1, 
              2⟩⟩⟩, ⟨⟨2, ⟨1, 
              1⟩⟩, ⟨4, ⟨0, 
              0⟩⟩⟩]]

Compute[
      (Underscript[trd, ℙ])[⟨⟨8, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨4, ⟨0, 
                0⟩⟩⟩⟩]]

PolynomialReduce[
      21 (x^2) (y^2) + 4  x (y^2) , {2 x y  + x, (x^2) + 3}, 
      MonomialOrder -> DegreeLexicographic, 
      CoefficientDomain -> Integers]

Compute[
      (Underscript[trd, ℙ])[⟨⟨21, ⟨2, 
              2⟩⟩, ⟨4, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨1, ⟨1, 
                0⟩⟩⟩, ⟨⟨1, ⟨2, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

Total Cofactor Reduction Modulo a Tuple

Compute[
      (Underscript[tcrd, ℙ])[⟨⟨21, ⟨2, 
              2⟩⟩, ⟨4, ⟨1, 
              2⟩⟩⟩, ⟨⟨⟨2, ⟨1, 
                1⟩⟩, ⟨1, ⟨1, 
                0⟩⟩⟩, ⟨⟨1, ⟨2, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

Critical Pair Difference

Expand[-x (x (y^2) + 3  x + 3) + 
        y ((x^2) y + 3  y + 4)]

Compute[
      (Underscript[cpd, ℙ])[⟨⟨1, ⟨1, 
              2⟩⟩, ⟨3, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨1, ⟨2, 
              1⟩⟩, ⟨3, ⟨0, 
              1⟩⟩, ⟨4, ⟨0, 
              0⟩⟩⟩]]

Groebner Basis

Compute[
      (Underscript[Gb, ℙ])[⟨⟩]]

GroebnerBasis[{ x + 4  y + 2, x y + 4 x + 3}, {x, y}, 
      MonomialOrder -> DegreeLexicographic, 
      CoefficientDomain -> Integers]

Compute[
      (Underscript[rdGb, ℙ])[⟨⟨⟨1, ⟨1, 
                0⟩⟩, ⟨4, ⟨0, 
                1⟩⟩, ⟨2, ⟨0, 
                0⟩⟩⟩, ⟨⟨1, ⟨1, 
                1⟩⟩, ⟨4, ⟨1, 
                0⟩⟩, ⟨3, ⟨0, 
                0⟩⟩⟩⟩]]

This is not yet what a "complete" reduction yields because the particular reduction multiplier function which we implemented in the Groebner extension functor only reduces the leading monomial!

We could carry out the reduction of the second polynomial in the basis by computing

\(Compute[⟨⟨\(-4\), ⟨0, 
              2⟩⟩, ⟨4, ⟨1, 
              0⟩⟩, ⟨\(-2\), ⟨0, 
              1⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩\( - \+ℙ\)\((\ ⟨⟨4, ⟨0, 
                  0⟩⟩⟩\(*\+ℙ\)⟨⟨1, ⟨1, 
                  0⟩⟩, ⟨4, ⟨0, 
                  1⟩⟩, ⟨2, ⟨0, 
                  0⟩⟩⟩)\)]\)

Then we would get the completely reduced Groebner basis

⟨⟨⟨1, ⟨1, 
            0⟩⟩, ⟨4, ⟨0, 
            1⟩⟩, ⟨2, ⟨0, 
            0⟩⟩⟩, ⟨⟨-4, ⟨0, 
            2⟩⟩, ⟨-18, ⟨0, 
            1⟩⟩, ⟨-5, ⟨0, 
            0⟩⟩⟩⟩

which is identical to the result of the Mathematica computation

Here is another example:

GroebnerBasis[{ x (y^2) + 4  y + 2, (x^2) y + 4 x + 3}, {x, y}, 
        MonomialOrder -> DegreeLexicographic,  
        CoefficientDomain -> Integers] // Timing

Compute[
        (Underscript[rdGb, ℙ])[⟨⟨⟨1, ⟨1, 
                  2⟩⟩, ⟨4, ⟨0, 
                  1⟩⟩, ⟨2, ⟨0, 
                  0⟩⟩⟩, ⟨⟨1, ⟨2, 
                  1⟩⟩, ⟨4, ⟨1, 
                  0⟩⟩, ⟨3, ⟨0, 
                  0⟩⟩⟩⟩]] // Timing

The polynomial

⟨⟨1, ⟨2, 
          1⟩⟩, ⟨4, ⟨1, 
          0⟩⟩, ⟨3, ⟨0, 
          0⟩⟩⟩

can be reduced further modulo

⟨⟨-2, ⟨1, 
            0⟩⟩, ⟨3, ⟨0, 
            1⟩⟩⟩.

Namely,

Compute[
      (Underscript[rd, ℙ])[⟨⟨4, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              0⟩⟩⟩, ⟨⟨-2, ⟨1, 
              0⟩⟩, ⟨3, ⟨0, 
              1⟩⟩⟩]]

so that we obtain the same Groebner basis as by the Mathematica computation.

Conclusions

The study in this paper could be extended in many different ways:

Introduce a functor for forming residue class domains modulo congruences and apply it for building up, independently of the built-in functions of Mathematica, the integers.

Use the residue class functor for introducing domains with algebraic numbers over fields.

Introduce a functor for quotient fields over integral domains and apply it for building the rational numbers from the integers and the rational functions over polynomial domains.  This will need also an application of the  the residue domains functor.

Apply the polynomial functor for the special case of univariate polynomials and use univariate polynomials as coefficient domain of multivariate polynomials.

Introduce polynomial functors for other representations of the polynomials. In particular introduce a functor that obtains the "standard" representation of polynomials as fully expanded and canonically ordered arithmetical terms over a set of indeterminates. Show the isomorphism of the various polynomial representations.

Study the effect on the efficiency of computations if a tower of functor applications for special domains is replaced by a special functor for the particular combinations of functors and study the trade-off between genericity and efficiency.

Give a set of axioms ("Groebner axioms") of the operations in a reduction ring that guarantee that in the Groebner bases construction described in the Groebner extension functor yields ideal bases that have the fundamental properties of Groebner bases. These axioms should, in addition, be such that, if a reduction ring satisfies the axioms, then also the polynomial ring over the reduction ring satisfies the axioms. (See [Buchberger 1984] for an answer to this question in a slightly different setting.)

Introduce other general functors on domains, as for example the Cartesian product functor, and check whether the Groebner axioms are preserved by these functors.

Extend the Groebner extension functor by various different reduction functions and by further functions for applying Groebner bases theory to the various fundamental problems in ideal theory as, for example, the syzygies problem (solution of systems of linear diophantine equations in reduction rings).

Extend the Groebner extension functor by improved algorithms for the construction of Groebner bases (criteria for detecting zero reductions, p-adic construction, basis conversion, Groebner walk, and linear algebra reduction).

References

[Buchberger 1984] 
B. Buchberger. A Critical-Pair/Completion Algorithm for Finitely Generated Ideals in Rings. In: E. Börger, G. Hasenjaeger, D. Rödding (eds), Logic and Machines: Decision Problems and Complexity (Proceedings of the Symposium "Rekursive Kombinatorik", Münster, May 23-28, 1983), Lecture Notes in Computer Science, Vol. 171, Springer, 1984, pp. 137-161.

[Buchberger 1991]
B. Buchberger. Gröbner Bases in Mathematica: Enthusiasm and Frustration. In: P. W. Gaffney, E. N. Houstis (eds.), Proceedings of the IFIP Working Conference on Programming Environments for High-Level Symbolic Computation, September 23-27, 1991, Karlsruhe, Germany, pp. 80-91.

[Buchberger 1996] 
B. Buchberger. Mathematica as a Rewrite Language. In: T. Ida, A. Ohori, M. Takeichi (eds.), Functional and Logic Programming (Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming, November 1-4, 1996, Shonan Village Center), World Scientific, Singapore - New Jersey - London - Hongkong, 1996, pp. 1-13.

[Buchberger et al. 2000]
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger. The Theorema Project: A Progress Report. In: M. Kerber and M. Kohlhase (eds.), Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, August 6-7, 2000, St. Andrews, Scotland),  A.K. Peters, Natick, Massachusetts, pp. 98-113.

[Milner et al. 1997] 
R. Milner, M. Tofte, R. Harper, D. MacQueen.  The Definition of Standard ML. MIT Press, 1997.
Paulson.  SML.

[Tomuta 1998]
E. Tomuta. Functor Proving in Theorema. PhD Thesis, Research Institute for Symbolic Computation, Johannes Kepler University, A4040 Linz, Austria, 1998..

[Stifter 1984]
S. Stifter. A Generalization of Reduction Rings. Journal of Symbolic Computation, Vol. 4, 1987, pp. 351-364.