|
#############################################################################
##
## This file is part of GAP, a system for computational discrete algebra.
## This file's authors include Frank Celler.
##
## Copyright of GAP belongs to its developers, whose names are too numerous
## to list here. Please refer to the COPYRIGHT file for details.
##
## SPDX-License-Identifier: GPL-2.0-or-later
##
## This file contains the operations for rewriting systems. Any
## implementation of a rewriting system must at least implement methods for
## <P/>
## constructing such a rewriting system,
## <C>CopyRws</C>,
## <C>IsConfluent</C>,
## <C>ReducedForm</C>, and
## <C>Rules</C>.
## <P/>
## An implementation might also want to implement <C>MakeConfluent</C> and/or
## <C>ConfluentRws</C>.
## <P/>
## The generic methods, which are defined in <F>rws.gi</F>, for
## <P/>
## <C>ReducedAdditiveInverse</C>,
## <C>ReducedComm</C>,
## <C>ReducedConjugate</C>,
## <C>ReducedDifference</C>
## <C>ReducedInverse</C>,
## <C>ReducedLeftQuotient</C>,
## <C>ReducedOne</C>,
## <C>ReducedPower</C>,
## <C>ReducedProduct</C>
## <C>ReducedScalarProduct</C>,
## <C>ReducedSum</C>, and
## <C>ReducedZero</C>,
## <P/>
## use <C>ReducedForm</C>. Depending on the underlying structure not all of them
## will work. For example, for a monoid <C>ReducedInverse</C> will produce an
## error because the generic methods tries to reduced the inverse of the
## given element.
## <P/>
## As in general a rewriting system will be first built and then used
## without changing it, some functions (e.g. <C>GroupByRws</C>) call
## <C>ReduceRules</C> to give the rewriting system a chance to optimise itself.
## The default method for <C>ReduceRules</C> is <Q>do nothing</Q>.
## <P/>
## The underlying structure is stored in the attribute <C>UnderlyingFamily</C>
## and the generators used for the rewriting system in the attribute
## <C>GeneratorsOfRws</C>. The number of rws generators is stored in the
## attribute <C>NumberGeneratorsOfRws</C>.
## <P/>
## The family of a rewriting system also contains the underlying family, the
## default method for <C>UnderlyingFamily</C> uses the family to get the
## underlying family for a given rewriting system.
##
## <#GAPDoc Label="[2]{rws}">
## The key point to note about rewriting systems is that they have
## properties such as
## <Ref Prop="IsConfluent" Label="for a rewriting system"/>
## and attributes such as <Ref Attr="Rules"/>, however
## they are rarely stored, but rather computed afresh each time they
## are asked for, from data stored in the private members of the rewriting
## system object. This is because a rewriting system often evolves
## through a session, starting with some rules which define the
## algebra <A>A</A> as relations, and then adding more rules to make
## the system confluent.
## For example, in the case of Knuth-Bendix rewriting systems (see
## Chapter <Ref Chap="Finitely Presented Semigroups and Monoids"/>),
## the function <C>CreateKnuthBendixRewritingSystem</C> creating the
## rewriting system (in the file <F>lib/kbsemi.gi</F>) uses
## <P/>
## <Log><![CDATA[
## kbrws := Objectify(NewType(rwsfam,
## IsMutable and IsKnuthBendixRewritingSystem and
## IsKnuthBendixRewritingSystemRep),
## rec(family:= fam,
## reduced:=false,
## tzrules:=List(relwco,i->
## [LetterRepAssocWord(i[1]),LetterRepAssocWord(i[2])]),
## pairs2check:=CantorList(Length(r)),
## ordering:=wordord,
## freefam:=freefam));
## ]]></Log>
## <P/>
## In particular, since we don't use the filter
## <C>IsAttributeStoringRep</C>
## in the <Ref Func="Objectify"/>,
## whenever <Ref Prop="IsConfluent" Label="for a rewriting system"/> is
## called,
## the appropriate method to determine confluence is called.
## <#/GAPDoc>
##
#############################################################################
##
#C IsRewritingSystem( <obj> )
##
## <#GAPDoc Label="IsRewritingSystem">
## <ManSection>
## <Filt Name="IsRewritingSystem" Arg='obj' Type='Category'/>
##
## <Description>
## This is the category in which all rewriting systems lie.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareCategory(
"IsRewritingSystem",
IsCopyable );
#############################################################################
##
#C IsReducedConfluentRewritingSystem( <obj> )
##
## <ManSection>
## <Filt Name="IsReducedConfluentRewritingSystem" Arg='obj' Type='Category'/>
##
## <Description>
## This is a subcategory of <Ref Func="IsRewritingSystem"/> for (immutable)
## rws which are reduced and confluent.
## </Description>
## </ManSection>
##
DeclareCategory(
"IsReducedConfluentRewritingSystem",
IsRewritingSystem);
#############################################################################
##
#P IsBuiltFromAdditiveMagmaWithInverses( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromAdditiveMagmaWithInverses" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty(
"IsBuiltFromAdditiveMagmaWithInverses",
IsObject );
#############################################################################
##
#P IsBuiltFromMagma( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromMagma" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty(
"IsBuiltFromMagma",
IsObject );
#############################################################################
##
#P IsBuiltFromMagmaWithOne( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromMagmaWithOne" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty(
"IsBuiltFromMagmaWithOne",
IsObject );
#############################################################################
##
#P IsBuiltFromMagmaWithInverses( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromMagmaWithInverses" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty(
"IsBuiltFromMagmaWithInverses",
IsObject );
#############################################################################
##
#P IsBuiltFromGroup( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromGroup" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty(
"IsBuiltFromGroup",
IsObject );
#############################################################################
##
#M IsBuiltFromMagma( <obj> )
##
InstallTrueMethod( IsBuiltFromMagma, IsBuiltFromMagmaWithOne );
#############################################################################
##
#M IsBuiltFromMagmaWithOne( <obj> )
##
InstallTrueMethod( IsBuiltFromMagmaWithOne, IsBuiltFromMagmaWithInverses );
#############################################################################
##
#P IsBuiltFromSemigroup( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromSemigroup" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty( "IsBuiltFromSemigroup", IsObject );
#############################################################################
##
#P IsBuiltFromMonoid( <obj> )
##
## <ManSection>
## <Prop Name="IsBuiltFromMonoid" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareProperty( "IsBuiltFromMonoid", IsObject );
#############################################################################
##
#M IsBuiltFromGroup( <obj> )
##
InstallTrueMethod( IsBuiltFromMagmaWithInverses, IsBuiltFromGroup );
#############################################################################
##
#A SemigroupOfRewritingSystem( <rws> )
#A MonoidOfRewritingSystem( <rws> )
##
## <#GAPDoc Label="SemigroupOfRewritingSystem">
## <ManSection>
## <Attr Name="SemigroupOfRewritingSystem" Arg='rws'/>
## <Attr Name="MonoidOfRewritingSystem" Arg='rws'/>
##
## <Description>
## returns the semigroup or monoid over which <A>rws</A> is
## a rewriting system.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareAttribute("SemigroupOfRewritingSystem",IsRewritingSystem);
DeclareAttribute("MonoidOfRewritingSystem",IsRewritingSystem);
#############################################################################
##
#O FreeStructureOfRewritingSystem( <obj> )
##
## <ManSection>
## <Oper Name="FreeStructureOfRewritingSystem" Arg='obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation( "FreeStructureOfRewritingSystem", [IsRewritingSystem]);
#############################################################################
##
#A ConfluentRws( <rws> )
##
## <#GAPDoc Label="ConfluentRws">
## <ManSection>
## <Attr Name="ConfluentRws" Arg='rws'/>
##
## <Description>
## Return a new rewriting system defining the same algebra as <A>rws</A>
## which is confluent.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
# NOTE: this is an attribute *but* rewriting system do not store this
# attribute because they are mutable.
##
DeclareAttribute(
"ConfluentRws",
IsRewritingSystem );
#############################################################################
##
#A GeneratorsOfRws( <rws> )
##
## <#GAPDoc Label="GeneratorsOfRws">
## <ManSection>
## <Attr Name="GeneratorsOfRws" Arg='rws'/>
##
## <Description>
## Returns the list of generators of the rewriting system <A>rws</A>.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareAttribute(
"GeneratorsOfRws",
IsRewritingSystem );
#############################################################################
##
#A NumberGeneratorsOfRws( <rws> )
##
## <ManSection>
## <Attr Name="NumberGeneratorsOfRws" Arg='rws'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareAttribute(
"NumberGeneratorsOfRws",
IsRewritingSystem );
#############################################################################
##
#A Rules( <rws> )
##
## <#GAPDoc Label="Rules">
## <ManSection>
## <Attr Name="Rules" Arg='rws'/>
##
## <Description>
## The rules comprising the rewriting system. Note that these may
## change through the life of the rewriting system, however they
## will always be a set of defining relations of the algebra
## described by the rewriting system.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
## NOTE: this is an attribute *but*, normally, rewriting system
## do not store this attribute.
##
DeclareAttribute(
"Rules",
IsRewritingSystem );
#############################################################################
##
#a UnderlyingFamily( <rws> )
##
#T DeclareAttribute(
#T "UnderlyingFamily",
#T IsObject );
#T already in `liefam.gd'
#############################################################################
##
#A OrderOfRewritingSystem(<rws>)
#A OrderingOfRewritingSystem(<rws>)
##
## <#GAPDoc Label="OrderOfRewritingSystem">
## <ManSection>
## <Attr Name="OrderOfRewritingSystem" Arg='rws'/>
## <Attr Name="OrderingOfRewritingSystem" Arg='rws'/>
##
## <Description>
## return the ordering of the rewriting system <A>rws</A>.
## <!-- %the synonym here guarantees compatibility with &GAP; 4.1 and &GAP; 4.2. -->
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareAttribute("OrderingOfRewritingSystem", IsRewritingSystem);
DeclareSynonym("OrderOfRewritingSystem", OrderingOfRewritingSystem);
#############################################################################
##
#P IsConfluent( <rws> )
#P IsConfluent( <A> )
##
## <#GAPDoc Label="IsConfluent">
## <ManSection>
## <Heading>IsConfluent</Heading>
## <Prop Name="IsConfluent" Arg='rws' Label="for a rewriting system"/>
## <Prop Name="IsConfluent" Arg='A'
## Label="for an algebra with canonical rewriting system"/>
##
## <Description>
## For a rewriting system <A>rws</A>,
## <Ref Prop="IsConfluent" Label="for a rewriting system"/> returns
## <K>true</K> if and only if <A>rws</A> is confluent.
## A rewriting system is <E>confluent</E> if, for every two words
## <M>u</M> and <M>v</M> in the free algebra <M>T</M> which represent the
## same element of the algebra <M>A</M> defined by <A>rws</A>,
## <C>ReducedForm( <A>rws</A>, </C><M>u</M> <C>) =
## ReducedForm( <A>rws</A>, </C><M>v</M><C>)</C> as words in the
## free algebra <M>T</M>.
## This element is the <E>unique normal form</E>
## of the element represented by <M>u</M>.
## <P/>
## For an algebra <A>A</A> with a canonical rewriting system associated
## with it,
## <Ref Prop="IsConfluent" Label="for an algebra with canonical rewriting system"/>
## checks whether that rewriting system is confluent.
## <P/>
## Also see <Ref Prop="IsConfluent" Label="for pc groups"/>.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
# NOTE: this is a property *but* the rewriting system does not store this
# attribute.
##
DeclareProperty(
"IsConfluent",
IsRewritingSystem );
#############################################################################
##
#P IsReduced( <rws> )
##
## <#GAPDoc Label="IsReduced">
## <ManSection>
## <Prop Name="IsReduced" Arg='rws'/>
##
## <Description>
## A rewriting system is reduced if for each rule <M>(l, r)</M>,
## <M>l</M> and <M>r</M> are both reduced.
## <P/>
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareProperty( "IsReduced", IsRewritingSystem and IsMutable );
#############################################################################
##
#O AddRule(<rws>, <rule>)
##
## <#GAPDoc Label="AddRule">
## <ManSection>
## <Oper Name="AddRule" Arg='rws, rule'/>
##
## <Description>
## Add <A>rule</A> to a rewriting system <A>rws</A>.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareOperation(
"AddRule",
[ IsRewritingSystem and IsMutable , IsHomogeneousList ] );
#############################################################################
##
#O AddRuleReduced(<rws>, <rule>)
##
## <#GAPDoc Label="AddRuleReduced">
## <ManSection>
## <Oper Name="AddRuleReduced" Arg='rws, rule'/>
##
## <Description>
## Add <A>rule</A> to rewriting system <A>rws</A>.
## Performs a reduction operation on the resulting system,
## so that if <A>rws</A> is reduced it will remain reduced.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareOperation(
"AddRuleReduced",
[ IsRewritingSystem and IsMutable , IsHomogeneousList ] );
#############################################################################
##
#O AddGenerators( <rws>, <gens> )
##
## <ManSection>
## <Oper Name="AddGenerators" Arg='rws, gens'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"AddGenerators",
[ IsRewritingSystem and IsMutable, IsHomogeneousList ] );
#############################################################################
##
#O MakeConfluent( <rws> )
##
## <#GAPDoc Label="MakeConfluent">
## <ManSection>
## <Oper Name="MakeConfluent" Arg='rws'/>
##
## <Description>
## Add rules (and perhaps reduce) in order to make <A>rws</A> confluent
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareOperation(
"MakeConfluent",
[ IsRewritingSystem and IsMutable ] );
#############################################################################
##
#O ReduceRules( <rws> )
##
## <#GAPDoc Label="ReduceRules">
## <ManSection>
## <Oper Name="ReduceRules" Arg='rws'/>
##
## <Description>
## Reduce rules and remove redundant rules to make <A>rws</A> reduced.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareOperation(
"ReduceRules",
[ IsRewritingSystem and IsMutable ] );
#############################################################################
##
#O ReducedAdditiveInverse( <rws>, <obj> )
##
## <ManSection>
## <Oper Name="ReducedAdditiveInverse" Arg='rws, obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedAdditiveInverse",
[ IsRewritingSystem,
IsAdditiveElement ] );
#############################################################################
##
#O ReducedComm( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedComm" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedComm",
[ IsRewritingSystem,
IsMultiplicativeElement,
IsMultiplicativeElement ] );
#############################################################################
##
#O ReducedConjugate( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedConjugate" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedConjugate",
[ IsRewritingSystem,
IsMultiplicativeElement,
IsMultiplicativeElement ] );
#############################################################################
##
#O ReducedDifference( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedDifference" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedDifference",
[ IsRewritingSystem,
IsAdditiveElement,
IsAdditiveElement ] );
#############################################################################
##
#O ReducedForm( <rws>, <u> )
##
## <#GAPDoc Label="ReducedForm">
## <ManSection>
## <Oper Name="ReducedForm" Arg='rws, u'/>
##
## <Description>
## Given an element <A>u</A> in the free (or term) algebra <M>T</M> over
## which <A>rws</A> is defined,
## rewrite <A>u</A> by successive applications of the
## rules of <A>rws</A> until no further rewriting is possible, and return
## the resulting element of <M>T</M>.
## </Description>
## </ManSection>
## <#/GAPDoc>
##
DeclareOperation(
"ReducedForm",
[ IsRewritingSystem,
IsObject ] );
#############################################################################
##
#O IsReducedForm( <rws>, <u> )
##
## <ManSection>
## <Oper Name="IsReducedForm" Arg='rws, u'/>
##
## <Description>
## Given an element <A>u</A> in the free (or term) algebra over which
## <A>rws</A> is defined,
## returns <C><A>u</A> = ReducedForm(<A>rws</A>, <A>u</A>)</C>.
## </Description>
## </ManSection>
##
DeclareOperation(
"IsReducedForm",
[ IsRewritingSystem,
IsObject ] );
#############################################################################
##
#O ReducedInverse( <rws>, <obj> )
##
## <ManSection>
## <Oper Name="ReducedInverse" Arg='rws, obj'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedInverse",
[ IsRewritingSystem,
IsMultiplicativeElement ] );
#############################################################################
##
#O ReducedLeftQuotient( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedLeftQuotient" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedLeftQuotient",
[ IsRewritingSystem,
IsMultiplicativeElement,
IsMultiplicativeElement ] );
#############################################################################
##
#O ReducedOne( <rws> )
##
## <ManSection>
## <Oper Name="ReducedOne" Arg='rws'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedOne",
[ IsRewritingSystem ] );
#############################################################################
##
#O ReducedPower( <rws>, <obj>, <pow> )
##
## <ManSection>
## <Oper Name="ReducedPower" Arg='rws, obj, pow'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedPower",
[ IsRewritingSystem,
IsMultiplicativeElement,
IsInt ] );
#############################################################################
##
#O ReducedProduct( <rws>, <u>, <v> )
##
## <ManSection>
## <Oper Name="ReducedProduct" Arg='rws, u, v'/>
##
## <Description>
## The result is <M>w</M> where <M>[w]</M> equals [<A>u</A>][<A>v</A>] in
## <M>A</M> and <M>w</M> is in reduced form.
## <P/>
## The remaining operations are defined similarly when they
## are defined (as determined by the signature of the term algebra).
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedProduct",
[ IsRewritingSystem,
IsMultiplicativeElement,
IsMultiplicativeElement ] );
#############################################################################
##
#O ReducedQuotient( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedQuotient" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedQuotient",
[ IsRewritingSystem,
IsMultiplicativeElement,
IsMultiplicativeElement ] );
#############################################################################
##
#O ReducedScalarProduct( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedScalarProduct" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedScalarProduct",
[ IsRewritingSystem,
IsScalar,
IsAdditiveElement ] );
#############################################################################
##
#O ReducedSum( <rws>, <left>, <right> )
##
## <ManSection>
## <Oper Name="ReducedSum" Arg='rws, left, right'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedSum",
[ IsRewritingSystem,
IsAdditiveElement,
IsAdditiveElement ] );
#############################################################################
##
#O ReducedZero( <rws> )
##
## <ManSection>
## <Oper Name="ReducedZero" Arg='rws'/>
##
## <Description>
## </Description>
## </ManSection>
##
DeclareOperation(
"ReducedZero",
[ IsRewritingSystem ] );
#############################################################################
##
#V InfoConfluence
##
DeclareInfoClass("InfoConfluence");
[ Normaldarstellung0.19Diashow
Übersetzung europäischer Sprachen durch Browser
]
|
