Introduction
Bi-graded linear operators (transformations) over n-dimensional vector spaces on a commutative ring . Members of this domain are morphisms . Products, permutations and composition (grafting) of morphisms are implemented. Operators are represented internally as tensors.
Operator composition and products can be visualized by directed graphs (read from top to bottom) such as:
n = 3 inputs
m = 0 outputs
External vertices in this graph represent vectors, and tensors. Internal nodes and arcs (edges) represent linear operators. Horizontal juxtaposition (i.e. a horizontal cross-section) represents tensor product. Vertical juxtaposition represents operator composition.
See examples and documentation below
I would like you to make brief comments in the form at the bottom of this web page. For more detailed but related comments click discussion on the top menu.
Regards,
Bill Page.
We try to start the right way by defining the concept of a monoidal category.
Ref: http://en.wikipedia.org/wiki/PROP_(category_theory)
spad
)abbrev category MONAL Monoidal
Monoidal(R:AbelianSemiGroup):Category == Monoid with
dom: % -> R
++ domain
cod: % -> R
++ co-domain
_/: (%,%) -> %
++ vertical composition f/g
apply:(%,%) -> %
++ horizontal product f g = f*g
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/3243124937217769214-25px001.spad using
old system compiler.
MONAL abbreviates category Monoidal
------------------------------------------------------------------------
initializing NRLIB MONAL for Monoidal
compiling into NRLIB MONAL
;;; *** |Monoidal| REDEFINED
Time: 0.03 SEC.
finalizing NRLIB MONAL
Processing Monoidal for Browser database:
--------(dom (R %))---------
--------(cod (R %))---------
--------(/ (% % %))---------
--->-->Monoidal((/ (% % %))): Improper first word in comments: vertical
"vertical composition \\spad{f/g}"
--------(apply (% % %))---------
--->-->Monoidal((apply (% % %))): Improper first word in comments: horizontal
"horizontal product \\spad{f} \\spad{g} = \\spad{f*g}"
--->-->Monoidal(constructor): Not documented!!!!
--->-->Monoidal(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/MONAL.NRLIB/MONAL.lsp" (written 19 APR 2011 08:38:04 PM):
; /var/zope2/var/LatexWiki/MONAL.NRLIB/MONAL.fasl written
; compilation finished in 0:00:00.048
------------------------------------------------------------------------
Monoidal is now explicitly exposed in frame initial
Monoidal will be automatically loaded when needed from
/var/zope2/var/LatexWiki/MONAL.NRLIB/MONAL
>> System error:
The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
The ANSI Standard, Glossary entry for "bounding index designator"
The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR
The initial object in this category is the domain Prop (Products and Permutations).
spad
)abbrev domain PROP Prop
Prop(): Exports == Implementation where
NNI ==> NonNegativeInteger
Exports ==> Join(Monoidal NNI, CoercibleTo OutputForm) with
_/:(NNI,NNI) -> %
++ Prop constructor
Implementation ==> add
Rep == Record(domain:NNI,codomain:NNI)
rep(x:%):Rep == x pretend Rep
per(x:Rep):% == x pretend %
dom(f:%):NNI == rep(f).domain
cod(f:%):NNI == rep(f).codomain
coerce(f:%):OutputForm == dom(f)::OutputForm / cod(f)::OutputForm
(f:NNI / g:NNI):% == per [f,g]
I == per [1,1]
-- evaluation
(ff:% / gg:%):% ==
g:=gg; f:=ff
-- partial application from the left
n:=subtractIfCan(cod ff,dom gg)
if n case NNI and n>0 then
-- apply g on f from the left, pass extra f outputs on the right
print(hconcat([message("arity warning: "), _
over(ff::OutputForm, _
gg::OutputForm*(I::OutputForm)^n::OutputForm) ]))$OutputForm
g:=gg*I^n
m:=subtractIfCan(dom gg, cod ff)
-- apply g on f from the left, add extra g inputs on the left
if m case NNI and m>0 then
print(hconcat([message("arity warning: "), _
over((I::OutputForm)^m::OutputForm*ff::OutputForm, _
gg::OutputForm)]))$OutputForm
f:=I^m*ff
f/g
0:% == per [0,0]
1:% == per [0,0]
-- product
apply(f:%,g:%):% == f * g
(f:% * g:%):% == per [dom(f)+dom(g),cod(f)+cod(g)]
-- preserves arity
(f:% + g:%):% ==
dom(f)~=dom(g) or cod(g) ~= cod(g) => error "arity"
f
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/9071963415324596130-25px002.spad using
old system compiler.
PROP abbreviates domain Prop
------------------------------------------------------------------------
initializing NRLIB PROP for Prop
compiling into NRLIB PROP
compiling local rep : $ -> Record(domain: NonNegativeInteger,codomain: NonNegativeInteger)
PROP;rep is replaced by x
Time: 0.05 SEC.
compiling local per : Record(domain: NonNegativeInteger,codomain: NonNegativeInteger) -> $
PROP;per is replaced by x
Time: 0 SEC.
compiling exported dom : $ -> NonNegativeInteger
Time: 0 SEC.
compiling exported cod : $ -> NonNegativeInteger
Time: 0.01 SEC.
compiling exported coerce : $ -> OutputForm
Time: 0.01 SEC.
compiling exported / : (NonNegativeInteger,NonNegativeInteger) -> $
Time: 0 SEC.
compiling exported / : ($,$) -> $
Time: 0.03 SEC.
compiling local Zero : () -> $
Time: 0.01 SEC.
compiling exported One : () -> $
Time: 0 SEC.
compiling exported apply : ($,$) -> $
Time: 0 SEC.
compiling exported * : ($,$) -> $
Time: 0.01 SEC.
compiling local + : ($,$) -> $
Time: 0.01 SEC.
(time taken in buildFunctor: 0)
;;; *** |Prop| REDEFINED
;;; *** |Prop| REDEFINED
Time: 0.01 SEC.
Cumulative Statistics for Constructor Prop
Time: 0.14 seconds
finalizing NRLIB PROP
Processing Prop for Browser database:
--------(/ (% NNI NNI))---------
--->-->Prop(constructor): Not documented!!!!
--->-->Prop(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/PROP.NRLIB/PROP.lsp" (written 19 APR 2011 08:38:05 PM):
; /var/zope2/var/LatexWiki/PROP.NRLIB/PROP.fasl written
; compilation finished in 0:00:00.259
------------------------------------------------------------------------
Prop is now explicitly exposed in frame initial
Prop will be automatically loaded when needed from
/var/zope2/var/LatexWiki/PROP.NRLIB/PROP
>> System error:
The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
The ANSI Standard, Glossary entry for "bounding index designator"
The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR
The LinearOperator? domain is Moniodal over NonNegativeInteger?. It is the free algebra over Prop with n-generators.
Ref: http://en.wikipedia.org/wiki/Category_of_vector_spaces
- all members of this domain have the same dimension
- it might be useful (but much more complicated) to allow source
and target dimensions to be different
spad
)abbrev domain LIN LinearOperator
LinearOperator(dim:NNI,gen:OrderedFinite,K:CommutativeRing): Exports == Implementation where
NNI ==> NonNegativeInteger
NAT ==> PositiveInteger
T ==> CartesianTensor(1,dim,K)
Exports ==> Join(Field, BiModule(K,K), Monoidal NNI, RetractableTo K) with
inp: List K -> %
++ incoming vector
inp: List % -> %
out: List K -> %
++ output vector
out: List % -> %
arity: % -> Prop
basisVectors: () -> List %
basisForms: () -> List %
tensor: % -> T
map: (K->K,%) -> %
if K has Evalable(K) then Evalable(K)
ravel: % -> List K
unravel: (Prop,List K) -> %
coerce:(x:List NAT) -> %
++ identity for composition and permutations of its products
coerce:(x:List None) -> %
++ [] = 1
elt: (%,%) -> %
elt: (%,NAT) -> %
elt: (%,NAT,NAT) -> %
elt: (%,NAT,NAT,NAT) -> %
Implementation ==> add
import List NNI
import NAT
Rep == Record(domain:NNI, codomain:NNI, data:T)
rep(x:%):Rep == x pretend Rep
per(x:Rep):% == x pretend %
-- Prop (arity)
dom(f:%):NNI == rep(f).domain
cod(f:%):NNI == rep(f).codomain
dat(f:%):T == rep(f).data
arity(f:%):Prop == dom(f)/cod(f)
retractIfCan(f:%):Union(K,"failed") ==
dom(f)=0 and cod(f)=0 => retract(dat f)$T
return "failed"
retract(f:%):K ==
dom(f)=0 and cod(f)=0 => retract(dat f)$T
error "failed"
-- basis
basisVectors():List % == [per [0,1,entries(row(1,i)$SquareMatrix(dim,K))::T] for i in 1..dim]
basisForms():List % == [per [1,0,entries(row(1,i)$SquareMatrix(dim,K))::T] for i in 1..dim]
-- manipulation
map(f:K->K, g:%):% == per [dom g,cod g,unravel(map(f,ravel dat g))$T]
if K has Evalable(K) then
eval(g:%,f:List Equation K):% == map((x:K):K+->eval(x,f),g)
ravel(g:%):List K == ravel dat g
unravel(p:Prop,r:List K):% ==
dim^(dom(p)+cod(p)) ~= #r => error "failed"
per [dom(p),cod(p),unravel(r)$T]
tensor(x:%):T == dat(x)
-- sum
(f:% + g:%):% ==
dat(f)=0 => g
dat(g)=0 => f
dom(f) ~= dom(g) or cod(f) ~= cod(g) => error "arity"
per [dom f,cod f,dat(f)+dat(g)]
(f:% - g:%):% ==
dat(f)=0 => g
dat(g)=0 => f
dom(f) ~= dom(f) or cod(g) ~= cod(g) => error "arity"
per [dom f, cod f,dat(f)-dat(g)]
_-(f:%):% == per [dom f, cod f,-dat(f)]
-- identity for sum (trivial zero map)
0 == per [0,0,0]
-- identity for product
1:% == per [0,0,1]
-- identity for composition
I == per([1,1,kroneckerDelta()$T])
-- repeated sum
(p:NNI * f:%):% ==
p=1 => f
q:=subtractIfCan(p,1)
q case NNI => q*f + f
-- zero map (non-trivial)
per [dom f,cod f,0*dat(f)]
-- permutations and identities
coerce(p:List NAT):% ==
r:=I^#p
#p = 1 and p.1 = 1 => return r
p1:List Integer:=[i for i in 1..#p]
p2:List Integer:=[#p+i for i in p]
p3:=concat(p1,p2)
per [#p,#p,reindex(dat r,p3)]
coerce(p:List None):% == per [0,0,1]
coerce(x:K):% == 1*x
-- product
elt(f:%,g:%):% == f * g
elt(f:%,g:NAT):% == f * I^g
-- why do we have to pretend? !!
elt(f:%,g1:NAT,g2:NAT):% == f * [g1 pretend NAT,g2 pretend NAT]::List NAT::%
elt(f:%,g1:NAT,g2:NAT,g3:NAT):% == f * [g1 pretend NAT,g2 pretend NAT,g3 pretend NAT]::List NAT::%
apply(f:%,g:%):% == f * g
(f:% * g:%):% ==
r:T := product(dat f,dat g)
-- dom(f) + cod(f) + dom(g) + cod(g)
p:List Integer := concat _
[[i for i in 1..dom(f)], _
[dom(f)+cod(f)+i for i in 1..dom(g)], _
[dom(f)+i for i in 1..cod(f)], _
[dom(f)+dom(g)+cod(f)+i for i in 1..cod(g)]]
-- dom(f) + dom(g) + cod(f) + cod(g)
per [dom(f)+dom(g),cod(f)+cod(g),reindex(r,p)]
-- repeated product
(f:% ^ p:NNI):% ==
p=1 => f
q:=subtractIfCan(p,1)
q case NNI => f^q * f
1
-- evaluation:
-- f/g : A^n -> A^p = f:A^n -> A^m / g:A^m -> A^p
(ff:% / gg:%):% ==
g:=gg; f:=ff
-- partial application from the left
n:=subtractIfCan(cod ff,dom gg)
if n case NNI and n>0 then
-- apply g on f from the left, pass extra f outputs on the right
print(hconcat([message("arity warning: "), _
over(arity(ff)::OutputForm, _
arity(gg)::OutputForm*(arity(I)::OutputForm)^n::OutputForm) ]))$OutputForm
g:=gg*I^n
m:=subtractIfCan(dom gg, cod ff)
-- apply g on f from the left, add extra g inputs on the left
if m case NNI and m>0 then
print(hconcat([message("arity warning: "), _
over((arity(I)::OutputForm)^m::OutputForm*arity(ff)::OutputForm, _
arity(gg)::OutputForm)]))$OutputForm
f:=I^m*ff
-- dom(g) ~= cod(f) => error "arity"
r:T := product(dat f, dat g)
g1:Integer:=dom(f)+1
f1:Integer:=dom(f)+cod(f)+1
for i in 0..cod(f)-1 repeat
r := contract(r,g1,f1-i)
per [dom(f),cod(g),r]
-- inherited from Ring
(x:% = y:%):Boolean ==
dom(x) ~= dom(y) or cod(x) ~= cod(y) => error "arity"
dat(x) = dat(y)
(x:K * y:%):% == per [dom y, cod y,x*dat(y)]
(x:% * y:K):% == per [dom x,cod x,dat(x)*y]
(x:Integer * y:%):% == per [dom y,cod y,x*dat(y)]
-- constructors
inp(x:List K):% == per [1,0,entries(x)::T]
inp(x:List %):% ==
#removeDuplicates([dom(y) for y in x]) ~= 1 or
#removeDuplicates([cod(y) for y in x]) ~= 1 => error "arity"
per [(dom(first x)+1),cod(first x),[dat(y) for y in x]::T]$Rep
out(x:List K):% == per [0,1,entries(x)::T]
out(x:List %):% ==
#removeDuplicates([dom(y) for y in x])~=1 or
#removeDuplicates([cod(y) for y in x])~=1 => error "arity"
per [dom(first x),(cod(first x)+1),[dat(y) for y in x]::T]$Rep
-- display operators using basis
coerce(x:%):OutputForm ==
dom(x)=0 and cod(x)=0 => return dat(x)::OutputForm
if size()$gen > 0 then
gens:List OutputForm:=[index(i::PositiveInteger)$gen::OutputForm for i in 1..dim]
else
-- default to numeric indices
gens:List OutputForm:=[i::OutputForm for i in 1..dim]
-- input basis
inps:List OutputForm := []
for i in 1..dom(x) repeat
empty? inps => inps:=gens
inps:=concat [[(inps.k * gens.j) for j in 1..dim] for k in 1..#inps]
-- output basis
outs:List OutputForm := []
for i in 1..cod(x) repeat
empty? outs => outs:=gens
outs:=concat [[(outs.k * gens.j) for j in 1..dim] for k in 1..#outs]
-- combine input (superscripts) and/or output(subscripts) to form basis symbols
bases:List OutputForm := []
if #inps > 0 and #outs > 0 then
bases:=concat([[ scripts(message("|"),[i,j]) for i in outs] for j in inps])
else if #inps > 0 then
bases:=[super(message("|"),i) for i in inps]
else if #outs > 0 then
bases:=[sub(message("|"),j) for j in outs]
-- merge bases with data to form term list
terms:=[(k=1 => base;k::OutputForm*base)
for base in bases for k in ravel dat(x) | k~=0]
empty? terms => return 0::OutputForm
-- combine the terms
return reduce(_+,terms)
spad
Compiling FriCAS source code from file
/var/zope2/var/LatexWiki/3864091039844420508-25px003.spad using
old system compiler.
LIN abbreviates domain LinearOperator
------------------------------------------------------------------------
initializing NRLIB LIN for LinearOperator
compiling into NRLIB LIN
importing List NonNegativeInteger
importing PositiveInteger
compiling local rep : $ -> Record(domain: NonNegativeInteger,codomain: NonNegativeInteger,data: CartesianTensor(One,dim,K))
LIN;rep is replaced by x
Time: 0.09 SEC.
compiling local per : Record(domain: NonNegativeInteger,codomain: NonNegativeInteger,data: CartesianTensor(One,dim,K)) -> $
LIN;per is replaced by x
Time: 0 SEC.
compiling exported dom : $ -> NonNegativeInteger
Time: 0.01 SEC.
compiling exported cod : $ -> NonNegativeInteger
Time: 0 SEC.
compiling local dat : $ -> CartesianTensor(One,dim,K)
Time: 0 SEC.
compiling exported arity : $ -> Prop
Time: 0 SEC.
compiling exported retractIfCan : $ -> Union(K,failed)
Time: 0.01 SEC.
compiling exported retract : $ -> K
Time: 0.01 SEC.
compiling exported basisVectors : () -> List $
Time: 0.16 SEC.
compiling exported basisForms : () -> List $
Time: 0.03 SEC.
compiling exported map : (K -> K,$) -> $
Time: 0.04 SEC.
****** Domain: K already in scope
augmenting K: (Evalable K)
compiling exported eval : ($,List Equation K) -> $
Time: 0.01 SEC.
compiling exported ravel : $ -> List K
Time: 0.01 SEC.
compiling exported unravel : (Prop,List K) -> $
Time: 0.05 SEC.
compiling exported tensor : $ -> CartesianTensor(One,dim,K)
Time: 0.01 SEC.
compiling exported + : ($,$) -> $
Time: 0.01 SEC.
compiling exported - : ($,$) -> $
Time: 0.01 SEC.
compiling exported - : $ -> $
Time: 0 SEC.
compiling exported Zero : () -> $
Time: 0 SEC.
compiling exported One : () -> $
Time: 0.01 SEC.
compiling exported * : (NonNegativeInteger,$) -> $
Time: 0 SEC.
compiling exported coerce : List PositiveInteger -> $
Time: 0.03 SEC.
compiling exported coerce : List None -> $
Time: 0.01 SEC.
compiling exported coerce : K -> $
Time: 0.03 SEC.
compiling exported elt : ($,$) -> $
Time: 0 SEC.
compiling exported elt : ($,PositiveInteger) -> $
Time: 0 SEC.
compiling exported elt : ($,PositiveInteger,PositiveInteger) -> $
Time: 0 SEC.
compiling exported elt : ($,PositiveInteger,PositiveInteger,PositiveInteger) -> $
Time: 0.01 SEC.
compiling exported apply : ($,$) -> $
Time: 0 SEC.
compiling exported * : ($,$) -> $
Time: 0.07 SEC.
compiling exported ^ : ($,NonNegativeInteger) -> $
Time: 0 SEC.
compiling exported / : ($,$) -> $
Time: 0.05 SEC.
compiling exported = : ($,$) -> Boolean
Time: 0.01 SEC.
compiling exported * : (K,$) -> $
Time: 0 SEC.
compiling exported * : ($,K) -> $
Time: 0 SEC.
compiling exported * : (Integer,$) -> $
Time: 0 SEC.
compiling exported inp : List K -> $
Time: 0 SEC.
compiling exported inp : List $ -> $
Time: 0.04 SEC.
compiling exported out : List K -> $
Time: 0 SEC.
compiling exported out : List $ -> $
Time: 0.02 SEC.
compiling exported coerce : $ -> OutputForm
Time: 0.07 SEC.
****** Domain: K already in scope
augmenting K: (Evalable K)
(time taken in buildFunctor: 10)
;;; *** |LinearOperator| REDEFINED
;;; *** |LinearOperator| REDEFINED
Time: 0.28 SEC.
Warnings:
[1] elt: pretend(PositiveInteger) -- should replace by @
[2] coerce: bases has no value
Cumulative Statistics for Constructor LinearOperator
Time: 1.08 seconds
finalizing NRLIB LIN
Processing LinearOperator for Browser database:
--------(inp (% (List K)))---------
--->-->LinearOperator((inp (% (List %)))): Not documented!!!!
--------(out (% (List K)))---------
--->-->LinearOperator((out (% (List %)))): Not documented!!!!
--->-->LinearOperator((arity ((Prop) %))): Not documented!!!!
--->-->LinearOperator((basisVectors ((List %)))): Not documented!!!!
--->-->LinearOperator((basisForms ((List %)))): Not documented!!!!
--->-->LinearOperator((tensor (T$ %))): Not documented!!!!
--->-->LinearOperator((map (% (Mapping K K) %))): Not documented!!!!
--->-->LinearOperator((ravel ((List K) %))): Not documented!!!!
--->-->LinearOperator((unravel (% (Prop) (List K)))): Not documented!!!!
--------(coerce (% (List NAT)))---------
--->-->LinearOperator((coerce (% (List NAT)))): Improper first word in comments: identity
"identity for composition and permutations of its products"
--------(coerce (% (List (None))))---------
--->-->LinearOperator((coerce (% (List (None))))): Improper first word in comments: []
"[] = 1"
--->-->LinearOperator((elt (% % %))): Not documented!!!!
--->-->LinearOperator((elt (% % NAT))): Not documented!!!!
--->-->LinearOperator((elt (% % NAT NAT))): Not documented!!!!
--->-->LinearOperator((elt (% % NAT NAT NAT))): Not documented!!!!
--->-->LinearOperator(constructor): Not documented!!!!
--->-->LinearOperator(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/LIN.NRLIB/LIN.lsp" (written 19 APR 2011 08:38:09 PM):
; /var/zope2/var/LatexWiki/LIN.NRLIB/LIN.fasl written
; compilation finished in 0:00:03.171
------------------------------------------------------------------------
LinearOperator is now explicitly exposed in frame initial
LinearOperator will be automatically loaded when needed from
/var/zope2/var/LatexWiki/LIN.NRLIB/LIN
>> System error:
The bounding indices 163 and 162 are bad for a sequence of length 162.
See also:
The ANSI Standard, Glossary entry for "bounding index designator"
The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR
Consult the source code above for more details.
Conveniences
axiom
-- summation
macro Σ(x,i)==reduce(+,[x for i in 1..dim])
Type: Void
axiom
-- list comprehension
macro Ξ(f,i)==[f for i in 1..dim]
Type: Void
Basis
axiom
dim:=2
axiom
Q:=EXPR INT
Type: Type
axiom
L:=LinearOperator(dim,OVAR [x,y],Q)
Type: Type
axiom
Dx:=basisVectors()$L
Type: List(LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer)))
axiom
dx:=basisForms()$L
Type: List(LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer)))
axiom
matrix Ξ(Ξ( dx.i * Dx.j, i),j)
Type: Matrix(LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer)))
axiom
matrix Ξ(Ξ( Dx.i / dx.j, i),j)
Type: Matrix(LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer)))
Construction
axiom
A1:L := Σ(superscript(a1,[i])*dx.i,i)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity A1
Type: Prop
axiom
A2:L := Σ(superscript(a2,[i])*dx.i,i)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
A:L := inp[A1,A2]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity A
Type: Prop
axiom
B1:L := Σ(subscript(b1,[i])*Dx.i,i)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity B1
Type: Prop
axiom
B2:L := Σ(subscript(b2,[i])*Dx.i,i)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
B:L := out[B1,B2]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity B
Type: Prop
axiom
BB:L := Σ(Σ(subscript(b,[i,j])*Dx.i*Dx.j,i),j)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
W:L := Σ(Σ(Σ(script(w,[[k],[i,j]])*(Dx.k*dx.i*dx.j),k),i),j)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
Composition (evaluation)
axiom
AB2 := A2 / B2; AB2::OutputForm = A2::OutputForm / B2::OutputForm
Type: Equation(OutputForm
?)
axiom
arity(AB2)::OutputForm = arity(A2)::OutputForm / arity(B2)::OutputForm
Type: Equation(OutputForm
?)
axiom
BA1 := B1 / A1; BA1::OutputForm = B1::OutputForm / A1::OutputForm
Type: Equation(OutputForm
?)
axiom
arity(BA1)::OutputForm = arity(B1)::OutputForm / arity(A1)::OutputForm
Type: Equation(OutputForm
?)
axiom
AB1 := A1 / B1; AB1::OutputForm = A1::OutputForm / B1::OutputForm
Type: Equation(OutputForm
?)
axiom
arity(AB1)::OutputForm = arity(A1)::OutputForm / arity(B1)::OutputForm
Type: Equation(OutputForm
?)
Partial Evaluation
axiom
BBA1 := B/A1
0
-
2
arity warning: ------
1 1 1
- (-)
0 1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
BBA2 := B/B1
0
-
2
arity warning: ------
0 1 2
- (-)
1 1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
BBA3 := A1/A
1 2 1
(-) -
1 0
arity warning: ------
2
-
0
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
BBA4 := B1/A
1 1 0
(-) -
1 1
arity warning: ------
2
-
0
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
Powers
axiom
AB3:=(AB1*AB1)*AB1;
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(AB3)
Type: Prop
axiom
test(AB3=AB1*(AB1*AB1))
Type: Boolean
axiom
test(AB3=AB1^3)
Type: Boolean
Sums
axiom
A12s := A1 + A2; A12s::OutputForm = A1::OutputForm + A2::OutputForm
Type: Equation(OutputForm
?)
axiom
arity(A12s)::OutputForm = arity(A1)::OutputForm + arity(A2)::OutputForm
Type: Equation(OutputForm
?)
axiom
B12s := B1 + B2; B12s::OutputForm = B1::OutputForm + B2::OutputForm
Type: Equation(OutputForm
?)
axiom
arity(B12s)::OutputForm = arity(B1)::OutputForm + arity(B2)::OutputForm
Type: Equation(OutputForm
?)
axiom
-B12s
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
Multiplication
axiom
A3s:=(A1+A1)+A1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(A3s)
Type: Prop
axiom
test(A3s=A1+(A1+A1))
Type: Boolean
axiom
test(A3s=A1*3)
Type: Boolean
axiom
B3s:=(B1+B1)+B1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(B3s)
Type: Prop
axiom
test(B3s=B1+(B1+B1))
Type: Boolean
axiom
test(B3s=B1*3)
Type: Boolean
Product
axiom
AB11:=A1*B1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(AB11)
Type: Prop
axiom
BA11:= B1*A1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(BA11)
Type: Prop
axiom
AB := A*B
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(AB)
Type: Prop
axiom
BA := B*A
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(BA)
Type: Prop
axiom
WB1:=W*B1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(WB1)
Type: Prop
axiom
X2:L:=inp[inp([script(x,[[],[i,j]]) for j in 1..2])$L for i in 1..dim]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
XB21:=X2*B1
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(XB21)
Type: Prop
axiom
Y2:L:=out[out([script(y,[[i,j]]) for j in 1..2])$L for i in 1..dim]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
XY22:=X2*Y2
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(XY22)
Type: Prop
axiom
YX22:=Y2*X2
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity(XY22)
Type: Prop
axiom
test((A*A)*A=A*(A*A))
Type: Boolean
axiom
test((B*B)*B=B*(B*B))
Type: Boolean
axiom
test((A*B)*A=A*(B*A))
Type: Boolean
Permutations and Identities
axiom
H:L:=[1,2]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
X:L:=[2,1]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
test(X/X=H)
Type: Boolean
Manipulations
axiom
tensor AB
Type: CartesianTensor
?(1,
2,
Expression(Integer))
axiom
ravel AB
Type: List(Expression(Integer))
axiom
test(unravel(arity AB,ravel AB)$L=AB)
Type: Boolean
axiom
map(x+->x+1,AB)$L
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
[superscript(a1,[i])=i for i in 1..dim]::List EQ Q
Type: List(Equation(Expression(Integer)))
axiom
eval(A,[superscript(a1,[i])=i for i in 1..dim]::List EQ Q)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
Examples
Another kind of diagram:
Y = Y
U U
Algebra
axiom
Y:=out[inp[inp([script(y,[[k],[i,j]]) for j in 1..2])$L for i in 1..2] for k in 1..2]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
Y:=Σ(Σ(Σ(script(y,[[k],[i,j]])*Dx.k*dx.i*dx.j,j),i),k)
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity Y
Type: Prop
axiom
tensor Y
Type: CartesianTensor
?(1,
2,
Expression(Integer))
Commutator
Algebra
axiom
Y - [2,1]
/ Y
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
Pairing
axiom
U:=inp[inp([script(u,[[],[i,j]]) for j in 1..2])$L for i in 1..2]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity U
Type: Prop
3-point function
axiom
I:L:=[1]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
YU := Y I
/ U
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
YU := Y.I
/ U
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity YU
Type: Prop
Oddities (should work on the right)
axiom
YU := Y [1]
/ U
There are no exposed library operations named Y but there are 2
unexposed operations with that name. Use HyperDoc Browse or issue
)display op Y
to learn more about the available operations.
Cannot find a definition or applicable library operation named Y
with argument type(s)
List(PositiveInteger)
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.
YU := Y.[1]
/ U
There are no exposed library operations named Y but there are 2
unexposed operations with that name. Use HyperDoc Browse or issue
)display op Y
to learn more about the available operations.
Cannot find a definition or applicable library operation named Y
with argument type(s)
List(PositiveInteger)
Perhaps you should use "@" to indicate the required return type,
or "$" to specify which version of the function you need.
Ok on the left
axiom
UY := [1].Y
/ U
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
UY := [1] Y
/ U
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity UY
Type: Prop
Co-algebra
axiom
λ:=inp[out[out([script(y,[[i],[j,k]]) for k in 1..2])$L for j in 1..2] for i in 1..2]
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity λ
Type: Prop
axiom
tensor λ
Type: CartesianTensor
?(1,
2,
Expression(Integer))
Handle
λ
Y
axiom
Φ := λ
/ Y
Type: LinearOperator
?(2,
OrderedVariableList
?([x,
y]),
Expression(Integer))
axiom
arity Φ
Type: Prop
Back to the top.
Please leave comments and suggestions.
Thanks
Bill Page
If linear operators really are to be morphisms (in the sense of category theory) then they must have a domain and a co-domain that are vector spaces, not just an in-degree and out-degree. E.g.:
Rep == Record(Dom:VectorSpace, Cod:VectorSpace, t:T)
But VectorSpace? is a category which would make Dom and Cod domains. The domains that currently satisfy VectorSpace? in Axiom are rather limited and seem oddly focused on number theory (finite fields). It is a good thing however that DirectProduct? is a conditional member of this cateogry.
axiom
DirectProduct(2,FRAC INT) has VectorSpace(FRAC INT)
Type: Boolean
Unfortunately:
axiom
DirectProduct(2,DirectProduct(2,FRAC INT)) has VectorSpace(FRAC INT)
Type: Boolean
The problem with VectorSpace? is that the domain [Vector]? is not a member of this category instead it satisfies VectoryCategory?.
Is it possible to treat tensors from CartesianTensor? as maps from VectorSpace? to VectorSpace?? We would like for example:
T:DirectProduct(dim,DirectProduct(dim,FRAC INT)) -> DirectProduct(dim,FRAC INT))
To be a linear operator with two inputs and one output.
A [FreeModule]
? over a [Field]
? is a VectorSpace
? unfortunately this is not currently understood by Axiom:
axiom
FreeModule(Fraction Integer,OrderedVariableList [e1,e1]) has VectorSpace(Fraction Integer)
Type: Boolean