(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 4.2' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 374386, 10782]*) (*NotebookOutlinePosition[ 409326, 11954]*) (* CellTagsIndexPosition[ 407790, 11923]*) (*WindowFrame->Normal*) Notebook[{ Cell[CellGroupData[{ Cell["\<\ Groebner Rings in TH\[Exists]OREM\[ForAll]: A Case Study in Functors and Categories\ \>", "Title", TextAlignment->Center, TextJustification->0], Cell["\<\ Bruno Buchberger RISC (Research Institute for Symbolic Computation) Johannes Kepler University A4232 Castle of Hagenberg, Austria Bruno.Buchberger@RISC.Uni-Linz.ac.at\ \>", "Subtitle", TextAlignment->Center, TextJustification->0, Background->GrayLevel[1]], Cell["Version 2003-11-15", "Text"], Cell[TextData[{ StyleBox["Acknowledgement", FontWeight->"Bold"], ": The research in this paper was sponsored by the Austrian FWF (Austrian \ Science Foundation, \[CapitalODoubleDot]sterreichischer Fonds zur F\ \[ODoubleDot]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." }], "Text"], Cell[CellGroupData[{ Cell["Introduction", "Section"], Cell[CellGroupData[{ Cell["The Objectives of This Paper", "Subsection"], Cell["This paper has two objectives:", "Text"], Cell[TextData[{ "provide a major ", StyleBox["case study for the use of categories and functors", FontWeight->"Bold"], " in ", StyleBox["Theorema, ", FontSlant->"Italic"], "introduced in [Buchberger 1996]," }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{56.8125, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "provide a formulation of the main algorithms in ", StyleBox["Groebner bases theory in a generic way", FontWeight->"Bold"], " based on (a new variant of) the notion of reduction ring introduced in \ [Buchberger 1984]." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{56.8125, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "All the ", StyleBox["Theorema", FontSlant->"Italic"], " 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." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Domains, Functors, and Categories", "Subsection"], Cell["\<\ 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:\ \>", "Text"], Cell[TextData[{ StyleBox["The computational aspect of functors: ", FontWeight->"Bold"], "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." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{56.8125, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ StyleBox["The reasoning aspect of functors:", FontWeight->"Bold"], " 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 \"", StyleBox["conservation theorems", FontWeight->"Bold"], "\". These are theorems that of the following structure:" }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{56.8125, Inherited}, {Inherited, Inherited}}], Cell["\<\ If domains U, V, ... are in the categories \[ScriptCapitalC], \ \[ScriptCapitalD], ... then F[ U, V, ...] is in category \[ScriptCapitalH].\ \>", "Text", CellMargins->{{59.1875, Inherited}, {Inherited, Inherited}}], Cell["\<\ (Example of a typical conservation theorem: If C is a ring then the \ polyonomial domain over C is also a ring.)\ \>", "Text"], Cell[TextData[{ "Our ", StyleBox["Theorema", FontSlant->"Italic"], " 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:" }], "Text"], Cell["\<\ 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.\ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{56.8125, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "It allows the formulation of categories and conservation theorems within \ the same language, namely ", StyleBox["Theorema", FontSlant->"Italic"], ", and also aims at providing automated reasoning facilities for \ conservation theorems (as part of a general methodology for automated \ proofs)." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{56.8125, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ "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 ", StyleBox["Theorema", FontSlant->"Italic"], ", 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:" }], "Text"], Cell[BoxData[ \(\(\(\(D[f]\)[x, y]\)\(.\)\)\)], "Input"], Cell["\<\ 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\ \>", "Text"], Cell[BoxData[ \(f\+D[x, y]\)], "Input"], Cell["for", "Text"], Cell[BoxData[ \(\(\(\(D[f]\)[x, y]\)\(.\)\)\)], "Input"], Cell["\<\ 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 \[Epsilon], i.e.\ \>", "Text"], Cell[BoxData[ RowBox[{" ", RowBox[{ FormBox[\(\[Epsilon]\+D\), "TraditionalForm"], " ", "[", "x", "]"}], " "}]], "Input"], Cell["\<\ yields true or false depending on whether or not the input x belongs to D. \ (Note that we use the Greek letter '\[Epsilon]' and not the set theory \ element symbol '\[Element]' 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.)\ \>", "Text"], Cell["\<\ 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.\ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["An Example of a Functor", "Subsection"], Cell[TextData[{ "Let's formulate, in ", StyleBox["Theorema", FontSlant->"Italic"], " notation, the functor CP that takes a domain D with operation + and forms \ the \"Cartesian product\" of D with D" }], "Text"], Cell[BoxData[ RowBox[{\(Cartesian\[Dash]Product[D]\), "=", RowBox[{"Functor", "[", RowBox[{ "N", ",", \(any[X, x1, x2, y1, y2]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\(+\(\(\[Colon]\)\(N\ \[Cross]N \[Rule] N\)\)\)\[RightAngleBracket]\)}, {GridBox[{ {\(\[Epsilon]\+N[ X] \[DoubleLeftRightArrow] \((is\[Dash]tuple[ X] \[And] \((\[LeftBracketingBar]X\ \[RightBracketingBar] = 2)\) \[And] \[Epsilon]\+D[X\_1] \[And] \[Epsilon]\+D[ X\_2])\)\)}, {\(\[LeftAngleBracket]x1, x2\[RightAngleBracket]\( + \+N\)\ \[LeftAngleBracket]y1, y2\[RightAngleBracket] = \[LeftAngleBracket]x1\( \ + \+D\)y1, x2\( + \+D\)y2\[RightAngleBracket]\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]], "Input"], Cell[TextData[{ "This shold be understood as follows: Assume that we have a domain D with \ the unary decision predicate ", Cell[BoxData[ \(\[Epsilon]\+D\)]], " and a binary function ", Cell[BoxData[ \(+\+D\)]], ". Then ", "Cartesian\[Dash]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" }], "Text"], Cell[BoxData[ \(\(\(\[ForAll] \+X\)\((\[Epsilon]\+N[ X] \[DoubleLeftRightArrow] \((is\[Dash]tuple[ X] \[And] \((\[LeftBracketingBar]X\[RightBracketingBar] = 2)\) \[And] \[Epsilon]\+D[X\_1] \[And] \[Epsilon]\+D[ X\_2])\))\)\(\ \)\)\)], "Input"], Cell[TextData[{ "where is\[Dash]tuple is a fixed predicate that decides whether a given \ object is a tuple, i.e. an object of the form \[LeftAngleBracket]a1,...,an\ \[RightAngleBracket] and \[LeftBracketingBar]X \[RightBracketingBar] denotes \ the length of tuple X. In words: ", Cell[BoxData[ \(\[Epsilon]\+N[X]\)]], ", i.e. X belongs to N, iff X is a tuple of length 2 and ", Cell[BoxData[ \(\[Epsilon]\+D[X\_1]\)]], ", i.e. the first component of X belongs to D, and also ", Cell[BoxData[ \(\[Epsilon]\+D[X\_2]\)]], ", i.e. the second component of X belongs to D. The information \ \[DoubleStruckS]= \[LeftAngleBracket]+\[Colon] N\[Cross]N\[Rule]N\ \[RightAngleBracket] 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 +\[Colon]N\[Cross]N\[Rule]N is a guarantee that the function \ ", Cell[BoxData[ \(+\+N\)]], " is indeed a binary function, i.e. maps objects satisfying ", Cell[BoxData[ \(\[Epsilon]\+N\)]], " to objects satisfying ", Cell[BoxData[ \(\[Epsilon]\+N\)]], ". (Such a guarantee needs a proof like the proof of any other property you \ assert about the operations defined in N, see below.)" }], "Text"], Cell["The definition", "Text"], Cell[BoxData[ \(\[LeftAngleBracket]x1, x2\[RightAngleBracket]\( + \+N\)\[LeftAngleBracket]y1, y2\[RightAngleBracket] = \[LeftAngleBracket]x1\( + \+D\)y1, x2\( + \+D\)y2\[RightAngleBracket]\)], "Input"], Cell[TextData[{ "describes the fact that the operation ", Cell[BoxData[ \(+\+N\)]], " in the new domain N is defined on tuples and is defined component-wised \ using the operation ", Cell[BoxData[ \(+\+D\)]], " in D on the components. Note that the operation ", Cell[BoxData[ \(+\+N\)]], " is intended to be defined on objects satisfying ", Cell[BoxData[ \(\[Epsilon]\+N\)]], ". However, as it stands, the operation will also give values on objects \ not satisfying ", Cell[BoxData[ \(\[Epsilon]\+N\)]], " but, typically, it will not be possible to prove anything on these values \ because, typically, nothing will be known on the values of ", Cell[BoxData[ \(x1\( + \+D\)y1\)]], " and ", Cell[BoxData[ \(x2\( + \+D\)y2\)]], " in case x1, y1, x2, y2 do not satisfy ", Cell[BoxData[ \(\[Epsilon]\+D\)]], "." }], "Text"], Cell[TextData[{ "Note that the ", StyleBox["Theorema", FontSlant->"Italic"], " 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:" }], "Text"], Cell[BoxData[ RowBox[{\(Cartesian\[Dash]Product[D]\), "=", RowBox[{\(such\ an\ N\ that\), "\[IndentingNewLine]", "\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], RowBox[{GridBox[{ {\(\[ForAll] \+X\((\[Epsilon]\+N[ X] \[DoubleLeftRightArrow] \((is\[Dash]tuple[ X] \[And] \((\[LeftBracketingBar]X\ \[RightBracketingBar] = 2)\) \[And] \[Epsilon]\+D[X\_1] \[And] \[Epsilon]\+D[ X\_2])\))\)\)}, {\(\[ForAll] \+\(x1, x2, y1, y2\)\((\[LeftAngleBracket]x1, x2\[RightAngleBracket]\( + \+N\)\ \[LeftAngleBracket]y1, y2\[RightAngleBracket] = \[LeftAngleBracket]x1\( \ + \+D\)y1, x2\( + \+D\)y2\[RightAngleBracket])\)\)} }, ColumnAlignments->{Left}], " ", ".", " "}]}]}]}]], "Input"], Cell["\<\ 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.\ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Computing with the Functor", "Subsection"], Cell[TextData[{ "In ", StyleBox["Theorema", FontSlant->"Italic"], ", 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 ", StyleBox["Theorema", FontSlant->"Italic"], " provers for proving propositions. In contrast, in ", StyleBox["Theorema", FontSlant->"Italic"], " 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." }], "Text"], Cell[TextData[{ "We illustrate now for the above example functor, how one can call the \ functor in a typical computation in the frame of a ", StyleBox["Theorema", FontSlant->"Italic"], " standard session. (In the current version of ", StyleBox["Theorema", FontSlant->"Italic"], ", functors are not yet available in computational sessions.)" }], "Text"], Cell[TextData[{ "First of all, we have to initialize ", StyleBox["Theorema", FontSlant->"Italic"], " by executing (within Mathematica)" }], "Text"], Cell[BoxData[ \(Needs["\"]\)], "Input"], Cell[TextData[{ "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 ", StyleBox["Theorema", FontSlant->"Italic"], " construct into a Mathematica input cell: " }], "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", ",", \(any[D]\), ",", "\[IndentingNewLine]", RowBox[{\(Cartesian\[Dash]Product[D]\), "=", RowBox[{"Functor", "[", RowBox[{ "N", ",", \(any[X, x1, x2, y1, y2]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\[Epsilon]\+N[ X] \[DoubleLeftRightArrow] \((is\[Dash]tuple[ X] \[And] \((\[LeftBracketingBar]X\ \[RightBracketingBar] = 2)\) \[And] \[Epsilon]\+D[X\_1] \[And] \[Epsilon]\+D[ X\_2])\)\)}, {\(\[LeftAngleBracket]x1, x2\[RightAngleBracket]\( + \+N\)\ \[LeftAngleBracket]y1, y2\[RightAngleBracket] = \ \[LeftAngleBracket]x1\( + \+D\)y1, x2\( + \+D\)y2\[RightAngleBracket]\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]}], "]"}]], "Input", CellTags->"Definition (Cartesian Product)"], Cell["Note that the \"any[D]\" construct declares 'D' as a variable.", "Text"], Cell["\<\ 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:\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[]\), ",", "\[IndentingNewLine]", RowBox[{\(Integer\[Dash]Numbers[]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\[Epsilon]\+N[x] \[DoubleLeftRightArrow] is\[Dash]integer[x]\)}, {\(x\( + \+N\)y = x + y\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]}], "]"}]], "Input", CellTags->"Definition (Integer Numbers)"], Cell[TextData[{ "Here, 'is\[Dash]integer' and '+' should refer to the Mathematica \ operations 'IsInteger' and '+'. For enforcing this, we have the 'Built-in' \ construct in ", StyleBox["Theorema", FontSlant->"Italic"], ", which allows to access functions programmed in Mathematica from within \ ", StyleBox["Theorema", FontSlant->"Italic"], " in a controlled way. This means that, in any computation or proof, ", StyleBox["Theorema", FontSlant->"Italic"], " uses exclusively those operations that are either explicitly defined by a \ ", StyleBox["Theorema", FontSlant->"Italic"], " definition or are explicitly mentioned in a 'Built-in' declaration." }], "Text"], Cell["\<\ 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\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(\[DoubleStruckCapitalZ] = Integer\[Dash]Numbers[]\)}, {\(\[DoubleStruckCapitalP] = Cartesian\[Dash]Product[\[DoubleStruckCapitalZ]]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Definition (Domains)"], Cell["\<\ 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\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Theory", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\"]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Theory (T)"], Cell["\<\ Now we can evaluate arbitrary expressions over \[DoubleStruckCapitalZ] and \ \[DoubleStruckCapitalP] using this theory and the built-in operations on \ (integer) numbers, tuples and propositional connectives. For example, if we \ enter\ \>", "Text"], Cell[BoxData[ \(Compute[2\( + \+\[DoubleStruckCapitalZ]\)3, using \[Rule] \[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell["we obtain", "Text"], Cell[BoxData[ \(5\)], "Output"], Cell["Also, entering", "Text"], Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ][3], using \[Rule] \[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell["yields", "Text"], Cell[BoxData[ \(True\)], "Output"], Cell[BoxData[ \(True\)], "Output"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ][3.5], using \[Rule] \[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ][ 2\( + \+\[DoubleStruckCapitalZ]\)3], using \[Rule] \[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[LeftAngleBracket]4, 7\[RightAngleBracket]\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 14\[RightAngleBracket], using \[Rule] \[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]6, 21\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[TextData[{ "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 ", StyleBox["Theorema", FontSlant->"Italic"], " 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:" }], "Text"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell["Now, ", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[2\( + \+\[DoubleStruckCapitalZ]\)3]\)], "Input"], Cell[BoxData[ \(5\)], "Output"] }, Open ]], Cell["and also", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ][3]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ][3.5]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ][ 2\( + \+\[DoubleStruckCapitalZ]\)3]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[LeftAngleBracket]4, 7\[RightAngleBracket]\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 14\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]6, 21\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\((\[LeftAngleBracket]4, 7\[RightAngleBracket]\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 14\[RightAngleBracket])\)\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 2\( + \+\[DoubleStruckCapitalZ]\)3\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]8, 26\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalP][\[LeftAngleBracket]\(-7\), 18\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalP][\[LeftAngleBracket]\(-7\), 18.5\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalP][\[LeftAngleBracket]\(-7\), 18, 3\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell["Let's also try", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalP][\[LeftAngleBracket]x, 18\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(IsInteger[x]\)], "Output"] }, Open ]], Cell["Note that the answer is just a simplified version of ", "Text"], Cell[BoxData[ \(\((is\[Dash]tuple[\[LeftAngleBracket]x, 18\[RightAngleBracket]] \[And] \((\[LeftBracketingBar]\ \[LeftAngleBracket]x, 18\[RightAngleBracket]\[RightBracketingBar] = 2)\) \[And] \[Epsilon]\+\[DoubleStruckCapitalZ][\ \[LeftAngleBracket]x, 18\[RightAngleBracket]\_1] \[And] \[Epsilon]\+\ \[DoubleStruckCapitalZ][\[LeftAngleBracket]x, \ 18\[RightAngleBracket]\_2])\)\)], "Input"], Cell[TextData[{ "for the constant x about which we have no knowledge: is\[Dash]tuple[\ \[LeftAngleBracket]x,18\[RightAngleBracket]] can be simplified to true also \ without any knowledge on x, also ( \[LeftBracketingBar]\[LeftAngleBracket] \ x, 18\[RightAngleBracket]\[RightBracketingBar] = 2) can be simplified to true \ without any knowledge on x. However, determining the truth value of ", Cell[BoxData[ \(\[Epsilon]\+D[\[LeftAngleBracket]x, 18\[RightAngleBracket]\_1]\)]], " needs the answer to the question whether ", Cell[BoxData[ \(\[Epsilon]\+\[DoubleStruckCapitalZ]\)]], "[x], i.e. whether is\[Dash]integer[x], which internally in Mathematica \ leads to calling IsInteger[x]. This cannot be decided because nothing is \ known about x." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Another Parameter Domain", "Subsection"], Cell["Now let's define another domain by", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[]\), ",", "\[IndentingNewLine]", RowBox[{\(Strange\[Dash]Numbers[]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\[Epsilon]\+N[x] \[DoubleLeftRightArrow] is\[Dash]integer[x]\)}, {\(x\( + \+N\)y = x*y\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]}], "]"}]], "Input", CellTags->"Definition (Strange Numbers)"], Cell["\<\ and feed this domain into the functor Cartesian\[Dash]Product for studying \ the dependence of the domain generated by a functor from the input domain.\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(\[DoubleStruckCapitalS] = Strange\[Dash]Numbers[]\)}, {\(\[DoubleStruckCapitalP] = Cartesian\[Dash]Product[\[DoubleStruckCapitalS]]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Definition (Domains)"], Cell[BoxData[ RowBox[{ StyleBox["Theory", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\"]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Theory (T)"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"], Cell["\<\ Now study and explain the results of each of the following evaluations:\ \>", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[2\( + \+\[DoubleStruckCapitalS]\)3]\)], "Input"], Cell[BoxData[ \(6\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalS][3]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalS][3.5]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[LeftAngleBracket]4, 7\[RightAngleBracket]\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 14\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]8, 98\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\((\[LeftAngleBracket]4, 7\[RightAngleBracket]\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 14\[RightAngleBracket])\)\( + \+\[DoubleStruckCapitalP]\)\ \[LeftAngleBracket]2, 2\( + \+\[DoubleStruckCapitalS]\)3\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]16, 588\[RightAngleBracket]\)], "Output"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["An Example Category and Conservation Theorem", "Subsection"], Cell[TextData[{ StyleBox["Now let's define a trivial category in ", "H\[OSlash]Z"], StyleBox["Theorema", FontSlant->"Italic"], ":" }], "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", ",", \(any[D, \[SmallCircle]]\), ",", "\[IndentingNewLine]", RowBox[{\(\(is\[Dash]commutid[ D, \[SmallCircle]]\)\(\[DoubleLeftRightArrow]\)\), "\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(\[ForAll] \+\(\[Epsilon]\+D[x, y]\)\[Epsilon]\+D[ x\(\[SmallCircle]\+D\)y]\)}, {\(\[ForAll] \+\(\[Epsilon]\+D[x, y]\)\((x\(\[SmallCircle]\+D\ \)y = y\(\[SmallCircle]\+D\)x)\)\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]}], " ", "]"}]], "Input", CellTags->"Definition (Commutid)"], Cell[TextData[{ "In words: D is a \"commutid\" w.r.t. the operation \[SmallCircle] in D \ iff, for all objects x and y belonging to D, ", Cell[BoxData[ \(x\(\[SmallCircle]\+D\)y\)]], " belong also to D and, for all objects x and y belonging to D, ", Cell[BoxData[ \(x\(\[SmallCircle]\+D\)y\)]], " is equal to ", Cell[BoxData[ \(y\(\[SmallCircle]\+D\)x\)]], ". Note again that, in this definition, 'D' and '\[SmallCircle]' are free \ variables whereas 'is\[Dash]commutatid' is a constant." }], "Text"], Cell["\<\ For getting acquainted with the underscript notation for operations in \ domains it is telling to look at\ \>", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Definition["\"]\)], "Input"], Cell[BoxData[ RowBox[{"\[Bullet]def", "[", RowBox[{"\<\"Commutid\"\>", ",", RowBox[{"\[Bullet]range", "[", RowBox[{ RowBox[{"\[Bullet]simpleRange", "[", StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], ",", RowBox[{"\[Bullet]simpleRange", "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}], "]"}], ",", "True", ",", RowBox[{"\[Bullet]flist", "[", RowBox[{"\[Bullet]lf", "[", RowBox[{"\<\"\"\>", ",", RowBox[{ RowBox[{"is\[Dash]commutid", "[", RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "\[DoubleLeftRightArrow]", RowBox[{ RowBox[{ UnderscriptBox["\[ForAll]", GridBox[{ { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}, { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]} }]], RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "[", RowBox[{ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "]"}]}], "\[And]", RowBox[{ UnderscriptBox["\[ForAll]", GridBox[{ { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}, { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]} }]], RowBox[{"(", RowBox[{ RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "[", RowBox[{ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "=", RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "[", RowBox[{ StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]}], ")"}]}]}]}]}], "]"}], "]"}]}], "]"}]], "Output"] }, Open ]], Cell[TextData[{ "which produces the definition in the internal prefix form of ", StyleBox["Theorema", FontSlant->"Italic"], " as a nested (Mathematica expression)" }], "Text"], Cell[BoxData[ RowBox[{"\[Bullet]def", "[", RowBox[{"\<\"Commutid\"\>", ",", RowBox[{"\[Bullet]range", "[", RowBox[{ RowBox[{"\[Bullet]simpleRange", "[", StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], ",", RowBox[{"\[Bullet]simpleRange", "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}], "]"}], ",", "True", ",", RowBox[{"\[Bullet]flist", "[", RowBox[{"\[Bullet]lf", "[", RowBox[{"\<\"\"\>", ",", RowBox[{ RowBox[{"is\[Dash]commutid", "[", RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "\[DoubleLeftRightArrow]", RowBox[{ RowBox[{ UnderscriptBox["\[ForAll]", GridBox[{ { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}, { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]} }]], RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "[", RowBox[{ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "]"}]}], "\[And]", RowBox[{ UnderscriptBox["\[ForAll]", GridBox[{ { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]}, { RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", "\[Epsilon]", "]"}], "[", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}]} }]], RowBox[{"(", RowBox[{ RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "[", RowBox[{ StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "=", RowBox[{ RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], "[", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None], "]"}], "[", RowBox[{ StyleBox["y", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["x", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}]}], ")"}]}]}]}]}], "]"}], "]"}]}], "]"}]], "Output"], Cell[TextData[{ "Note that, as range description of a quantifier, we can use ", Cell[BoxData[ \(\[Epsilon]\+D[x, y]\)]], " as an abbreviation for ", Cell[BoxData[ \(\[Epsilon]\+D[x]\)]], ",", Cell[BoxData[ \(\[Epsilon]\+D[y]\)]], "." }], "Text"], Cell["\<\ Now we can formulate, for example, the following conservation theorem:\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Theorem", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", RowBox[{"any", "[", RowBox[{"D", ",", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], ",", "\[IndentingNewLine]", RowBox[{ RowBox[{"is\[Dash]commutid", "[", RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], "\[Implies]", \(is\[Dash]commutid[ Cartesian\[Dash]Product[D], \[SmallCircle]]\)}]}], "]"}]], "Input",\ CellTags->"Theorem (Cartesian Products of Commutids)"], Cell[TextData[{ "It is the ultimate goal of ", StyleBox["Theorema", FontSlant->"Italic"], " 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." }], "Text"], Cell[TextData[{ "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 ", StyleBox["Theorema", FontSlant->"Italic"], ". However, the implementation done in this dissertation is not any more \ integrated into the current version of ", StyleBox["Theorema", FontSlant->"Italic"], ". 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 ", StyleBox["Theorema", FontSlant->"Italic"], "." }], "Text"], Cell["\<\ For explaining the typical structure of proofs of conservation theorems, let \ us do the proof of the Theorem[\"Cartesian Products of Commutids\"] by hand: \ \ \>", "Text"], Cell["Assume ", "Text"], Cell[BoxData[ RowBox[{ RowBox[{"is\[Dash]commutid", "[", RowBox[{ StyleBox["D", FontWeight->"Plain", FontSlant->"Italic", Background->None], ",", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], ","}]], "Input"], Cell["i.e.", "Text"], Cell[BoxData[GridBox[{ {\(\(\[ForAll] \+\(\[Epsilon]\+D[x, y]\)\[Epsilon]\+D[ x\(\[SmallCircle]\+D\)y]\)\(,\)\), \((A1)\)}, {\(\(\[ForAll] \+\(\[Epsilon]\+D[x, y]\)\((x\(\[SmallCircle]\+D\)y = y\(\[SmallCircle]\+D\)x)\)\)\(,\)\), \((A2)\)} }, ColumnAlignments->{Left}]], "Input"], Cell["let ", "Text"], Cell[BoxData[ \(\(\(P = Cartesian\[Dash]Product[D]\)\(,\)\)\)], "Input"], Cell["and show", "Text"], Cell[BoxData[ RowBox[{ RowBox[{"is\[Dash]commutid", "[", RowBox[{"P", ",", StyleBox["\[SmallCircle]", FontWeight->"Plain", FontSlant->"Italic", Background->None]}], "]"}], ","}]], "Input"], Cell["i.e.", "Text"], Cell[BoxData[GridBox[{ {\(\(\[ForAll] \+\(\[Epsilon]\+P[x, y]\)\[Epsilon]\+P[ x\(\[SmallCircle]\+P\)y]\)\(,\)\), \((G1)\)}, {\(\[ForAll] \+\(\[Epsilon]\+P[x, y]\)\(\((x\(\[SmallCircle]\+P\)y = y\(\[SmallCircle]\+P\)x)\)\(.\)\)\), \((G2)\)} }, ColumnAlignments->{Left}]], "Input"], Cell["Now assume", "Text"], Cell[BoxData[GridBox[{ {\(\(\[Epsilon]\+P[x]\)\(,\)\)}, {\(\(\[Epsilon]\+P[y]\)\(,\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell["i.e. for certain x1, x2, y1, y2", "Text"], Cell[BoxData[GridBox[{ {\(\(x = \[LeftAngleBracket]x1, x2\[RightAngleBracket]\)\(,\)\)}, {\(\(\[Epsilon]\+D[x1]\)\(,\)\)}, {\(\(\[Epsilon]\+D[x2]\)\(,\)\)}, {\(\(y = \[LeftAngleBracket]y1, y2\[RightAngleBracket]\)\(,\)\)}, {\(\(\[Epsilon]\+D[x1]\)\(,\)\)}, {\(\(\[Epsilon]\+D[x2]\)\(,\)\)} }, ColumnAlignments->{Left}]], "Input"], Cell["and show", "Text"], Cell[BoxData[ \(\(\(\[Epsilon]\+P[x\(\[SmallCircle]\+P\)y]\)\(.\)\)\)], "Input"], Cell["Now,", "Text"], Cell[BoxData[ RowBox[{\(\[Epsilon]\+P[x\(\[SmallCircle]\+P\)y]\), " ", "\[LeftRightArrow]", " ", \(\[Epsilon]\+P[\[LeftAngleBracket]x1, x2\[RightAngleBracket]\(\[SmallCircle]\+P\)\[LeftAngleBracket]y1, y2\[RightAngleBracket]]\), " ", "\[LeftRightArrow]", " ", \(\[Epsilon]\+P[\[LeftAngleBracket]x1\(\[SmallCircle]\+D\)y1, x2\(\[SmallCircle]\+D\)y2\[RightAngleBracket]]\), " ", "\[LeftRightArrow]", GridBox[{ {\(is\[Dash]tuple[\[LeftAngleBracket]x1\(\[SmallCircle]\+D\)y1, x2\(\[SmallCircle]\+D\)y2\[RightAngleBracket]]\)}, {\(\[LeftBracketingBar]\[LeftAngleBracket]x1\(\[SmallCircle]\+D\)y1,\ x2\(\[SmallCircle]\+D\)y2\[RightAngleBracket] = 2\[RightBracketingBar]\)}, {\(\[Epsilon]\+D[x1\(\[SmallCircle]\+D\)y1]\)}, {\(\[Epsilon]\+D[x2\(\[SmallCircle]\+D\)y2]\)} }, ColumnAlignments->{Left}], " ", \( \[LeftRightArrow] \&\(by\ \((A1)\)\)\), " ", \(\(true\)\(.\)\)}]], "Input"], Cell["Similarly, (G2) can be proved.", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["The Reduction Ring Approach to Groebner Bases", "Subsection"], Cell[TextData[{ "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 ", StyleBox["Theorema", FontSlant->"Italic"], ", [Buchberger et al. 1997, 2000]. " }], "Text"], Cell["\<\ 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.\ \>", "Text"], Cell["\<\ 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.\ \>", "Text"], Cell[TextData[{ "In this paper, we carry this approach through in all details, as far as \ the computational aspect is concerned, using the functor mechanism of ", StyleBox["Theorema", FontSlant->"Italic"], ". 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 ", StyleBox["Theorema", FontSlant->"Italic"], " projects that such proofs can be generated automatically or at least \ computer-supported in the future." }], "Text"], Cell["\<\ The three operations, that are added in reduction rings to the ordinary ring \ operations, have the following objective and significance:\ \>", "Text"], Cell[TextData[{ StyleBox["The predicate >", FontWeight->"Bold"], ": 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." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{58.375, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ StyleBox["The operation rdm \"reducing multiplier\": ", FontWeight->"Bold"], "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." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{58.375, Inherited}, {Inherited, Inherited}}], Cell[TextData[{ StyleBox["The operation lcrd \"least common reducible\": ", FontWeight->"Bold"], "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 ", Cell[BoxData[ \(TraditionalForm\`Z\_1\)]], ":= Z - rdm[ Z, x] * x and then further on to an irreducible element a and \ by going from Z to ", Cell[BoxData[ \(TraditionalForm\`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\" ", Cell[BoxData[ \(TraditionalForm\`Z\_1\)]], " - ", Cell[BoxData[ \(TraditionalForm\`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." }], "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{58.375, Inherited}, {Inherited, Inherited}}], Cell["\<\ 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!)\ \>", "Text"], Cell[TextData[{ "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 ", StyleBox["not ", FontSlant->"Italic"], "take the ordinary less relation, which would not be Noetherian!)" }], "Text"], Cell["\<\ 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.\ \>", "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Preparation of Theorema", "Section"], Cell[CellGroupData[{ Cell["The Objective of this Section", "Subsection"], Cell[TextData[{ "In this section, we carry out a couple of technical steps for preparing ", StyleBox["Theorema", FontSlant->"Italic"], " for the tasks to be carried out in this notebook.", StyleBox[" First of all, start with a new Mathematica kernel by quitting \ the kernel using the appropriate line in the Mathematica menu.", FontWeight->"Bold"] }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["A Word on Computation and Complexity in Theorema", "Subsection"], Cell[TextData[{ "The ", StyleBox["Theorema", FontSlant->"Italic"], " 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 ", Cell[BoxData[ \(TraditionalForm\`\[ForAll] \+\(i = 1, ... , n\)\)]], "... etc." }], "Text"], Cell[TextData[{ "It is important to know that ", StyleBox["Theorema", FontSlant->"Italic"], " is implemented in the Mathematica language and, hence, we can not expect \ that algorithms expressed in ", StyleBox["Theorema", FontSlant->"Italic"], " 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.)" }], "Text"], Cell["\<\ 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, \ \>", "Text"], Cell["\<\ generality, structuredness and elegance of towers of domains and executable \ algorithms \ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{72.75, Inherited}, {Inherited, Inherited}}], Cell["\<\ and the possibility of proving properties of these algorithms.\ \>", "Text", CellDingbat->"\[EmptySmallCircle]", CellMargins->{{72.75, Inherited}, {Inherited, Inherited}}], Cell["\<\ 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. \ \>", "Text"], Cell[TextData[{ "We will consider speed in a later stage of the ", StyleBox["Theorema", FontSlant->"Italic"], " project when we will have clarified the logical frame of domain oriented \ and provenly correct computation within the current, slow ", StyleBox["Theorema", FontSlant->"Italic"], " 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 ", StyleBox["Theorema", FontSlant->"Italic"], ". We may still want to keep Mathematica as the implementation language for \ the logic part of ", StyleBox["Theorema", FontSlant->"Italic"], ", i.e. the implementation of provers, solvers, and simplifiers." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Additional Mathematica Functions", "Subsection"], Cell[BoxData[{ \(Clear[PFInverse, PFQuotient]\), "\[IndentingNewLine]", \(PFInverse[x_, p_] := \(ExtendedGCD[x, p]\)[\([2, 1]\)]\), "\[IndentingNewLine]", \(PFQuotient[x_, y_, p_] := Mod[x\ PFInverse[y, p], p]\)}], "Input"], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[1, 1, 5]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[1, 2, 5]\)], "Input"], Cell[BoxData[ \(3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[1, 3, 5]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[1, 4, 5]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[2, 1, 5]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[2, 2, 5]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[2, 3, 5]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[2, 4, 5]\)], "Input"], Cell[BoxData[ \(3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[3, 1, 5]\)], "Input"], Cell[BoxData[ \(3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[3, 2, 5]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[3, 3, 5]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[3, 4, 5]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[4, 1, 5]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[4, 2, 5]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[4, 3, 5]\)], "Input"], Cell[BoxData[ \(3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(PFQuotient[4, 4, 5]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Start Theorema", "Subsection"], Cell[TextData[{ "Now we start ", StyleBox["Theorema", FontSlant->"Italic"], " again by executing" }], "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Needs["\"]\)], "Input"], Cell[BoxData[ \("You can specify your personal preferences in a file `Setup.m` in the \ directory (folder) \"Theorema -> User\" in your private Theorema \ directory!"\)], "Print"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Correction", "Subsection"], Cell[TextData[{ "In the current version of ", StyleBox["Theorema", FontSlant->"Italic"], ", the following Mathematica function defintion must be entered" }], "Text"], Cell[BoxData[ \(\[LeftBracketingBar]\[LeftAngleBracket]x___? IsSequenceFree\[RightAngleBracket]\[RightBracketingBar] := Length[{x}]\)], "Input"], Cell[TextData[{ "for completing a definition in the ", StyleBox["Theorema", FontSlant->"Italic"], " package." }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell[TextData[{ "Make ", StyleBox["Mathematica", FontSlant->"Italic"], " Functions Accessible" }], "Subsection"], Cell[TextData[{ "The following ", StyleBox["Theorema", FontSlant->"Italic"], " command attaches certain ", StyleBox["Theorema", FontSlant->"Italic"], " names to certain Mathematica functions and makes them available for calls \ from within ", StyleBox["Theorema", FontSlant->"Italic"], ". (Note that all other functions from the Mathematica function library are \ hidden from ", StyleBox["Theorema", FontSlant->"Italic"], ". If you want more Mathematica functions to be accessible from within ", StyleBox["Theorema", FontSlant->"Italic"], " you should introduce them by a similar \"Built-in\" command.)" }], "Text"], Cell[BoxData[ RowBox[{ StyleBox["Built\[Dash]in", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(is\[Dash]even \[Rule] EvenQ\)}, {\(is\[Dash]odd \[Rule] OddQ\)}, {\(mod \[Rule] Mod\)}, {\(gcd \[Rule] GCD\)}, {\(lcm \[Rule] LCM\)}, {\(sign \[Rule] Sign\)}, {\(maximum \[Rule] Max\)}, {\(quotient \[Rule] Quotient\)}, {\(pf\[Dash]inverse \[Rule] PFInverse\)}, {\(pf\[Dash]quotient \[Rule] PFQuotient\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Built\[Dash]in (Mathematica general functions)"] }, Open ]], Cell[CellGroupData[{ Cell["Some Basic Functions Programmed in Theorema", "Subsection"], Cell["\<\ The following function 'pairs' computes a list consisting of all pairs of \ elements in a given list:\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", ",", \(any[a, x, x\&_]\), ",", "\[IndentingNewLine]", GridBox[{ {\(pairs[\[LeftAngleBracket]\[RightAngleBracket]] = \ \[LeftAngleBracket]\[RightAngleBracket]\)}, {\(pairs[\[LeftAngleBracket]x, x\&_\[RightAngleBracket]] = \[LeftAngleBracket]\(\ \[LeftAngleBracket]x, \[LeftAngleBracket]x\&_\[RightAngleBracket]\_i\ \[RightAngleBracket]\)\( \[VerticalSeparator] \+\(i = 1, \[Ellipsis], \[LeftBracketingBar]\ \[LeftAngleBracket]x\&_\[RightAngleBracket]\[RightBracketingBar]\)\)\ \[RightAngleBracket] \[CupCap] pairs[\[LeftAngleBracket]x\&_\[RightAngleBracket]]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Definition (Theorema general functions)"], Cell["For example", "Text"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Definition["\"]\[RightAngleBracket]]\)], \ "Input"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\ pairs[\[LeftAngleBracket]\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\ pairs[\[LeftAngleBracket]1\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\ pairs[\[LeftAngleBracket]1, 2, 3, 4, 5\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]\[LeftAngleBracket]1, 2\[RightAngleBracket], \[LeftAngleBracket]1, 3\[RightAngleBracket], \[LeftAngleBracket]1, 4\[RightAngleBracket], \[LeftAngleBracket]1, 5\[RightAngleBracket], \[LeftAngleBracket]2, 3\[RightAngleBracket], \[LeftAngleBracket]2, 4\[RightAngleBracket], \[LeftAngleBracket]2, 5\[RightAngleBracket], \[LeftAngleBracket]3, 4\[RightAngleBracket], \[LeftAngleBracket]3, 5\[RightAngleBracket], \[LeftAngleBracket]4, 5\[RightAngleBracket]\[RightAngleBracket]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\ pairs[\[LeftAngleBracket]1, 2, 1, 1, 2\[RightAngleBracket]]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]\[LeftAngleBracket]1, 2\[RightAngleBracket], \[LeftAngleBracket]1, 1\[RightAngleBracket], \[LeftAngleBracket]1, 1\[RightAngleBracket], \[LeftAngleBracket]1, 2\[RightAngleBracket], \[LeftAngleBracket]2, 1\[RightAngleBracket], \[LeftAngleBracket]2, 1\[RightAngleBracket], \[LeftAngleBracket]2, 2\[RightAngleBracket], \[LeftAngleBracket]1, 1\[RightAngleBracket], \[LeftAngleBracket]1, 2\[RightAngleBracket], \[LeftAngleBracket]1, 2\[RightAngleBracket]\[RightAngleBracket]\)], "Output"] }, Open ]] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["The Rationals in Decimal Representation as Field", "Section"], Cell[CellGroupData[{ Cell["Informal Explanation", "Subsection"], Cell[TextData[{ "We define a functor \"rational numbers field\" that constructs the domain \ of rational numbers in decimal notation in ", StyleBox["Theorema", FontSlant->"Italic"], ". 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). \ " }], "Text"], Cell[TextData[{ "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 ", StyleBox["Theorema", FontSlant->"Italic"], " we have the \"Built-in\" construct in ", StyleBox["Theorema", FontSlant->"Italic"], " that does not only allow to assign ", StyleBox["Theorema", FontSlant->"Italic"], " 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" }], "Text"], Cell[BoxData[ \(Built\[Dash]in["\"]\)], "Input"], Cell[BoxData[ \(Built\[Dash]in["\"]\)], "Input"], Cell[BoxData[ \(Built\[Dash]in["\"]\)], "Input"], Cell[BoxData[ \(Built\[Dash]in["\"]\)], "Input"], Cell[BoxData[ \(Built\[Dash]in["\"]\)], "Input"], Cell["\<\ 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.\ \>", "Text"], Cell[TextData[{ "In order to access these boundles of operations in ", StyleBox["Theorema", FontSlant->"Italic"], ", one can start their accessibility by calling them individually like, for \ example," }], "Text"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"]\[RightAngleBracket]\ ]\)], "Input"], Cell["or collectively, like", "Text"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"]\[RightAngleBracket]]\)], "Input"], Cell["\<\ 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 \[Rule]' optional parameter into \ the Compute call. For example,\ \>", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\ 2 + 3, \ using \[Rule] Built\[Dash]in["\"]]\)], "Input"], Cell[BoxData[ \(5\)], "Output"] }, Open ]], Cell["or", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\ \[LeftAngleBracket]2 + 3, 3 + 4\[RightAngleBracket], \ using \[Rule] \[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"]\[RightAngleBracket]]\)], "Input"], Cell[BoxData[ \(\[LeftAngleBracket]5, 7\[RightAngleBracket]\)], "Output"] }, Open ]], Cell["\<\ If you want to see which Mathematica functions are accessible by \ Built\[Dash]in[\"Numbers\"] just evaluate\ \>", "Text"], Cell[BoxData[ \(Built\[Dash]in["\"]\)], "Input"], Cell["and you get the list of all functions in that bundle:", "Text"], Cell[BoxData[ \(\[Bullet]bui["Numbers", \[Bullet]range[], True, \[Bullet]flist[\[Bullet]lf[ "!", \[Trademark]Factorial = Factorial], \[Bullet]lf[ "^", \(\(^\)\(=\)\(^\)\)], \[Bullet]lf[ "*", \(\(*\)\(=\)\(*\)\)], \[Bullet]lf["-", \(- = -\)], \[Bullet]lf[ "+", \(+ = +\)], \[Bullet]lf[ "=", \(\(=\)\(=\)\(\[Equal]\)\)], \[Bullet]lf[ "<", \(\(<\)\(=\)\(<\)\)], \[Bullet]lf[ ">", \(\(>\)\(=\)\(>\)\)], \[Bullet]lf[ "()", \[Trademark]Binomial = Binomial], \[Bullet]lf[ ":=", \(\(:=\)\(=\)\(:=\)\)], \[Bullet]lf[ "inf", \[Trademark]Infimum = Infimum], \[Bullet]lf[ "IsInteger", \[Trademark]IsInteger = IsInteger], \[Bullet]lf[ "IsNatural", \[Trademark]IsNatural = IsNatural], \[Bullet]lf[ "IsPrime", \[Trademark]IsPrime = IsPrime], \[Bullet]lf[ "IsRational", \[Trademark]IsRational = IsRational], \[Bullet]lf[ "max", \[Trademark]Maximum = Maximum], \[Bullet]lf[ "min", \[Trademark]Minimum = Minimum], \[Bullet]lf[ "sup", \[Trademark]Supremum = Supremum], \[Bullet]lf[ "SuperMinus", \[Trademark]SuperMinus = SuperMinus], \[Bullet]lf[ "SuperPlus", \[Trademark]SuperPlus = SuperPlus], \[Bullet]lf[ "\[LeftBracketingBar]\[RightBracketingBar]", \ \[Trademark]BracketingBar = BracketingBar], \[Bullet]lf[ "\[Sqrt]", \[Sqrt] = \[Sqrt]], \[Bullet]lf[ "\[Divide]", \(\(/\)\(=\)\(/\)\)], \[Bullet]lf[ "\[GreaterEqual]", \ \(\(\[GreaterEqual]\)\(=\)\(\[GreaterEqual]\)\)], \[Bullet]lf[ "\[LessEqual]", \(\(\[LessEqual]\)\(=\)\(\[LessEqual]\)\)], \ \[Bullet]lf[ "\[VerticalBar]", \ \(\(\[VerticalBar]\)\(=\)\(\[VerticalBar]\)\)]]]\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell["Definition", "Subsection", InitializationCell->True], Cell[TextData[{ "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 \[Epsilon] \ which refers to a ", StyleBox["Theorema", FontSlant->"Italic"], " built\[Dash]in function 'is\[Dash]rational' that decides whether or not a \ Mathematica expression denotes a rational number with enumerator and \ denominator in decimal representation." }], "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[]\), ",", "\[IndentingNewLine]", RowBox[{\(rational\[Dash]numbers\[Dash]field[]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\(\[IndentingNewLine]\)\(\[Epsilon]\+N[ x] \[DoubleLeftRightArrow] is\[Dash]rational[x]\)\)}, {\(0\+N = 0\)}, {\(1\+N = 1\)}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {\(inverse\+N[x] = 1/x\)}, {\(x\(/\+N\)y = x/y\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]}], "]"}]], "Input", InitializationCell->True, CellTags->"Definition (rational numbers field)"] }, Open ]], Cell[CellGroupData[{ Cell["Examples", "Subsection"], Cell[CellGroupData[{ Cell["Theory", "Subsubsection"], Cell[BoxData[ \(Definition["\<\[DoubleStruckCapitalQ]0\>", \[DoubleStruckCapitalQ]0 = rational\[Dash]numbers\[Dash]field[]]\)], "Input", CellTags->"Definition (\[DoubleStruckCapitalQ]0)"], Cell["\<\ Note that the constant denoting the result of applying the functor 'rational\ \[Dash]numbers\[Dash]field' is, of course, completely arbitrary. Whe chose \ here the constant '\[DoubleStruckCapitalQ]0' instead of the usual '\ \[DoubleStruckCapitalQ]' because we want to emphasize that \ \[DoubleStruckCapitalQ]0 denotes the domain of rationals equipped with only \ the field opertaions.\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Theory", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\<\[DoubleStruckCapitalQ]0\>"]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Theory (T)"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"] }, Open ]], Cell[CellGroupData[{ Cell["Field Operations", "Subsubsection"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalQ]0[2.0005]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalQ]0[2/5]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[0\+\[DoubleStruckCapitalQ]0]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[1\+\[DoubleStruckCapitalQ]0]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[5/2\( + \+\[DoubleStruckCapitalQ]0\)3]\)], "Input"], Cell[BoxData[ \(11\/2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-\+\[DoubleStruckCapitalQ]0\(-2\)\)/3]\)], "Input"], Cell[BoxData[ \(2\/3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[3\( - \+\[DoubleStruckCapitalQ]0\)\(-2\)/3]\)], "Input"], Cell[BoxData[ \(11\/3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[5\(*\+\[DoubleStruckCapitalQ]0\)3/4]\)], "Input"], Cell[BoxData[ \(15\/4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[inverse\+\[DoubleStruckCapitalQ]0[3/4]]\)], "Input"], Cell[BoxData[ \(4\/3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(7/ 5\)\(/\+\[DoubleStruckCapitalQ]0\)\((\(-2\)/3)\)]\)], "Input"], Cell[BoxData[ \(\(-21\)\/10\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(7/5\)\(/\+\[DoubleStruckCapitalQ]\)\((\(-2\)/3)\)]\)], "Input"], Cell[BoxData[ \(\(7\/5\)\(/\+\[DoubleStruckCapitalQ]\)\((\(-2\)\/3)\)\)], "Output"] }, Open ]] }, Open ]] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Domains Modulo a Prime as Fields", "Section"], Cell[CellGroupData[{ Cell["Definitions", "Subsection", InitializationCell->True], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[p]\), ",", "\[IndentingNewLine]", RowBox[{\(prime\[Dash]field[p]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ { RowBox[{"\[IndentingNewLine]", RowBox[{\(\(\[Epsilon]\+N[ x]\)\(\[DoubleLeftRightArrow]\)\), "\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(is\[Dash]integer[x]\)}, {\(0 \[LessEqual] x\)}, {\(x < p\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], " "}]}]}, {\(0\+N = 0\)}, {\(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]\)}, {\(inverse\+N[x] = pf\[Dash]inverse[x, p]\)}, {\(x\(/\+N\)y = pf\[Dash]quotient[x, y, p]\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]}], "]"}]], "Input", InitializationCell->True, CellTags->"Definition (prime field)"], Cell[TextData[{ "Remark on the operations in the functor: ", Cell[BoxData[ \(inverse\+N\)], InitializationCell->True], " and ", Cell[BoxData[ \(\(/\+N\)\)], InitializationCell->True], " refer to the function pf\[Dash]inverse and pf\[Dash]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 ", StyleBox["Theorema\".", FontSlant->"Italic"] }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Examples", "Subsection"], Cell[CellGroupData[{ Cell["Theory", "Subsubsection"], Cell[BoxData[ \(Definition["\<\[DoubleStruckCapitalF]5\>", \[DoubleStruckCapitalF]5 = prime\[Dash]field[5]]\)], "Input", CellTags->"Definition (\[DoubleStruckCapitalF]5)"], Cell[BoxData[ RowBox[{ StyleBox["Theory", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\<\[DoubleStruckCapitalF]5\>"]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Theory (T)"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"] }, Open ]], Cell[CellGroupData[{ Cell["Arithmetic", "Subsubsection"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalF]5[0]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalF]5[4]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalF]5[5]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalF]5[\(-1\)]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[0\+\[DoubleStruckCapitalF]5]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[1\+\[DoubleStruckCapitalF]5]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[4\( + \+\[DoubleStruckCapitalF]5\)1]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-\+\[DoubleStruckCapitalF]5\((2)\)\)]\)], "Input"], Cell[BoxData[ \(3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[1\( - \+\[DoubleStruckCapitalF]5\)\((2)\)]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[4\(*\+\[DoubleStruckCapitalF]5\)3]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[inverse\+\[DoubleStruckCapitalF]5[3]]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[4\(/\+\[DoubleStruckCapitalF]5\)3]\)], "Input"], Cell[BoxData[ \(3\)], "Output"] }, Open ]] }, Open ]] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Reduction Fields", "Section"], Cell[CellGroupData[{ Cell["Informal Explanation", "Subsection"], Cell["\<\ 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?\ \>", "Text"], Cell[TextData[{ "First of all note that in a field an element x\[NotEqual]0 can be reduced \ to 0 by any element y (\[NotEqual]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 \[NotEqual]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 ", StyleBox["not ", FontSlant->"Italic"], "Noetherian. Finally, we have to invent the appropriate lcrd: Given two \ rationals x and y, both \[NotEqual]0, any rational z\[NotEqual]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 \[NotEqual]0 as the lcrd[ \ x, y]. We choose lcrd[ x, y] := 1." }], "Text"], Cell["\<\ 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.\ \>", "Text"], Cell[TextData[{ StyleBox["For extending a domain by new operations, in principle, we have \ an extra language construct in ", "\.10\[CapitalAGrave]Z"], StyleBox["Theorema", FontSlant->"Italic"], ", 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 \[Epsilon] of the domain and all the operations of \ the old domain D to the new domain N by definitions of the form" }], "Text"], Cell[BoxData[ \(x\( + \+N\)y = x\( + \+D\)y\)], "Input"], Cell["\<\ and then we define the new operations in N in terms of the known operations \ in D. \ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Definition", "Subsection", InitializationCell->True], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[D]\), ",", "\[IndentingNewLine]", RowBox[{\(reduction\[Dash]field[D]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\(\[IndentingNewLine]\)\(\[Epsilon]\+N[ x] \[DoubleLeftRightArrow] \[Epsilon]\+D[ x]\)\)}, {\(0\+N = 0\+D\)}, {\(1\+N = 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 \[DoubleLeftRightArrow] \((\((x \ \[NotEqual] 0\+D)\) \[And] \((y = 0\+D)\))\)\)\(\[IndentingNewLine]\) \)}, { RowBox[{\(rdm\+N[x, y]\), " ", \( (*\ the\ reduction\ multiplier\ of\ x\ modulo\ y\ \ \ *) \), " ", "=", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(x\(/\+D\)y\), "\[DoubleLeftArrow]", \(x \[NotEqual] 0\+D \[And] y \[NotEqual] 0\+D\)}, {\(0\+D\), "\[DoubleLeftArrow]", "otherwise"} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], " "}]}, { RowBox[{\(lcrd\+N[x, y]\), " ", \( (*\ the\ least\ common\ reducible\ of\ x\ and\ y\ \ \ *) \), " ", "=", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(1\+D\), "\[DoubleLeftArrow]", \(x \[NotEqual] 0\+D \[And] y \[NotEqual] 0\+D\)}, {\(0\+D\), "\[DoubleLeftArrow]", "otherwise"} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}]}]} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\n", "\t", "]"}]}]}], "]"}]], "Input", InitializationCell->True, CellTags->"Definition (reduction field)"], Cell[TextData[{ "Remarks on the operations in the functor: ", Cell[BoxData[ \(rdm\+N\)], InitializationCell->True], " is defined for all field elements x and y. For the inputs x and y for \ which no reduction is possible ", Cell[BoxData[ \(rdm\+N\)], InitializationCell->True], "[ x, y] is defined to be zero. By this, it is guaranteed that x is \ reducible modulo y iff x - ", Cell[BoxData[ \(rdm\+N\)], InitializationCell->True], "[ x, y] * y ", Cell[BoxData[ \(TraditionalForm\`\( < \+N\)\)]], " x. Similarly, ", Cell[BoxData[ \(lcrd\+N[x, y]\)], InitializationCell->True], " is defined for all field elements x and y." }], "Text", InitializationCell->True] }, Open ]], Cell[CellGroupData[{ Cell["Examples", "Subsection"], Cell[CellGroupData[{ Cell["Theory", "Subsubsection"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(\[DoubleStruckCapitalQ]0 = rational\[Dash]numbers\[Dash]field[]\)}, {\(\[DoubleStruckCapitalQ]\[EmptyUpTriangle] = reduction\[Dash]field[\[DoubleStruckCapitalQ]0]\)}, {\(\[DoubleStruckCapitalF]5 = prime\[Dash]field[5]\)}, {\(\[DoubleStruckCapitalF]5\[EmptyUpTriangle] = reduction\[Dash]field[\[DoubleStruckCapitalF]5]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Definition (Domains)"], Cell["\<\ Again, the constant denoting the result of applying the functor rdrat is, of \ course, completely arbitrary. We chose here the constant '\ \[DoubleStruckCapitalQ]\[EmptyUpTriangle]' instead of the usual '\ \[DoubleStruckCapitalQ]' because we want to emphasize that \ \[DoubleStruckCapitalQ]\[EmptyUpTriangle] denotes the domain of rationals \ viewed as a reduction ring and not the ordinary domain of rationals viewed as \ a field.\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Theory", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\"]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Theory (T)"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"] }, Open ]], Cell[CellGroupData[{ Cell["Ring Operations", "Subsubsection"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalQ]0[2.0005]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle][ 2.0005]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle][ 2/3]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalF]5[6]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle][ 4]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[0\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[0\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[1\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[1\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5/2\( + \+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(11\/2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 4\( + \+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\(-2\)\)/ 3]\)], "Input"], Cell[BoxData[ \(2\/3\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5/2\( - \+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(\(-1\)\/2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 2\( - \+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5\(*\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)3/4]\)], "Input"], Cell[BoxData[ \(15\/4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[4\(*\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]\)4]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5\(/\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)\(3/4\)]\)], "Input"], Cell[BoxData[ \(5\(/\+\(reduction\[Dash]field[ rational\[Dash]numbers\[Dash]field[]]\)\)\(3\/4\)\)], "Output"] }, Open ]], Cell["\<\ The operation / is not any more available in the reduction ring \ \[DoubleStruckCapitalQ]\[EmptyUpTriangle] !\ \>", "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[3\(/\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]\)2]\)], "Input"], Cell[BoxData[ \(3\(/\+\(reduction\[Dash]field[prime\[Dash]field[5]]\)\)2\)], "Output"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Additional Operations", "Subsubsection"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5/2\( > \+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5/2\( > \+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)0]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 0\( > \+\[DoubleStruckCapitalQ]\[EmptyUpTriangle]\)0]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 4\( > \+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 4\( > \+\[DoubleStruckCapitalF]5\[EmptyUpTriangle]\)0]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle][3, 2]]\)], "Input"], Cell[BoxData[ \(3\/2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle][3, 2]]\)], "Input"], Cell[BoxData[ \(4\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle][0, 2]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle][3, 0]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalQ]\[EmptyUpTriangle][3, 2]]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle][3, 2]]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalF]5\[EmptyUpTriangle][3, 0]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]] }, Open ]] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["The Integers Viewed as a Reduction Ring", "Section"], Cell[CellGroupData[{ Cell["Informal Explanation", "Subsection"], Cell["\<\ 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.\ \>", "Text"], Cell["\<\ 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.\ \>", "Text"], Cell["\<\ Now it is clear that, for positive x and y, rdm[ x, y] can be chosen 1 if \ \[LeftBracketingBar]x\[RightBracketingBar] \[GreaterEqual] \ \[LeftBracketingBar]y\[RightBracketingBar] . 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[ \ \[LeftBracketingBar]x\[RightBracketingBar], \[LeftBracketingBar]y\ \[RightBracketingBar]].\ \>", "Text"], Cell["\<\ lcrd[ x, y] for positive integers is just the maximum of x and y.\ \>", "Text"], Cell["\<\ 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.)\ \>", "Text"], Cell["\<\ 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.\ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Definition", "Subsection", InitializationCell->True], Cell[CellGroupData[{ Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[]\), ",", "\[IndentingNewLine]", RowBox[{\(reduction\[Dash]integers[]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\[Epsilon]\+N[x] \[DoubleLeftRightArrow] is\[Dash]integer[x]\)}, {\(0\+N = 0\)}, {\(1\+N = 1\)}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {\(\(x\( > \+N\)y \[DoubleLeftRightArrow] \ \[LeftBracketingBar]x\[RightBracketingBar] > \[LeftBracketingBar]y\ \[RightBracketingBar]\)\(\[IndentingNewLine]\) \)}, {\(\(rdm\+N[x, y]\ \ (*\ a\ reduction\ multiplier\ of\ x\ modulo\ y\ \ \ *) \ = sign[x] sign[\ y] rdmp[\[LeftBracketingBar]x\[RightBracketingBar],\ \[LeftBracketingBar]y\[RightBracketingBar]]\)\(\[IndentingNewLine]\) \(\ \)\)}, { RowBox[{\(rdmp[x, y]\), " ", \( (*\ a\ reduction\ multiplier\ for\ non - negative\ x\ modulo\ non - negative\ y\ \ *) \), " ", "=", "\[IndentingNewLine]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {"1", "\[DoubleLeftArrow]", RowBox[{"\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(x \[GreaterEqual] y\)}, {\(y > 0\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], " "}]}, {"0", "\[DoubleLeftArrow]", "otherwise"} }, ColumnAlignments->{Left}], "\[IndentingNewLine]", StyleBox["}", ShowContents->False]}], " "}]}, {\(\(lcrd\+N[x, y]\)\(\ \)\( (*\ the\ least\ common\ reducible\ of\ x\ and\ y\ \ \ *) \)\(\ \)\(=\)\(maximum[\[LeftBracketingBar]x\[RightBracketingBar], \ \[LeftBracketingBar]y\[RightBracketingBar]]\)\(\ \)\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\[IndentingNewLine]", "\n", "\t", "]"}]}]}], "]"}]], "Input", InitializationCell->True, CellTags->"Definition (reduction integers)"], Cell[BoxData[ \(General::"spell1" \(\(:\)\(\ \)\) "Possible spelling error: new symbol name \"\!\(rdmp\)\" is similar to \ existing symbol \"\!\(rdm\)\"."\)], "Message"] }, Open ]], Cell["Some remarks on the operations in this functor:", "Text", InitializationCell->True], Cell[TextData[{ "Note that the functions rdmp and ", Cell[BoxData[ \(lrd\)], InitializationCell->True], " are ", StyleBox["not", FontSlant->"Italic"], " one of the three additional operations necessary in reduction rings but \ they are just auxiliary functions on the way to defining ", Cell[BoxData[ \(TraditionalForm\`rdm\+N\)]], " and ", Cell[BoxData[ \(lcrd\+N\)], InitializationCell->True], ". The auxiliary functions do not carry the underscript N and, hence, are \ not available outside the functor!" }], "Text"], Cell["\<\ Now we define a slightly more restricted but more efficient version of this \ functor:\ \>", "Text"], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", " ", ",", \(any[]\), ",", "\[IndentingNewLine]", RowBox[{\(reduction\[Dash]integers\[Dash]by\[Dash]quotient[]\), "=", RowBox[{"Functor", "[", RowBox[{"N", ",", \(any[x, y]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ {\(\[Epsilon]\+N[x] \[DoubleLeftRightArrow] is\[Dash]integer[x]\)}, {\(0\+N = 0\)}, {\(1\+N = 1\)}, {\(x\( + \+N\)y = x + y\)}, {\(\(-\+N x\) = \(-x\)\)}, {\(x\( - \+N\)y = x - y\)}, {\(x\(*\+N\)y = x*y\)}, {\(\(x\( > \+N\)y \[DoubleLeftRightArrow] \ \[LeftBracketingBar]x\[RightBracketingBar] > \[LeftBracketingBar]y\ \[RightBracketingBar]\)\(\[IndentingNewLine]\) \)}, {\(\(rdm\+N[x, y]\ \ (*\ a\ reduction\ multiplier\ of\ x\ modulo\ y\ \ \ *) \ = sign[x] sign[\ y] rdmp[\[LeftBracketingBar]x\[RightBracketingBar],\ \[LeftBracketingBar]y\[RightBracketingBar]]\)\(\[IndentingNewLine]\) \(\ \)\)}, { RowBox[{\(rdmp[x, y]\), " ", \( (*\ a\ reduction\ multiplier\ for\ non - negative\ x\ modulo\ non - negative\ y\ \ *) \), " ", "=", "\[IndentingNewLine]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(quotient[x, y]\), "\[DoubleLeftArrow]", RowBox[{"\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(x \[GreaterEqual] y\)}, {\(y > 0\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], " "}]}, {"0", "\[DoubleLeftArrow]", "otherwise"} }, ColumnAlignments->{Left}], "\[IndentingNewLine]", StyleBox["}", ShowContents->False]}], " "}]}, {\(\(lcrd\+N[x, y]\)\(\ \)\( (*\ the\ least\ common\ reducible\ of\ x\ and\ y\ \ \ *) \)\(\ \)\(=\)\(maximum[\[LeftBracketingBar]x\[RightBracketingBar], \ \[LeftBracketingBar]y\[RightBracketingBar]]\)\(\ \)\)} }, ColumnAlignments->{Left}]} }, ColumnAlignments->{Left}, RowLines->0.75]}], "\[IndentingNewLine]", "\n", "\t", "]"}]}]}], "]"}]], "Input", InitializationCell->True, CellTags->"Definition (reduction integers by quotient)"] }, Open ]], Cell[CellGroupData[{ Cell["Examples", "Subsection"], Cell[CellGroupData[{ Cell["Theory", "Subsubsection"], Cell[BoxData[ \(Definition["\<\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\>", \ \[DoubleStruckCapitalZ]\[EmptyUpTriangle] = reduction\[Dash]integers[]]\)], "Input", CellTags->"Definition (\[DoubleStruckCapitalZ]\[EmptyUpTriangle])"], Cell[BoxData[ RowBox[{ StyleBox["Theory", FontWeight->"Bold"], "[", RowBox[{"\"\\"", ",", "\[IndentingNewLine]", GridBox[{ {\(Definition["\"]\)}, {\(Definition["\"]\)}, {\(Definition["\<\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\>"]\)} }, ColumnAlignments->{Left}]}], "]"}]], "Input", CellTags->"Theory (T)"], Cell[BoxData[ \(Use[\[LeftAngleBracket]Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Built\[Dash]in["\"], Theory["\"]\[RightAngleBracket]]\)], "Input"] }, Open ]], Cell[CellGroupData[{ Cell["Arithmetic", "Subsubsection"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][ 2]]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][ 2.5]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\[Epsilon]\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][ 2/5]]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[0\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[1\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5\( + \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(8\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\(-2\)\)]\)], \ "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 5\( - \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(2\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[5\(*\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(15\)], "Output"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Additional Operations", "Subsubsection"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 4\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 3\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)3]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 3\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)\(-3\)]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-3\)\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)3]\)], \ "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-3\) = 3]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[TextData[{ "Hence, 3 and -3 are incomparable w.r.t. ", Cell[BoxData[ \(\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)\)]], "." }], "Text"], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[\(-3\)\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)2]\)], \ "Input"], Cell[BoxData[ \(True\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ 2\( > \+\[DoubleStruckCapitalZ]\[EmptyUpTriangle]\)\(-3\)]\)], "Input"], Cell[BoxData[ \(False\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][3, 3]]\)], "Input"], Cell[BoxData[ \(1\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][3, 4]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][3, \(-4\)]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][\(-3\), 4]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][\(-3\), \(-4\)]]\)], \ "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][2, 4]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ rdm\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][2, \(-4\)]]\)], "Input"], Cell[BoxData[ \(0\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][5, 5]]\)], "Input"], Cell[BoxData[ \(5\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][6, 6]]\)], "Input"], Cell[BoxData[ \(6\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][6, 5]]\)], "Input"], Cell[BoxData[ \(6\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][5, \(-6\)]]\)], "Input"], Cell[BoxData[ \(6\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][\(-5\), 6]]\)], "Input"], Cell[BoxData[ \(6\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][\(-5\), \(-6\)]]\)], \ "Input"], Cell[BoxData[ \(6\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][\(-10\), \(-10\)]]\)], \ "Input"], Cell[BoxData[ \(10\)], "Output"] }, Open ]], Cell[CellGroupData[{ Cell[BoxData[ \(Compute[ lcrd\+\[DoubleStruckCapitalZ]\[EmptyUpTriangle][\(-10\), 5]]\)], "Input"], Cell[BoxData[ \(10\)], "Output"] }, Open ]] }, Open ]] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["\<\ Division Semigroup in Tuples Representation with Lexical Ordering\ \>", "Section"], Cell[CellGroupData[{ Cell["Informal Explanation", "Subsection"], Cell["\<\ 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.\ \>", "Text"], Cell["\<\ 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\".\ \>", "Text", InitializationCell->True], Cell[TextData[{ "We use here a special representation of power products, which is very \ common in computer algebra: ", Cell[BoxData[ \(TraditionalForm\`\(x\_1\^i\_1 ... \) x\_n\^i\_n\)]], "is represented by the tuple of exponents ", Cell[BoxData[ \(TraditionalForm\`\[LeftAngleBracket]\(i\_\[AliasDelimiter]\), ... , i\_n\)]], "\[RightAngleBracket]. 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!" }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Definitions", "Subsection", InitializationCell->True], Cell[BoxData[ RowBox[{ StyleBox["Definition", FontWeight->"Bold"], "[", RowBox[{ "\"\\"", ",", \(any[k, D]\), ",", "\[IndentingNewLine]", RowBox[{\(tuples\[Dash]division\[Dash]semigroup\[Dash]lexical[k]\), " ", \( (*\ the\ division\ semigroup\ in\ tuples\ representation\ of\ length\ \ k\ \ with\ lexicographic\ ordering\ *) \), "=", "\[IndentingNewLine]", RowBox[{"Functor", "[", RowBox[{ "N", ",", \(any[m, m\&_, n, n\&_, x, y, i]\), ",", "\n", "\t", GridBox[{ {\(\[DoubleStruckS] = \[LeftAngleBracket]\ \[RightAngleBracket]\)}, {GridBox[{ { RowBox[{\(\(\[Epsilon]\+N[ x]\)\(\[DoubleLeftRightArrow]\)\), "\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(is\[Dash]tuple[x]\)}, {\(\[LeftBracketingBar]x\ \[RightBracketingBar] = k\)}, { RowBox[{\(\[ForAll] \+\(i = 1, \[Ellipsis], k\)\), RowBox[{"\[And]", RowBox[{ StyleBox["{", SpanMaxSize->Infinity], GridBox[{ {\(is\[Dash]integer[x\_i]\)}, {\(x\_i \[GreaterEqual] 0\)} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], " "}]}]} }, ColumnAlignments->{Left}], StyleBox["}", ShowContents->False]}], " "}]}, {\(1\+N = \[LeftAngleBracket]\(0\)\( \ \[VerticalSeparator] \+\(i = 1, \[Ellipsis], k\)\)\[RightAngleBracket]\)}, {\(x\(*\+N\)y = \[LeftAngleBracket]\(x\_i + y\_i\)\( \[VerticalSeparator] \+\(i = 1, \[Ellipsis], k\)\)\[RightAngleBracket]\)}, {\(x\(/\+N\)y = \[LeftAngleBracket]\(x\_i -