diff options
| author | dos-reis <gdr@axiomatics.org> | 2013-06-18 00:47:44 +0000 |
|---|---|---|
| committer | dos-reis <gdr@axiomatics.org> | 2013-06-18 00:47:44 +0000 |
| commit | 5d68f2651a08223febcc172a6cb49a6e92899034 (patch) | |
| tree | dfea7ee6418af2cb05fd0747facf7ff92b4fa1c9 /src/algebra/catdef.spad.pamphlet | |
| parent | 7db3376a614a5aeacc114c38002ea65e57046dc5 (diff) | |
| download | open-axiom-5d68f2651a08223febcc172a6cb49a6e92899034.tar.gz | |
* algebra/catdef.spad.pamphlet (CommutativeOperatorCategory): New.
(CommutativeOperation): Likewise.
* algebra/Makefile.am (oa_algebra_layer_0): Include them.
Diffstat (limited to 'src/algebra/catdef.spad.pamphlet')
| -rw-r--r-- | src/algebra/catdef.spad.pamphlet | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet index b2daad4e..9e6a8102 100644 --- a/src/algebra/catdef.spad.pamphlet +++ b/src/algebra/catdef.spad.pamphlet @@ -42,6 +42,39 @@ BinaryOperation(T: Type): Join(BinaryOperatorCategory T, SetCategory) with @ +\section{Commutative Operations} + +<<category COMOPC CommutativeOperatorCategory>>= +)abbrev category COMOPC CommutativeOperatorCategory +++ Author: Gabriel Dos Reis +++ Date Created: June 17, 2013 +++ Date Last Modified: June 17, 2013 +++ Description: +++ This is the category of all domains that implement commutative operations. +CommutativeOperatorCategory(T: BasicType): Category == + BinaryOperatorCategory T with + assume commutativity == + forall(f: %, x: T, y: T) . f(x,y) = f(y,x) +@ + +<<domain COMOP CommutativeOperation>>= +)abbrev domain COMOP CommutativeOperation +++ Author: Gabriel Dos Reis +++ Date Created: June 17, 2013 +++ Date Last Modified: June 17, 2013 +++ Description: +++ This domain implements commutative operations. +CommutativeOperation(T: BasicType): Public == Private where + Public == Join(CommutativeOperatorCategory T, CoercibleTo BinaryOperation T) + with + commutativeOperation: ((T,T) -> T) -> % + ++ \spad{commutativeOperation f} constructs a commutative operation + ++ over \spad{T}, thus asserting a commutativity property. + Private == BinaryOperation T add + commutativeOperation f == per binaryOperation f + coerce(x: %): BinaryOperation T == rep x +@ + \section{Idempotent operations} @@ -2255,6 +2288,8 @@ Functorial(S: Type): Category == Type with <<category FUNCTOR Functorial>> <<category BINOPC BinaryOperatorCategory>> <<domain BINOP BinaryOperation>> +<<category COMOPC CommutativeOperatorCategory>> +<<domain COMOP CommutativeOperation>> <<category IDEMOPC IdempotentOperatorCategory>> <<category SGPOPC SemiGroupOperatorCategory>> <<domain SGPOP SemiGroupOperation>> |