help links subscribe changes refresh edit

	ClosedLinearOperator
	↑	→ SandBoxRibbonCategory

SandBoxClosedLinearOperator

Edit detail for SandBoxClosedLinearOperator revision 1 of 3

	1 2 3
Editor: Bill Page Time: 2011/05/31 18:56:10 GMT-7
Note: testing and bug fixes

changed:
-
Introduction

  Bi-graded two-color linear operators (transformations) over a finite n-dimensional vector space, including products and duals on a field $K$. Members of this domain are morphisms $K^{\pm^n} \to K^{\pm^m},$ where $K^{+}=K,$ $K^{++}=A\otimes A,$ and $K^{-}=K^*,$ (dual), etc. Products, permutations and composition (grafting) of morphisms are implemented.  Operators are represented internally as tensors.

Operator composition and products can be visualized by oriented directed graphs. The graphs have a top and a bottom and arrows are directed either downwards or upwards.

External vertices in this graph represent vectors, tensors and their duals. Internal nodes and arcs (edges) represent linear operators. Edges may be one of two different "colors" (labelled + and - in the code that follows) or marked with arrows directed either downwards (+) or upwards (-). Horizontal juxtaposition (i.e. a horizontal cross-section) represents tensor product. Vertical juxtaposition of edges of the same color represents operator composition.

See examples and documentation <a href="#getting_started">below</a>

I would be glad if you to make brief comments in the form at the <a href="#comments">bottom</a> of this web page. For more detailed but related comments click "discussion":http:/LinearOperatorDiscussion on the top menu.

Regards,
Bill Page.

<a name="source_code">Source Code</a>

  We try to start by defining the concept of a compact closed category.

Ref:

- http://en.wikipedia.org/wiki/Closed_monoidal_category

- http://en.wikipedia.org/wiki/Compact_closed_category

\begin{spad}
)abbrev domain ARITY Arity
Arity():  Exports == Implementation where
  COLOR ==> OrderedVariableList ['_+,'_-]
  LIST2 ==> ListFunctions2
  NNI ==> NonNegativeInteger
  RS ==> Record(gen:COLOR,exp:NNI)

  Exports ==> Join(Monoid, RetractableTo COLOR) with
    index: PositiveInteger -> %
    dn: () -> %
      ++ default
    up: () -> %
      ++ dual
    0: %
      ++ use 0 for identity
    "+": (%,%) -> %
      ++ composition
    size: % -> NonNegativeInteger
    len: % -> Integer
    color: (%,NNI) -> %
    overlap: (%,%) -> Record(lm:%, mm:%, rm:%)
  Implementation ==> FreeMonoid COLOR add
    Rep == FreeMonoid COLOR
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %
    index(x:PositiveInteger):% == per(index(x)$COLOR ::Rep)
    up():% == index(2)
    dn():% == index(1)
    0:% == per 1
    (f:% + g:%):% == per(rep f * rep g)
    coerce(x:%):OutputForm == (rep(x)=1 => message "0";rep(x)::OutputForm)
    -- size of FreeMonoid is just number of factors
    -- len is total length
    len(f:%):Integer ==
      reduce(_+,map(x+->x.exp,factors rep f)$LIST2(RS,NNI),0)$List(NNI) pretend Integer
    -- i'th element
    color(f:%,i:NNI):% ==
      j:NNI:=0
      for x in factors rep f repeat
        j:=j+x.exp
        if j>=i then
          return per coerce x.gen
      error "index error"
\end{spad}

\begin{spad}
)abbrev category CMONAL ClosedMonoidal
ClosedMonoidal():Category == Ring with
    dom: % -> Arity
      ++ domain
    cod: % -> Arity
      ++ co-domain
    _/: (%,%) -> %
      ++ vertical composition f/g
    apply: (%,%) -> %
      ++ horizontal product f g = f*g
    "^": (%,Arity) -> %
      ++ colored power
    dagger: % -> %
      ++ reverse arrows:
      ++ cod f = dom dagger f
      ++ dom f = cod dagger f
\end{spad}

The initial object in this category is the domain ClosedProp (Products and Permutations). The ClosedProp domain represents everything that is "constant" about all the domains in this category. It can be defined as an endofunctor with only the information available about the category itself. 

\begin{spad}
)abbrev domain CPROP ClosedProp
ClosedProp(L:ClosedMonoidal): Exports == Implementation where

  Exports ==> ClosedMonoidal with
    coerce: L -> %

  Implementation ==> add
    Rep == Record(domain:Arity, codomain:Arity)
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %

    coerce(f:%):OutputForm == dom(f)::OutputForm / cod(f)::OutputForm

    coerce(f:L):% == per [dom f, cod f]                    -- coerce(f:L):% == per f

    dom(x:%):Arity == rep(x).domain                          -- dom(x:%):NNI == dom rep x
    cod(x:%):Arity == rep(x).codomain                        -- cod(x:%):NNI == cod rep x
    --0:% == per [1,1]                                       -- 0:% == per 0
    1:% == per [1,1]                                       -- 1:% == per 1
    -- evaluation
    (f:% / g:%):% == per [dom f, cod g]                    -- (f:% / g:%):% == per (rep f / rep g)
    -- product
    apply(f:%,g:%):% == per [dom f * dom g, cod f * cod g] -- apply(f:%,g:%):% == per apply(rep f,rep g)
    (f:% * g:%):% == per [dom f * dom g, cod f * cod g]    --(f:% * g:%):% == per (rep f * rep g)
    -- sum
    --(f:% + g:%):% == per [dom f, cod f]                    --(f:% + g:%):% == per (rep f + rep g)
    dagger(f:%):% == per [cod f, dom f]
    (f:% ^ p:Arity):% ==
       r:% := 1
       for i in 1..len(p) repeat
         if color(p,i)=dn() then
           r:=r*f
         else
           r:=r*dagger(f)
       return r
\end{spad}

The ClosedLinearOperator domain is ClosedMonoidal over FreeMonoid OrderedVariables ['_+,'_-], i.e. strings of $\pm$ symbols. The objects of this domain are all tensor powers of a vector space of fixed dimension. The arrows are linear operators that map from one object (tensor powers of vector space and it's dual) to another such power.

Ref: http://en.wikipedia.org/wiki/Category_of_vector_spaces

- all members of this domain have the same dimension

Faster tensors
\begin{axiom}
)lib CARTEN
\end{axiom}

\begin{spad}
)abbrev domain CLOP ClosedLinearOperator
ClosedLinearOperator(gener:OrderedFinite,K:Field): Exports == Implementation where
  NNI ==> NonNegativeInteger
  Exports ==> Join(Ring, VectorSpace K, ClosedMonoidal, RetractableTo K) with
    arity: % -> ClosedProp %
    basisOut: () -> List %
    basisIn: () -> List %
    map: (K->K,%) -> %
    if K has Evalable(K) then Evalable(K)
    eval: % -> %
    ravel: % -> List K
    unravel: (ClosedProp %,List K) -> %
    coerce:(x:List Integer) -> %
      ++ identity for composition and permutations of its products
    coerce:(x:List None) -> %
      ++ [] = 1
    elt: (%,%) -> %
    elt: (%,Integer) -> %
    elt: (%,Integer,Integer) -> %
    elt: (%,Integer,Integer,Integer) -> %
    _/: (Tuple %,Tuple %) -> %
    _/: (Tuple %,%) -> %
    _/: (%,Tuple %) -> %
      ++ yet another syntax for product
    ev: NNI -> %
      ++ (2,0)-tensor for evaluation
    co: NNI -> %
      ++ (0,2)-tensor for co-evaluation
  Implementation ==> add

    LIST2 ==> ListFunctions2
    dim:NNI := size()$gener
    T := CartesianTensor(1,dim,K)
    L := Record(domain:Arity, codomain:Arity, data:T)
    RR := Record(gen:L,exp:NNI)
    -- FreeMonoid provides unevaluated products
    Rep == FreeMonoid L
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %
    dimension():CardinalNumber == coerce dim

    -- Prop (arity)
    dom(f:%):Arity ==
      reduce(_*,map(x+->(x.gen.domain)^(x.exp),factors rep f)$LIST2(RR,Arity),1)$List(Arity)
    cod(f:%):Arity ==
      reduce(_*,map(x+->(x.gen.codomain)^(x.exp),factors rep f)$LIST2(RR,Arity),1)$List(Arity)
    dagger(f:%):% ==
      r:=1
      for f1 in factors rep f repeat
        p:List Integer := concat [ _
          [len(f1.gen.domain)+i for i in 1..len(f1.gen.codomain)], _
          [i for i in 1..len(f1.gen.domain)]]
        r:= per(coerce [f1.gen.codomain, f1.gen.domain, reindex(f1.gen.data,p) ])^f1.exp * r
      return r

    prod(f:L,g:L):L ==
      r:T := product(f.data,g.data)
      -- dom(f) + cod(f) + dom(g) + cod(g)
      p:List Integer := concat                _
        [[i for i in 1..len(f.domain)],              _
        [len(f.domain)+len(f.codomain)+i for i in 1..len(g.domain)], _
        [len(f.domain)+i for i in 1..len(f.codomain)],        _
        [len(f.domain)+len(g.domain)+len(f.codomain)+i for i in 1..len(g.codomain)]]
        -- dom(f) + dom(g) + cod(f) + cod(g)
      --output("prod p = ",p::OutputForm)$OutputPackage
      [(f.domain)*(g.domain),(f.codomain)*(g.codomain),reindex(r,p)]

    dats(fs:List RR):L ==
      r:L := [1,1,1$T]  -- scalar 1 as tensor
      for y in fs repeat
        t:L:=y.gen
        for n in 1..y.exp repeat
          r:=prod(r,t)
      return r

    dat(f:Rep):L == dats factors f
      
    arity(f:%):ClosedProp % == f::ClosedProp %

    eval(f:%):% == per coerce dat(rep f)

    retractIfCan(f:%):Union(K,"failed") ==
      dom(f)=1 and cod(f)=1 => retract(dat(rep f).data)$T
      return "failed"
    retract(f:%):K ==
      dom(f)=1 and cod(f)=1 => retract(dat(rep f).data)$T
      error "failed"

    -- basis
    basisOut():List % == [per coerce [1,dn(),entries(row(1,i)$SquareMatrix(dim,K))::T] for i in 1..dim]
    basisIn():List % == [per coerce [dn(),1,entries(row(1,i)$SquareMatrix(dim,K))::T] for i in 1..dim]
    ev(n:NNI):% == reduce(_+,[ dx^n * dx^n for dx in basisIn()])$List(%)
    co(n:NNI):% == reduce(_+,[ Dx^n * Dx^n for Dx in basisOut()])$List(%)

    -- manipulation
    map(f:K->K, g:%):% == per coerce [dom g,cod g,unravel(map(f,ravel dat(rep g).data))$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(rep g).data
    unravel(p:ClosedProp %,r:List K):% ==
      dim^(len(dom(p)*cod(p)) pretend NNI) ~= #r => error "failed"
      per coerce [dom(p),cod(p),unravel(r)$T]

    -- sum
    (f:% + g:%):% ==
      dat(rep f).data=0 => g
      dat(rep g).data=0 => f
      dom(f) ~= dom(g) or cod(f) ~= cod(g) => error "arity"
      per coerce [dom f,cod f,dat(rep f).data+dat(rep g).data]

    (f:% - g:%):% ==
      dat(rep f).data=0 => g
      dat(rep g).data=0 => f
      dom(f) ~= dom(f) or cod(g) ~= cod(g) => error "arity"
      per coerce [dom f, cod f,dat(rep f).data-dat(rep g).data]

    _-(f:%):% == per coerce [dom f, cod f,-dat(rep f).data]

    (x:% = y:%):Boolean ==
      if rep x = rep y then true
      else rep eval x = rep eval y

    -- identity for sum (trivial zero map)
    0 == per coerce [1,1,0]
    zero?(f:%):Boolean == dat(rep f).data = 0 * dat(rep f).data
    -- identity for product
    1:% == per 1
    one?(f:%):Boolean == one? rep f
    -- identity for composition
    I := per coerce [dn(),dn(),kroneckerDelta()$T]

    -- permutations and identities
    coerce(p:List Integer):% ==
      r:=I^#p
      --#p = 1 and p.1 = 1 => return r
      p3:List Integer:=concat [ _
        [i for i in 1..#p], _
        [#p+abs(i) for i in p]]
      d:Arity:=dn()^(#p)
      c:Arity := reduce(_*,map((x:Integer):Arity+->(x>0=>dn();up()),p)$LIST2(Integer,Arity))$List(Arity)
      r:=per coerce [d, c, reindex(dat(rep r).data,p3)]
      return r
    coerce(p:List None):% == per coerce [1,1,1]
    -- twist
    X := [2,1]::List Integer::%

    -- product
    elt(f:%,g:%):% == f * g
    elt(f:%,g:Integer):% == f * [g @ Integer]::List Integer::%
    elt(f:%,g1:Integer,g2:Integer):% == f * [g1 @ Integer,g2 @ Integer]::List Integer::%
    elt(f:%,g1:Integer,g2:Integer,g3:Integer):% ==
      f * [g1 @ Integer,g2 @ Integer,g3 @ Integer]::List Integer::%
    apply(f:%,g:%):% == f * g
    -- just free monoid product
    (f:% * g:%):% ==
      -- evaluate scalars
      if f = 1 then return g
      if g = 1 then return f
      if dom(f)=1 and cod(f)=1 then
        if dom(g)=1 and cod(g)=1 then
          per coerce [1,1,coerce(retract(eval f)@K * retract(eval g)@K)]
        else
          per (rep(eval f) * rep g)
      else
        if dom(g)=1 and cod(g)=1 then
          per (rep f * rep(eval g))
        else
          per (rep f * rep g)

    coerce(x:K):% == 1*x

    -- tensor powers
    (f:% ^ p:Arity):% ==
       r:% := 1
       for i in 1..len(p) repeat
         if color(p,i)=dn() then
           r:=r*f
         else
           r:=r*dagger(f)
       return r

    -- returns arity of leading identities
    leadI(x:Rep):Arity ==
      xx := x
      s:Arity:=1
      repeat
        r:=overlap(rep(I),xx)
        output("lead r = ", r::OutputForm)$OutputPackage
        if r.lm=1 and r.mm=rep(I) then
          s := s * dn()
          xx:= r.lm
        else
          r:=overlap(rep(dagger I),xx)
          if r.lm=1 and r.mm=rep(I) then
            s := s * up()
            xx:= r.lm
          else
            break
      return s

    -- returns arity of trailing identities
    trailI(x:Rep):Arity ==
      xx := x
      s:Arity:=1
      repeat
        r:=overlap(xx,rep(I))
        output("trail r = ", r::OutputForm)$OutputPackage
        if r.rm=1 and r.mm=rep(I) then
          s := dn() * s
          xx:= r.rm
        else
          r:=overlap(xx,rep(dagger I))
          if r.rm=1 and r.mm=rep(I) then
            s := up() * s
            xx:= r.rm
          else
            break
      return s

    -- tensor composition:
    compose(lnf:Integer,f:Rep,lfn:Integer, lng:Integer,g:Rep,lgn:Integer):T ==
      output("lnf, lfn, lng, lgn = ", [lnf,lfn,lng,lgn]::List Integer::OutputForm)$OutputPackage
      ldf := len dom(per f)
      lcf := len cod(per f)
      ldg := len dom(per g)
      lcg := len cod(per g)
      --output("ldf, lcf, ldg, lcg = ", [ldf,lcf,ldg,lcg]::List Integer::OutputForm)$OutputPackage
      output("f, g = ", [f,g]::List Rep::OutputForm)$OutputPackage
      -- check for permutations (for now just twists)
      if lcf-lng-lgn=2 then
        if f=rep(X) then
          if g=rep(X) then -- compose permutations
            output("f/g = I*I", 1::OutputForm)$OutputPackage
            return dat(rep(I*I)).data
          else -- twist input
            p:List Integer := concat [ _
              [i for i in 1..lnf], _
              [lnf+2,lnf+1], _
              [lnf+2+i for i in 1..lfn], _
              [lnf+2+lfn+i for i in 1..lcg] ]
            print(p::OutputForm)$OutputForm
            return reindex(dat(g).data,p)
        else if g=rep(X) then -- twist output
          p:List Integer := concat [ _
            [i for i in 1..ldf], _
            [ldf+i for i in 1..lng], _
            [ldf+lng+2,ldf+lng+1], _
            [ldf+lng+2+i for i in 1..lgn] ]
          print(p::OutputForm)$OutputForm
          return reindex(dat(f).data,p)
      r:T := contract(lcf-lng-lgn, dat(f).data,ldf+lng+1, dat(g).data,lnf+1)
      p:List Integer:=concat [ _
        [ldf+lgn+i for i in 1..lnf], _
        [i for i in 1..ldf], _
        [ldf+lnf+lng+i for i in 1..lfn], _
        [ldf+i for i in 1..lng], _
        [ldf+lnf+lng+lfn+lgn+i for i in 1..lcg], _
        [ldf+lng+i for i in 1..lgn] ]
      print(p::OutputForm)$OutputForm
      return reindex(r,p)

    parallelize(f:Rep,g:Rep):Record(f1:Rep,g1:Rep,f2:Rep,g2:Rep) ==
      -- parallelize composition f/g = (f1/g1)*(f2/g2)
      r:Record(f1:Rep,g1:Rep,f2:Rep,g2:Rep):=[1,1,1,1]
      if cod(per f)~=1 then
        i:Integer:=1
        j:Integer:=1
        n:NNI:=1
        m:NNI:=1
        r.f1 := nthFactor(f,1)::Rep
        r.g1 := nthFactor(g,1)::Rep
        --print(r::OutputForm)$OutputForm
        while cod(per r.f1) ~= dom(per r.g1) repeat
          if len(cod per r.f1) < len(dom per r.g1) then
            if n < nthExpon(f,i) then
              n:=n+1
            else
              n:=1
              i:=i+1
            r.f1 := r.f1 * nthFactor(f,i)::Rep
          else if len(cod per r.f1) > len(dom per r.g1) then
            if m < nthExpon(g,j) then
              m:=m+1
            else
              n:=1
              j:=j+1
            r.g1 := r.g1 * nthFactor(g,j)::Rep
          --print([cod(per r.f1)::OutputForm,dom(per r.g1)::OutputForm]::List OutputForm::OutputForm)$OutputForm
        r.f2 := overlap(r.f1, f).rm
        r.g2 := overlap(r.g1, g).rm
      return r

    -- f/g : A^n -> A^p = f:A^n -> A^m / g:A^m -> A^p
    (ff:% / gg:%):% ==
      -- scalars
      if dom(ff)=1 and cod(ff)=1 and dom(gg)=1 and cod(gg)=1 then return ff*gg
      fg:=overlap(cod ff,dom gg)
      if fg.rm~=1 or fg.lm~=1 then
        -- pass extra f inputs on the left
        -- pass extra g outputs on the right
        print(hconcat([message("arity warning: "), _
              over(arity(ff)::OutputForm * arity(I^(fg.rm))::OutputForm, _
                   arity(I^(fg.lm))::OutputForm * arity(gg)::OutputForm) ]))$OutputForm
      r:=parallelize(rep(ff*I^(fg.rm)),rep(I^(fg.lm)*gg))
      -- remove leading and trailing identities
      nf := leadI r.f1
      r.f1 := overlap(rep(I^nf),r.f1).rm
      ng := leadI r.g1
      r.g1 := overlap(rep(I^ng),r.g1).rm
      --output("nf,ng = ",[nf,ng]::List Arity::OutputForm)$OutputPackage
      fn := trailI r.f1
      f := overlap(r.f1,rep(I^fn)).lm
      gn := trailI r.g1
      g := overlap(r.g1,rep(I^gn)).lm
      --output("fn,gn = ",[fn,gn]::List Arity::OutputForm)$OutputPackage
      -- parallel factors guarantees that these are just identities
      if nf~=1 and nf=ng then
        return I^nf*(per(r.f2)/per(r.g2))
      if fn~=1 and gn~=1 then
        return (per(f)/per(g))*I^fn
      return per([nf*dom(per f)*fn, ng*cod(per g)*gn, _
                  compose(len nf,f,len fn, len ng,g,len gn)]::Rep) * _
             (per(r.f2)/per(r.g2))

    -- another notation for composition of products
    (t:Tuple % / x:%):% == t / construct([x])$PrimitiveArray(%)::Tuple(%)
    (x:% / t:Tuple %):% == construct([x])$PrimitiveArray(%)::Tuple(%) / t
    (f:Tuple % / g:Tuple %):% ==
      fs:List % := [select(f,i) for i in 0..length(f)-1]
      gs:List % := [select(g,i) for i in 0..length(g)-1]
      fr:=reduce(elt@(%,%)->%,fs,1)
      gr:=reduce(elt@(%,%)->%,gs,1)
      fr / gr

    (x:K * y:%):% == per coerce [dom y, cod y,x*dat(rep y).data]
    (x:% * y:K):% == per coerce [dom x,cod x,dat(rep x).data*y]
    (x:Integer * y:%):% == per coerce [dom y,cod y,x*dat(rep y).data]

    -- display operators using basis
    show(x:%):OutputForm ==
      dom(x)=1 and cod(x)=1 => return (dat(rep x).data)::OutputForm
      gens:List OutputForm:=[index(i::PositiveInteger)$gener::OutputForm for i in 1..dim]
      -- input basis
      inps:List OutputForm := list empty()
      dx:=dom(x)
      for i in 1..len(dx) repeat
        --empty? inps => inps:=gens
        inps:=concat [[(inps.k * (color(dx,i)=dn()=>gens.j;super(gens.j,message "*"))) _
          for j in 1..dim] for k in 1..#inps]
      -- output basis
      outs:List OutputForm := list empty()
      cx:=cod(x)
      for i in 1..len(cx) repeat
        --empty? outs => outs:=gens
        outs:=concat [[(outs.k * (color(cx,i)=dn()=>gens.j;super(gens.j,message "*"))) _
          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]
      else
        bases:List OutputForm:= []
      -- merge bases with data to form term list
      terms:=[(k=1 => base;k::OutputForm*base)
        for base in bases for k in ravel(x) | k~=0]
      empty? terms => return 0::OutputForm
      -- combine the terms
      return reduce(_+,terms)

    coerce(x:%):OutputForm ==
      r:OutputForm := empty()
      for y in factors(rep x) repeat
        if y.exp = 1 then
          if size rep x = 1 then
            r := show per coerce y.gen
          else
            r:=r*paren(list show per coerce y.gen)
        else
          r:=r*paren(list show per coerce y.gen)^(y.exp::OutputForm)
      return r
\end{spad}

<A NAME="getting_started">Getting Started</A>

  Consult the source code <a href="#source_code">above</a> for more details.

Convenient Notation
\begin{axiom}
-- summation
macro Σ(f,i,b) == reduce(+,[f*b.i for i in 1..#b])
-- list comprehension
macro Ξ(f,i)==[f for i in 1..retract(dimension()$L)]
\end{axiom}

Example
\begin{axiom}
Q := EXPR INT
L := CLOP(OVAR ['x,'y],Q)
)show L
\end{axiom}

Basis
\begin{axiom}
dim:Integer:=retract dimension()$L
Dx:=basisOut()$L
dx:=basisIn()$L
matrix Ξ(Ξ( eval(dx.i * Dx.j), i),j)
matrix Ξ(Ξ( Dx.i / dx.j, i),j)
\end{axiom}

(1,1)-tensor
\begin{axiom}
A:L := Σ( Σ( script(a,[[j],[i]]), i,Dx), j,dx)
a:=arity(A)
p:=dom(A)
\end{axiom}
scalar
\begin{axiom}
s:= 3::L
arity s
2*s
s*2
\end{axiom}

Powers
\begin{axiom}
A^p
a^p
\end{axiom}

\begin{axiom}
s/A
A/s
3*A
A/3
\end{axiom}
identities
\begin{axiom}
I:L := [1]
I*I
arity(I*I)
I/I
H:L:=[1,2]
arity(H)
eval(I*I)
arity eval(I*I)
test( I*I = H )
-- twist
X:L := [2,1]
test(X/X=H)
test(X/H=X)
test(H/X=X)
-- printing
I*X*X*I
(I*X*X*I)/(X*I*I*X)
-- trace
U:L:=ev(1)
Ω:L:=co(1)
Ω/U
test
  ( I Ω  ) /
  (  U I ) = I
test
  (  Ω I ) /
  ( I U  ) = I
\end{axiom}

Back to the <a href="#source_code">top</a>.

<a name="comments">Comments</a>

  Please leave comments and suggestions.

  Thanks

  Bill Page

Introduction

Bi-graded two-color linear operators (transformations) over a finite n-dimensional vector space, including products and duals on a field . Members of this domain are morphisms $K^{\pm^n} \to K^{\pm^m},$ where $K^{+}=K,$ $K^{++}=A\otimes A,$ and $K^{-}=K^<em>,$ (dual), etc. Products, permutations and composition (grafting) of morphisms are implemented. Operators are represented internally as tensors.

Operator composition and products can be visualized by oriented directed graphs. The graphs have a top and a bottom and arrows are directed either downwards or upwards.

External vertices in this graph represent vectors, tensors and their duals. Internal nodes and arcs (edges) represent linear operators. Edges may be one of two different "colors" (labelled + and - in the code that follows) or marked with arrows directed either downwards (+) or upwards (-). Horizontal juxtaposition (i.e. a horizontal cross-section) represents tensor product. Vertical juxtaposition of edges of the same color represents operator composition.

See examples and documentation below

I would be glad if 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.

Source Code

We try to start by defining the concept of a compact closed category.

Ref:

spad

)abbrev domain ARITY Arity
Arity():  Exports == Implementation where
  COLOR ==> OrderedVariableList ['_+,'_-]
  LIST2 ==> ListFunctions2
  NNI ==> NonNegativeInteger
  RS ==> Record(gen:COLOR,exp:NNI)

  Exports ==> Join(Monoid, RetractableTo COLOR) with
    index: PositiveInteger -> %
    dn: () -> %
      ++ default
    up: () -> %
      ++ dual
    0: %
      ++ use 0 for identity
    "+": (%,%) -> %
      ++ composition
    size: % -> NonNegativeInteger
    len: % -> Integer
    color: (%,NNI) -> %
    overlap: (%,%) -> Record(lm:%, mm:%, rm:%)
  Implementation ==> FreeMonoid COLOR add
    Rep == FreeMonoid COLOR
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %
    index(x:PositiveInteger):% == per(index(x)$COLOR ::Rep)
    up():% == index(2)
    dn():% == index(1)
    0:% == per 1
    (f:% + g:%):% == per(rep f * rep g)
    coerce(x:%):OutputForm == (rep(x)=1 => message "0";rep(x)::OutputForm)
    -- size of FreeMonoid is just number of factors
    -- len is total length
    len(f:%):Integer ==
      reduce(_+,map(x+->x.exp,factors rep f)$LIST2(RS,NNI),0)$List(NNI) pretend Integer
    -- i'th element
    color(f:%,i:NNI):% ==
      j:NNI:=0
      for x in factors rep f repeat
        j:=j+x.exp
        if j>=i then
          return per coerce x.gen
      error "index error"

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/3593414395608860020-25px001.spad using 
      old system compiler.
   ARITY abbreviates domain Arity 
------------------------------------------------------------------------
   initializing NRLIB ARITY for Arity 
   compiling into NRLIB ARITY 
   compiling local rep : $ -> FreeMonoid OrderedVariableList construct(QUOTE +,QUOTE -)
      ARITY;rep is replaced by x 
Time: 0.10 SEC.

   compiling local per : FreeMonoid OrderedVariableList construct(QUOTE +,QUOTE -) -> $
      ARITY;per is replaced by x 
Time: 0.01 SEC.

   compiling exported index : PositiveInteger -> $
Time: 0.02 SEC.

   compiling exported up : () -> $
Time: 0 SEC.

   compiling exported dn : () -> $
Time: 0.01 SEC.

   compiling local Zero : () -> $
Time: 0.01 SEC.

   compiling exported + : ($,$) -> $
Time: 0 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0.02 SEC.

   compiling exported len : $ -> Integer
Time: 0.15 SEC.

   compiling exported color : ($,NonNegativeInteger) -> $
Time: 0.24 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |Arity| REDEFINED

;;;     ***       |Arity| REDEFINED
Time: 0.01 SEC.

   Warnings: 
      [1] len: pretend(Integer) -- should replace by @

   Cumulative Statistics for Constructor Arity
      Time: 0.57 seconds

--------------non extending category----------------------
.. Arity of cat 
(|Join| (|Monoid|)
        (|RetractableTo| (|OrderedVariableList| (|construct| '+ '-)))
        (CATEGORY |domain| (SIGNATURE |index| ($ (|PositiveInteger|)))
         (SIGNATURE |dn| ($)) (SIGNATURE |up| ($)) NIL (SIGNATURE + ($ $ $))
         (SIGNATURE |size| ((|NonNegativeInteger|) $))
         (SIGNATURE |len| ((|Integer|) $))
         (SIGNATURE |color| ($ $ (|NonNegativeInteger|)))
         (SIGNATURE |overlap|
          ((|Record| (|:| |lm| $) (|:| |mm| $) (|:| |rm| $)) $ $))))   has no 
(|RetractableTo| (|OrderedVariableList| (|construct| + -)))    finalizing NRLIB ARITY 
   Processing Arity for Browser database:
--->-->Arity((index (% (PositiveInteger)))): Not documented!!!!
--------(dn (%))---------
--------(up (%))---------
-----------------
--->-->Arity(): Improper first word in comments: use
"use 0 for identity"
--------(+ (% % %))---------
--->-->Arity((size ((NonNegativeInteger) %))): Not documented!!!!
--->-->Arity((len ((Integer) %))): Not documented!!!!
--->-->Arity((color (% % NNI))): Not documented!!!!
--->-->Arity((overlap ((Record (: lm %) (: mm %) (: rm %)) % %))): Not documented!!!!
--->-->Arity(constructor): Not documented!!!!
--->-->Arity(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/ARITY.NRLIB/ARITY.lsp" (written 31 MAY 2011 06:56:12 PM):

; /var/zope2/var/LatexWiki/ARITY.NRLIB/ARITY.fasl written
; compilation finished in 0:00:00.239
------------------------------------------------------------------------
   Arity is now explicitly exposed in frame initial 
   Arity will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/ARITY.NRLIB/ARITY

   >> 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

spad

)abbrev category CMONAL ClosedMonoidal
ClosedMonoidal():Category == Ring with
    dom: % -> Arity
      ++ domain
    cod: % -> Arity
      ++ co-domain
    _/: (%,%) -> %
      ++ vertical composition f/g
    apply: (%,%) -> %
      ++ horizontal product f g = f*g
    "^": (%,Arity) -> %
      ++ colored power
    dagger: % -> %
      ++ reverse arrows:
      ++ cod f = dom dagger f
      ++ dom f = cod dagger f

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/7854049118560040482-25px002.spad using 
      old system compiler.
   CMONAL abbreviates category ClosedMonoidal 
------------------------------------------------------------------------
   initializing NRLIB CMONAL for ClosedMonoidal 
   compiling into NRLIB CMONAL 

;;;     ***       |ClosedMonoidal| REDEFINED
Time: 0.03 SEC.

   finalizing NRLIB CMONAL 
   Processing ClosedMonoidal for Browser database:
--------(dom ((Arity) %))---------
--------(cod ((Arity) %))---------
--------(/ (% % %))---------
--->-->ClosedMonoidal((/ (% % %))): Improper first word in comments: vertical
"vertical composition \\spad{f/g}"
--------(apply (% % %))---------
--->-->ClosedMonoidal((apply (% % %))): Improper first word in comments: horizontal
"horizontal product \\spad{f} \\spad{g} = \\spad{f*g}"
--------(^ (% % (Arity)))---------
--------(dagger (% %))---------
--->-->ClosedMonoidal(constructor): Not documented!!!!
--->-->ClosedMonoidal(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/CMONAL.NRLIB/CMONAL.lsp" (written 31 MAY 2011 06:56:12 PM):

; /var/zope2/var/LatexWiki/CMONAL.NRLIB/CMONAL.fasl written
; compilation finished in 0:00:00.027
------------------------------------------------------------------------
   ClosedMonoidal is now explicitly exposed in frame initial 
   ClosedMonoidal will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/CMONAL.NRLIB/CMONAL

   >> 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 ClosedProp? (Products and Permutations). The ClosedProp? domain represents everything that is "constant" about all the domains in this category. It can be defined as an endofunctor with only the information available about the category itself.

spad

)abbrev domain CPROP ClosedProp
ClosedProp(L:ClosedMonoidal): Exports == Implementation where

  Exports ==> ClosedMonoidal with
    coerce: L -> %

  Implementation ==> add
    Rep == Record(domain:Arity, codomain:Arity)
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %

    coerce(f:%):OutputForm == dom(f)::OutputForm / cod(f)::OutputForm

    coerce(f:L):% == per [dom f, cod f]                    -- coerce(f:L):% == per f

    dom(x:%):Arity == rep(x).domain                          -- dom(x:%):NNI == dom rep x
    cod(x:%):Arity == rep(x).codomain                        -- cod(x:%):NNI == cod rep x
    --0:% == per [1,1]                                       -- 0:% == per 0
    1:% == per [1,1]                                       -- 1:% == per 1
    -- evaluation
    (f:% / g:%):% == per [dom f, cod g]                    -- (f:% / g:%):% == per (rep f / rep g)
    -- product
    apply(f:%,g:%):% == per [dom f * dom g, cod f * cod g] -- apply(f:%,g:%):% == per apply(rep f,rep g)
    (f:% * g:%):% == per [dom f * dom g, cod f * cod g]    --(f:% * g:%):% == per (rep f * rep g)
    -- sum
    --(f:% + g:%):% == per [dom f, cod f]                    --(f:% + g:%):% == per (rep f + rep g)
    dagger(f:%):% == per [cod f, dom f]
    (f:% ^ p:Arity):% ==
       r:% := 1
       for i in 1..len(p) repeat
         if color(p,i)=dn() then
           r:=r*f
         else
           r:=r*dagger(f)
       return r

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/7228414894644034724-25px003.spad using 
      old system compiler.
   CPROP abbreviates domain ClosedProp 
------------------------------------------------------------------------
   initializing NRLIB CPROP for ClosedProp 
   compiling into NRLIB CPROP 
   compiling local rep : $ -> Record(domain: Arity,codomain: Arity)
      CPROP;rep is replaced by x 
Time: 0.04 SEC.

   compiling local per : Record(domain: Arity,codomain: Arity) -> $
      CPROP;per is replaced by x 
Time: 0 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0 SEC.

   compiling exported coerce : L -> $
Time: 0.01 SEC.

   compiling exported dom : $ -> Arity
Time: 0 SEC.

   compiling exported cod : $ -> Arity
Time: 0 SEC.

   compiling exported One : () -> $
Time: 0 SEC.

   compiling exported / : ($,$) -> $
Time: 0.01 SEC.

   compiling exported apply : ($,$) -> $
Time: 0 SEC.

   compiling exported * : ($,$) -> $
Time: 0 SEC.

   compiling exported dagger : $ -> $
Time: 0 SEC.

   compiling exported ^ : ($,Arity) -> $
Time: 0.02 SEC.

(time taken in buildFunctor:  10)

;;;     ***       |ClosedProp| REDEFINED

;;;     ***       |ClosedProp| REDEFINED
Time: 0.01 SEC.

   Cumulative Statistics for Constructor ClosedProp
      Time: 0.09 seconds

   finalizing NRLIB CPROP 
   Processing ClosedProp for Browser database:
--->-->ClosedProp((coerce (% L))): Not documented!!!!
--->-->ClosedProp(constructor): Not documented!!!!
--->-->ClosedProp(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/CPROP.NRLIB/CPROP.lsp" (written 31 MAY 2011 06:56:13 PM):

; /var/zope2/var/LatexWiki/CPROP.NRLIB/CPROP.fasl written
; compilation finished in 0:00:00.482
------------------------------------------------------------------------
   ClosedProp is now explicitly exposed in frame initial 
   ClosedProp will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/CPROP.NRLIB/CPROP

   >> 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 ClosedLinearOperator? domain is ClosedMonoidal? over FreeMonoid? OrderedVariables? ['_+,'_-]?, i.e. strings of $\pm$ symbols. The objects of this domain are all tensor powers of a vector space of fixed dimension. The arrows are linear operators that map from one object (tensor powers of vector space and it's dual) to another such power.

Ref: http://en.wikipedia.org/wiki/Category_of_vector_spaces

all members of this domain have the same dimension

Faster tensors

axiom

)lib CARTEN

   CartesianTensor is now explicitly exposed in frame initial 
   CartesianTensor will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/CARTEN.NRLIB/CARTEN

spad

)abbrev domain CLOP ClosedLinearOperator
ClosedLinearOperator(gener:OrderedFinite,K:Field): Exports == Implementation where
  NNI ==> NonNegativeInteger
  Exports ==> Join(Ring, VectorSpace K, ClosedMonoidal, RetractableTo K) with
    arity: % -> ClosedProp %
    basisOut: () -> List %
    basisIn: () -> List %
    map: (K->K,%) -> %
    if K has Evalable(K) then Evalable(K)
    eval: % -> %
    ravel: % -> List K
    unravel: (ClosedProp %,List K) -> %
    coerce:(x:List Integer) -> %
      ++ identity for composition and permutations of its products
    coerce:(x:List None) -> %
      ++ [] = 1
    elt: (%,%) -> %
    elt: (%,Integer) -> %
    elt: (%,Integer,Integer) -> %
    elt: (%,Integer,Integer,Integer) -> %
    _/: (Tuple %,Tuple %) -> %
    _/: (Tuple %,%) -> %
    _/: (%,Tuple %) -> %
      ++ yet another syntax for product
    ev: NNI -> %
      ++ (2,0)-tensor for evaluation
    co: NNI -> %
      ++ (0,2)-tensor for co-evaluation
  Implementation ==> add

    LIST2 ==> ListFunctions2
    dim:NNI := size()$gener
    T := CartesianTensor(1,dim,K)
    L := Record(domain:Arity, codomain:Arity, data:T)
    RR := Record(gen:L,exp:NNI)
    -- FreeMonoid provides unevaluated products
    Rep == FreeMonoid L
    rep(x:%):Rep == x pretend Rep
    per(x:Rep):% == x pretend %
    dimension():CardinalNumber == coerce dim

    -- Prop (arity)
    dom(f:%):Arity ==
      reduce(_*,map(x+->(x.gen.domain)^(x.exp),factors rep f)$LIST2(RR,Arity),1)$List(Arity)
    cod(f:%):Arity ==
      reduce(_*,map(x+->(x.gen.codomain)^(x.exp),factors rep f)$LIST2(RR,Arity),1)$List(Arity)
    dagger(f:%):% ==
      r:=1
      for f1 in factors rep f repeat
        p:List Integer := concat [ _
          [len(f1.gen.domain)+i for i in 1..len(f1.gen.codomain)], _
          [i for i in 1..len(f1.gen.domain)]]
        r:= per(coerce [f1.gen.codomain, f1.gen.domain, reindex(f1.gen.data,p) ])^f1.exp * r
      return r

    prod(f:L,g:L):L ==
      r:T := product(f.data,g.data)
      -- dom(f) + cod(f) + dom(g) + cod(g)
      p:List Integer := concat                _
        [[i for i in 1..len(f.domain)],              _
        [len(f.domain)+len(f.codomain)+i for i in 1..len(g.domain)], _
        [len(f.domain)+i for i in 1..len(f.codomain)],        _
        [len(f.domain)+len(g.domain)+len(f.codomain)+i for i in 1..len(g.codomain)]]
        -- dom(f) + dom(g) + cod(f) + cod(g)
      --output("prod p = ",p::OutputForm)$OutputPackage
      [(f.domain)*(g.domain),(f.codomain)*(g.codomain),reindex(r,p)]

    dats(fs:List RR):L ==
      r:L := [1,1,1$T]  -- scalar 1 as tensor
      for y in fs repeat
        t:L:=y.gen
        for n in 1..y.exp repeat
          r:=prod(r,t)
      return r

    dat(f:Rep):L == dats factors f

    arity(f:%):ClosedProp % == f::ClosedProp %

    eval(f:%):% == per coerce dat(rep f)

    retractIfCan(f:%):Union(K,"failed") ==
      dom(f)=1 and cod(f)=1 => retract(dat(rep f).data)$T
      return "failed"
    retract(f:%):K ==
      dom(f)=1 and cod(f)=1 => retract(dat(rep f).data)$T
      error "failed"

    -- basis
    basisOut():List % == [per coerce [1,dn(),entries(row(1,i)$SquareMatrix(dim,K))::T] for i in 1..dim]
    basisIn():List % == [per coerce [dn(),1,entries(row(1,i)$SquareMatrix(dim,K))::T] for i in 1..dim]
    ev(n:NNI):% == reduce(_+,[ dx^n * dx^n for dx in basisIn()])$List(%)
    co(n:NNI):% == reduce(_+,[ Dx^n * Dx^n for Dx in basisOut()])$List(%)

    -- manipulation
    map(f:K->K, g:%):% == per coerce [dom g,cod g,unravel(map(f,ravel dat(rep g).data))$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(rep g).data
    unravel(p:ClosedProp %,r:List K):% ==
      dim^(len(dom(p)*cod(p)) pretend NNI) ~= #r => error "failed"
      per coerce [dom(p),cod(p),unravel(r)$T]

    -- sum
    (f:% + g:%):% ==
      dat(rep f).data=0 => g
      dat(rep g).data=0 => f
      dom(f) ~= dom(g) or cod(f) ~= cod(g) => error "arity"
      per coerce [dom f,cod f,dat(rep f).data+dat(rep g).data]

    (f:% - g:%):% ==
      dat(rep f).data=0 => g
      dat(rep g).data=0 => f
      dom(f) ~= dom(f) or cod(g) ~= cod(g) => error "arity"
      per coerce [dom f, cod f,dat(rep f).data-dat(rep g).data]

    _-(f:%):% == per coerce [dom f, cod f,-dat(rep f).data]

    (x:% = y:%):Boolean ==
      if rep x = rep y then true
      else rep eval x = rep eval y

    -- identity for sum (trivial zero map)
    0 == per coerce [1,1,0]
    zero?(f:%):Boolean == dat(rep f).data = 0 * dat(rep f).data
    -- identity for product
    1:% == per 1
    one?(f:%):Boolean == one? rep f
    -- identity for composition
    I := per coerce [dn(),dn(),kroneckerDelta()$T]

    -- permutations and identities
    coerce(p:List Integer):% ==
      r:=I^#p
      --#p = 1 and p.1 = 1 => return r
      p3:List Integer:=concat [ _
        [i for i in 1..#p], _
        [#p+abs(i) for i in p]]
      d:Arity:=dn()^(#p)
      c:Arity := reduce(_*,map((x:Integer):Arity+->(x>0=>dn();up()),p)$LIST2(Integer,Arity))$List(Arity)
      r:=per coerce [d, c, reindex(dat(rep r).data,p3)]
      return r
    coerce(p:List None):% == per coerce [1,1,1]
    -- twist
    X := [2,1]::List Integer::%

    -- product
    elt(f:%,g:%):% == f * g
    elt(f:%,g:Integer):% == f * [g @ Integer]::List Integer::%
    elt(f:%,g1:Integer,g2:Integer):% == f * [g1 @ Integer,g2 @ Integer]::List Integer::%
    elt(f:%,g1:Integer,g2:Integer,g3:Integer):% ==
      f * [g1 @ Integer,g2 @ Integer,g3 @ Integer]::List Integer::%
    apply(f:%,g:%):% == f * g
    -- just free monoid product
    (f:% * g:%):% ==
      -- evaluate scalars
      if f = 1 then return g
      if g = 1 then return f
      if dom(f)=1 and cod(f)=1 then
        if dom(g)=1 and cod(g)=1 then
          per coerce [1,1,coerce(retract(eval f)@K * retract(eval g)@K)]
        else
          per (rep(eval f) * rep g)
      else
        if dom(g)=1 and cod(g)=1 then
          per (rep f * rep(eval g))
        else
          per (rep f * rep g)

    coerce(x:K):% == 1*x

    -- tensor powers
    (f:% ^ p:Arity):% ==
       r:% := 1
       for i in 1..len(p) repeat
         if color(p,i)=dn() then
           r:=r*f
         else
           r:=r*dagger(f)
       return r

    -- returns arity of leading identities
    leadI(x:Rep):Arity ==
      xx := x
      s:Arity:=1
      repeat
        r:=overlap(rep(I),xx)
        output("lead r = ", r::OutputForm)$OutputPackage
        if r.lm=1 and r.mm=rep(I) then
          s := s * dn()
          xx:= r.lm
        else
          r:=overlap(rep(dagger I),xx)
          if r.lm=1 and r.mm=rep(I) then
            s := s * up()
            xx:= r.lm
          else
            break
      return s

    -- returns arity of trailing identities
    trailI(x:Rep):Arity ==
      xx := x
      s:Arity:=1
      repeat
        r:=overlap(xx,rep(I))
        output("trail r = ", r::OutputForm)$OutputPackage
        if r.rm=1 and r.mm=rep(I) then
          s := dn() * s
          xx:= r.rm
        else
          r:=overlap(xx,rep(dagger I))
          if r.rm=1 and r.mm=rep(I) then
            s := up() * s
            xx:= r.rm
          else
            break
      return s

    -- tensor composition:
    compose(lnf:Integer,f:Rep,lfn:Integer, lng:Integer,g:Rep,lgn:Integer):T ==
      output("lnf, lfn, lng, lgn = ", [lnf,lfn,lng,lgn]::List Integer::OutputForm)$OutputPackage
      ldf := len dom(per f)
      lcf := len cod(per f)
      ldg := len dom(per g)
      lcg := len cod(per g)
      --output("ldf, lcf, ldg, lcg = ", [ldf,lcf,ldg,lcg]::List Integer::OutputForm)$OutputPackage
      output("f, g = ", [f,g]::List Rep::OutputForm)$OutputPackage
      -- check for permutations (for now just twists)
      if lcf-lng-lgn=2 then
        if f=rep(X) then
          if g=rep(X) then -- compose permutations
            output("f/g = I*I", 1::OutputForm)$OutputPackage
            return dat(rep(I*I)).data
          else -- twist input
            p:List Integer := concat [ _
              [i for i in 1..lnf], _
              [lnf+2,lnf+1], _
              [lnf+2+i for i in 1..lfn], _
              [lnf+2+lfn+i for i in 1..lcg] ]
            print(p::OutputForm)$OutputForm
            return reindex(dat(g).data,p)
        else if g=rep(X) then -- twist output
          p:List Integer := concat [ _
            [i for i in 1..ldf], _
            [ldf+i for i in 1..lng], _
            [ldf+lng+2,ldf+lng+1], _
            [ldf+lng+2+i for i in 1..lgn] ]
          print(p::OutputForm)$OutputForm
          return reindex(dat(f).data,p)
      r:T := contract(lcf-lng-lgn, dat(f).data,ldf+lng+1, dat(g).data,lnf+1)
      p:List Integer:=concat [ _
        [ldf+lgn+i for i in 1..lnf], _
        [i for i in 1..ldf], _
        [ldf+lnf+lng+i for i in 1..lfn], _
        [ldf+i for i in 1..lng], _
        [ldf+lnf+lng+lfn+lgn+i for i in 1..lcg], _
        [ldf+lng+i for i in 1..lgn] ]
      print(p::OutputForm)$OutputForm
      return reindex(r,p)

    parallelize(f:Rep,g:Rep):Record(f1:Rep,g1:Rep,f2:Rep,g2:Rep) ==
      -- parallelize composition f/g = (f1/g1)*(f2/g2)
      r:Record(f1:Rep,g1:Rep,f2:Rep,g2:Rep):=[1,1,1,1]
      if cod(per f)~=1 then
        i:Integer:=1
        j:Integer:=1
        n:NNI:=1
        m:NNI:=1
        r.f1 := nthFactor(f,1)::Rep
        r.g1 := nthFactor(g,1)::Rep
        --print(r::OutputForm)$OutputForm
        while cod(per r.f1) ~= dom(per r.g1) repeat
          if len(cod per r.f1) < len(dom per r.g1) then
            if n < nthExpon(f,i) then
              n:=n+1
            else
              n:=1
              i:=i+1
            r.f1 := r.f1 * nthFactor(f,i)::Rep
          else if len(cod per r.f1) > len(dom per r.g1) then
            if m < nthExpon(g,j) then
              m:=m+1
            else
              n:=1
              j:=j+1
            r.g1 := r.g1 * nthFactor(g,j)::Rep
          --print([cod(per r.f1)::OutputForm,dom(per r.g1)::OutputForm]::List OutputForm::OutputForm)$OutputForm
        r.f2 := overlap(r.f1, f).rm
        r.g2 := overlap(r.g1, g).rm
      return r

    -- f/g : A^n -> A^p = f:A^n -> A^m / g:A^m -> A^p
    (ff:% / gg:%):% ==
      -- scalars
      if dom(ff)=1 and cod(ff)=1 and dom(gg)=1 and cod(gg)=1 then return ff*gg
      fg:=overlap(cod ff,dom gg)
      if fg.rm~=1 or fg.lm~=1 then
        -- pass extra f inputs on the left
        -- pass extra g outputs on the right
        print(hconcat([message("arity warning: "), _
              over(arity(ff)::OutputForm * arity(I^(fg.rm))::OutputForm, _
                   arity(I^(fg.lm))::OutputForm * arity(gg)::OutputForm) ]))$OutputForm
      r:=parallelize(rep(ff*I^(fg.rm)),rep(I^(fg.lm)*gg))
      -- remove leading and trailing identities
      nf := leadI r.f1
      r.f1 := overlap(rep(I^nf),r.f1).rm
      ng := leadI r.g1
      r.g1 := overlap(rep(I^ng),r.g1).rm
      --output("nf,ng = ",[nf,ng]::List Arity::OutputForm)$OutputPackage
      fn := trailI r.f1
      f := overlap(r.f1,rep(I^fn)).lm
      gn := trailI r.g1
      g := overlap(r.g1,rep(I^gn)).lm
      --output("fn,gn = ",[fn,gn]::List Arity::OutputForm)$OutputPackage
      -- parallel factors guarantees that these are just identities
      if nf~=1 and nf=ng then
        return I^nf*(per(r.f2)/per(r.g2))
      if fn~=1 and gn~=1 then
        return (per(f)/per(g))*I^fn
      return per([nf*dom(per f)*fn, ng*cod(per g)*gn, _
                  compose(len nf,f,len fn, len ng,g,len gn)]::Rep) * _
             (per(r.f2)/per(r.g2))

    -- another notation for composition of products
    (t:Tuple % / x:%):% == t / construct([x])$PrimitiveArray(%)::Tuple(%)
    (x:% / t:Tuple %):% == construct([x])$PrimitiveArray(%)::Tuple(%) / t
    (f:Tuple % / g:Tuple %):% ==
      fs:List % := [select(f,i) for i in 0..length(f)-1]
      gs:List % := [select(g,i) for i in 0..length(g)-1]
      fr:=reduce(elt@(%,%)->%,fs,1)
      gr:=reduce(elt@(%,%)->%,gs,1)
      fr / gr

    (x:K * y:%):% == per coerce [dom y, cod y,x*dat(rep y).data]
    (x:% * y:K):% == per coerce [dom x,cod x,dat(rep x).data*y]
    (x:Integer * y:%):% == per coerce [dom y,cod y,x*dat(rep y).data]

    -- display operators using basis
    show(x:%):OutputForm ==
      dom(x)=1 and cod(x)=1 => return (dat(rep x).data)::OutputForm
      gens:List OutputForm:=[index(i::PositiveInteger)$gener::OutputForm for i in 1..dim]
      -- input basis
      inps:List OutputForm := list empty()
      dx:=dom(x)
      for i in 1..len(dx) repeat
        --empty? inps => inps:=gens
        inps:=concat [[(inps.k * (color(dx,i)=dn()=>gens.j;super(gens.j,message "*"))) _
          for j in 1..dim] for k in 1..#inps]
      -- output basis
      outs:List OutputForm := list empty()
      cx:=cod(x)
      for i in 1..len(cx) repeat
        --empty? outs => outs:=gens
        outs:=concat [[(outs.k * (color(cx,i)=dn()=>gens.j;super(gens.j,message "*"))) _
          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]
      else
        bases:List OutputForm:= []
      -- merge bases with data to form term list
      terms:=[(k=1 => base;k::OutputForm*base)
        for base in bases for k in ravel(x) | k~=0]
      empty? terms => return 0::OutputForm
      -- combine the terms
      return reduce(_+,terms)

    coerce(x:%):OutputForm ==
      r:OutputForm := empty()
      for y in factors(rep x) repeat
        if y.exp = 1 then
          if size rep x = 1 then
            r := show per coerce y.gen
          else
            r:=r*paren(list show per coerce y.gen)
        else
          r:=r*paren(list show per coerce y.gen)^(y.exp::OutputForm)
      return r

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/6630313653435219433-25px005.spad using 
      old system compiler.
   CLOP abbreviates domain ClosedLinearOperator 
------------------------------------------------------------------------
   initializing NRLIB CLOP for ClosedLinearOperator 
   compiling into NRLIB CLOP 
   processing macro definition LIST2 ==> ListFunctions2 
   compiling local rep : $ -> FreeMonoid L
      CLOP;rep is replaced by x 
Time: 0.21 SEC.

   compiling local per : FreeMonoid L -> $
      CLOP;per is replaced by x 
Time: 0 SEC.

   compiling exported dimension : () -> CardinalNumber
Time: 0 SEC.

   compiling exported dom : $ -> Arity
Time: 0.02 SEC.

   compiling exported cod : $ -> Arity
Time: 0.02 SEC.

   compiling exported dagger : $ -> $
Time: 5.94 SEC.

   compiling local prod : (L,L) -> L
Time: 0.02 SEC.

   compiling local dats : List RR -> L
Time: 0.01 SEC.

   compiling local dat : FreeMonoid L -> L
Time: 0 SEC.

   compiling exported arity : $ -> ClosedProp $
Time: 0.01 SEC.

   compiling exported eval : $ -> $
Time: 0 SEC.

   compiling exported retractIfCan : $ -> Union(K,failed)
Time: 0.01 SEC.

   compiling exported retract : $ -> K
Time: 0.01 SEC.

   compiling exported basisOut : () -> List $
Time: 0.02 SEC.

   compiling exported basisIn : () -> List $
Time: 0.02 SEC.

   compiling exported ev : NonNegativeInteger -> $
Time: 0.11 SEC.

   compiling exported co : NonNegativeInteger -> $
Time: 0.01 SEC.

   compiling exported map : (K -> K,$) -> $
Time: 0 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 SEC.

   compiling exported unravel : (ClosedProp $,List K) -> $
Time: 0.10 SEC.

   compiling exported + : ($,$) -> $
Time: 0.02 SEC.

   compiling exported - : ($,$) -> $
Time: 0.02 SEC.

   compiling exported - : $ -> $
Time: 0 SEC.

   compiling exported = : ($,$) -> Boolean
Time: 0.01 SEC.

   compiling exported Zero : () -> $
Time: 0 SEC.

   compiling exported zero? : $ -> Boolean
Time: 0 SEC.

   compiling exported One : () -> $
Time: 0 SEC.

   compiling exported one? : $ -> Boolean
Time: 0 SEC.

   compiling exported coerce : List Integer -> $
Time: 0.02 SEC.

   compiling exported coerce : List None -> $
Time: 0.01 SEC.

   compiling exported elt : ($,$) -> $
Time: 0 SEC.

   compiling exported elt : ($,Integer) -> $
Time: 0 SEC.

   compiling exported elt : ($,Integer,Integer) -> $
Time: 0 SEC.

   compiling exported elt : ($,Integer,Integer,Integer) -> $
Time: 0 SEC.

   compiling exported apply : ($,$) -> $
Time: 0 SEC.

   compiling exported * : ($,$) -> $
Time: 0.34 SEC.

   compiling exported coerce : K -> $
Time: 0 SEC.

   compiling exported ^ : ($,Arity) -> $
Time: 0.01 SEC.

   compiling local leadI : FreeMonoid L -> Arity
Time: 0.09 SEC.

   compiling local trailI : FreeMonoid L -> Arity
Time: 0.09 SEC.

   compiling local compose : (Integer,FreeMonoid L,Integer,Integer,FreeMonoid L,Integer) -> T$
Time: 0.35 SEC.

   compiling local parallelize : (FreeMonoid L,FreeMonoid L) -> Record(f1: FreeMonoid L,g1: FreeMonoid L,f2: FreeMonoid L,g2: FreeMonoid L)
Time: 0.03 SEC.

   compiling exported / : ($,$) -> $
Time: 2.97 SEC.

   compiling exported / : (Tuple $,$) -> $
Time: 0.03 SEC.

   compiling exported / : ($,Tuple $) -> $
Time: 0.01 SEC.

   compiling exported / : (Tuple $,Tuple $) -> $
Time: 0.03 SEC.

   compiling exported * : (K,$) -> $
Time: 0 SEC.

   compiling exported * : ($,K) -> $
Time: 0 SEC.

   compiling exported * : (Integer,$) -> $
Time: 0.01 SEC.

   compiling local show : $ -> OutputForm
Time: 0.28 SEC.

   compiling exported coerce : $ -> OutputForm
Time: 0.06 SEC.

****** Domain: K already in scope
augmenting K: (Evalable K)
(time taken in buildFunctor:  10)

;;;     ***       |ClosedLinearOperator| REDEFINED

;;;     ***       |ClosedLinearOperator| REDEFINED
Time: 0.03 SEC.

   Warnings: 
      [1] parallelize:  i has no value
      [2] parallelize:  j has no value

   Cumulative Statistics for Constructor ClosedLinearOperator
      Time: 10.93 seconds

   finalizing NRLIB CLOP 
   Processing ClosedLinearOperator for Browser database:
--->-->ClosedLinearOperator((arity ((ClosedProp %) %))): Not documented!!!!
--->-->ClosedLinearOperator((basisOut ((List %)))): Not documented!!!!
--->-->ClosedLinearOperator((basisIn ((List %)))): Not documented!!!!
--->-->ClosedLinearOperator((map (% (Mapping K K) %))): Not documented!!!!
--->-->ClosedLinearOperator((eval (% %))): Not documented!!!!
--->-->ClosedLinearOperator((ravel ((List K) %))): Not documented!!!!
--->-->ClosedLinearOperator((unravel (% (ClosedProp %) (List K)))): Not documented!!!!
--------(coerce (% (List (Integer))))---------
--->-->ClosedLinearOperator((coerce (% (List (Integer))))): Improper first word in comments: identity
"identity for composition and permutations of its products"
--------(coerce (% (List (None))))---------
--->-->ClosedLinearOperator((coerce (% (List (None))))): Improper first word in comments: []
"[] = 1"
--->-->ClosedLinearOperator((elt (% % %))): Not documented!!!!
--->-->ClosedLinearOperator((elt (% % (Integer)))): Not documented!!!!
--->-->ClosedLinearOperator((elt (% % (Integer) (Integer)))): Not documented!!!!
--->-->ClosedLinearOperator((elt (% % (Integer) (Integer) (Integer)))): Not documented!!!!
--->-->ClosedLinearOperator((/ (% (Tuple %) (Tuple %)))): Not documented!!!!
--->-->ClosedLinearOperator((/ (% (Tuple %) %))): Not documented!!!!
--------(/ (% % (Tuple %)))---------
--->-->ClosedLinearOperator((/ (% % (Tuple %)))): Improper first word in comments: yet
"yet another syntax for product"
--------(ev (% NNI))---------
--->-->ClosedLinearOperator((ev (% NNI))): Improper first word in comments: 
"(2,{}0)-tensor for evaluation"
--------(co (% NNI))---------
--->-->ClosedLinearOperator((co (% NNI))): Improper first word in comments: 
"(0,{}2)-tensor for co-evaluation"
--->-->ClosedLinearOperator(constructor): Not documented!!!!
--->-->ClosedLinearOperator(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/CLOP.NRLIB/CLOP.lsp" (written 31 MAY 2011 06:56:26 PM):

; /var/zope2/var/LatexWiki/CLOP.NRLIB/CLOP.fasl written
; compilation finished in 0:00:05.580
------------------------------------------------------------------------
   ClosedLinearOperator is now explicitly exposed in frame initial 
   ClosedLinearOperator will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/CLOP.NRLIB/CLOP

   >> 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

Getting Started

Consult the source code above for more details.

Convenient Notation

axiom

-- summation
macro Σ(f,i,b) == reduce(+,[f*b.i for i in 1..#b])

Type: Void

axiom

-- list comprehension
macro Ξ(f,i)==[f for i in 1..retract(dimension()$L)]

Type: Void

Example

axiom

Q := EXPR INT

$\label{eq1}\hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ })$

(1)

Type: Type

axiom

L := CLOP(OVAR ['x,'y],Q)

$\label{eq2}\hbox{\axiomType{ClosedLinearOperator}\ } (\hbox{\axiomType{OrderedVariableList}\ } ([ x , y ]) , \hbox{\axiomType{Expression}\ } (\hbox{\axiomType{Integer}\ }))$

(2)

Type: Type

axiom

)show L

 ClosedLinearOperator(OrderedVariableList([x,y]),Expression(Integer)) is a domain constructor.
 Abbreviation for ClosedLinearOperator is CLOP 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------

 ?*? : (Integer,%) -> %                ?*? : (PositiveInteger,%) -> %
 ?*? : (%,%) -> %                      ?+? : (%,%) -> %
 ?-? : (%,%) -> %                      -? : % -> %
 ?/? : (Tuple(%),Tuple(%)) -> %        ?/? : (Tuple(%),%) -> %
 ?/? : (%,Tuple(%)) -> %               ?/? : (%,%) -> %
 ?=? : (%,%) -> Boolean                1 : () -> %
 0 : () -> %                           ?^? : (%,Arity) -> %
 ?^? : (%,PositiveInteger) -> %        apply : (%,%) -> %
 arity : % -> ClosedProp(%)            basisIn : () -> List(%)
 basisOut : () -> List(%)              co : NonNegativeInteger -> %
 cod : % -> Arity                      coerce : % -> OutputForm
 coerce : Expression(Integer) -> %     coerce : Integer -> %
 coerce : List(Integer) -> %           coerce : List(None) -> %
 dagger : % -> %                       dimension : () -> CardinalNumber
 dom : % -> Arity                      elt : (%,Integer,Integer) -> %
 ?.? : (%,Integer) -> %                ?.? : (%,%) -> %
 ev : NonNegativeInteger -> %          eval : % -> %
 hash : % -> SingleInteger             latex : % -> String
 one? : % -> Boolean                   recip : % -> Union(%,"failed")
 sample : () -> %                      zero? : % -> Boolean
 ?~=? : (%,%) -> Boolean              
 ?*? : (Expression(Integer),%) -> %
 ?*? : (NonNegativeInteger,%) -> %
 ?*? : (%,Expression(Integer)) -> %
 ?/? : (%,Expression(Integer)) -> %
 ?^? : (%,NonNegativeInteger) -> %
 characteristic : () -> NonNegativeInteger
 elt : (%,Integer,Integer,Integer) -> %
 eval : (%,Equation(Expression(Integer))) -> %
 eval : (%,Expression(Integer),Expression(Integer)) -> %
 eval : (%,List(Equation(Expression(Integer)))) -> %
 eval : (%,List(Expression(Integer)),List(Expression(Integer))) -> %
 map : ((Expression(Integer) -> Expression(Integer)),%) -> %
 ravel : % -> List(Expression(Integer))
 retract : % -> Expression(Integer)
 retractIfCan : % -> Union(Expression(Integer),"failed")
 subtractIfCan : (%,%) -> Union(%,"failed")
 unravel : (ClosedProp(%),List(Expression(Integer))) -> %

Basis

axiom

dim:Integer:=retract dimension()$L

$\label{eq3}2$

(3)

Type: Integer

axiom

Dx:=basisOut()$L

$\label{eq4}\left[{|_{\ x}}, \:{|_{\ y}}\right]$

(4)

Type: List(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

dx:=basisIn()$L

$\label{eq5}\left[{|^{\ x}}, \:{|^{\ y}}\right]$

(5)

Type: List(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

matrix Ξ(Ξ( eval(dx.i * Dx.j), i),j)

$\label{eq6}\left[ \begin{array}{cc} {|_{\ x}^{\ x}}&{|_{\ x}^{\ y}} \ {|_{\ y}^{\ x}}&{|_{\ y}^{\ y}}$

(6)

Type: Matrix(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

matrix Ξ(Ξ( Dx.i / dx.j, i),j)

   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= 0,codomain= +,data= [1,0]]]
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= +,codomain= 0,data= [1,0]]]
   trail r =
     [lm= [domain= 0,codomain= +,data= [1,0]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
     [lm= [domain= +,codomain= 0,data= [1,0]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
     [[domain= 0,codomain= +,data= [1,0]],[domain= +,codomain= 0,data= [1,0]]]
   []
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= 0,codomain= +,data= [0,1]]]
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= +,codomain= 0,data= [1,0]]]
   trail r =
     [lm= [domain= 0,codomain= +,data= [0,1]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
     [lm= [domain= +,codomain= 0,data= [1,0]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
     [[domain= 0,codomain= +,data= [0,1]],[domain= +,codomain= 0,data= [1,0]]]
   []
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= 0,codomain= +,data= [1,0]]]
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= +,codomain= 0,data= [0,1]]]
   trail r =
     [lm= [domain= 0,codomain= +,data= [1,0]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
     [lm= [domain= +,codomain= 0,data= [0,1]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
     [[domain= 0,codomain= +,data= [1,0]],[domain= +,codomain= 0,data= [0,1]]]
   []
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= 0,codomain= +,data= [0,1]]]
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
      rm= [domain= +,codomain= 0,data= [0,1]]]
   trail r =
     [lm= [domain= 0,codomain= +,data= [0,1]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
     [lm= [domain= +,codomain= 0,data= [0,1]], mm= 1,
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
     [[domain= 0,codomain= +,data= [0,1]],[domain= +,codomain= 0,data= [0,1]]]
   []

$\label{eq7}\left[ \begin{array}{cc} & 0 \ 0 &$

(7)

Type: Matrix(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

(1,1)-tensor

axiom

A:L := Σ( Σ( script(a,[[j],[i]]), i,Dx), j,dx)

$\label{eq8}{{a_{1}^{1}}\ {|_{\ x}^{\ x}}}+{{a_{1}^{2}}\ {|_{\ y}^{\ x}}}+{{a_{2}^{1}}\ {|_{\ x}^{\ y}}}+{{a_{2}^{2}}\ {|_{\ y}^{\ y}}}$

(8)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

a:=arity(A)

$\label{eq9}+ \over +$

(9)

Type: ClosedProp?(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

p:=dom(A)

$\label{eq10}+$

(10)

Type: Arity

scalar

axiom

s:= 3::L

$\label{eq11}3$

(11)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

arity s

$\label{eq12}0 \over 0$

(12)

Type: ClosedProp?(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

2*s

$\label{eq13}6$

(13)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

s*2

$\label{eq14}6$

(14)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

Powers

axiom

A^p

$\label{eq15}{{a_{1}^{1}}\ {|_{\ x}^{\ x}}}+{{a_{1}^{2}}\ {|_{\ y}^{\ x}}}+{{a_{2}^{1}}\ {|_{\ x}^{\ y}}}+{{a_{2}^{2}}\ {|_{\ y}^{\ y}}}$

(15)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

a^p

$\label{eq16}+ \over +$

(16)

Type: ClosedProp?(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

s/A

                  0 +
                  - -
                  0 +
   arity warning: ---
                  0 +
                  - -
                  0 +
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                                                      +1  0+
      rm= [domain= 0,codomain= 0,data= 3][domain= +,codomain= +,data= |    |]]
                                                                      +0  1+
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                       + 1   2+
                                       |a   a |
                                       | 1   1|
      rm= [domain= +,codomain= +,data= |      |]]
                                       | 1   2|
                                       |a   a |
                                       + 2   2+
   trail r =
     [lm= [domain= 0,codomain= 0,data= 3],
                                       +1  0+
      mm= [domain= +,codomain= +,data= |    |], rm= 1]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   trail r =
                                       + 1   2+
                                       |a   a |
                                       | 1   1|
     [lm= [domain= +,codomain= +,data= |      |], mm= 1,
                                       | 1   2|
                                       |a   a |
                                       + 2   2+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,1,0,0]
   f, g =
                                                                   + 1   2+
                                                                   |a   a |
                                                                   | 1   1|
     [[domain= 0,codomain= 0,data= 3],[domain= +,codomain= +,data= |      |]]
                                                                   | 1   2|
                                                                   |a   a |
                                                                   + 2   2+
   [1,2]

$\label{eq17}{3 \ {a_{1}^{1}}\ {|_{\ x}^{\ x}}}+{3 \ {a_{1}^{2}}\ {|_{\ y}^{\ x}}}+{3 \ {a_{2}^{1}}\ {|_{\ x}^{\ y}}}+{3 \ {a_{2}^{2}}\ {|_{\ y}^{\ y}}}$

(17)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

A/s

                  + 0
                  - -
                  + 0
   arity warning: ---
                  + 0
                  - -
                  + 0
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                       + 1   2+
                                       |a   a |
                                       | 1   1|
      rm= [domain= +,codomain= +,data= |      |]]
                                       | 1   2|
                                       |a   a |
                                       + 2   2+
                                                     +1  0+
   lead r =  [lm= 1,mm= [domain= +,codomain= +,data= |    |],rm= 1]
                                                     +0  1+
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
   trail r =
                                       + 1   2+
                                       |a   a |
                                       | 1   1|
     [lm= [domain= +,codomain= +,data= |      |], mm= 1,
                                       | 1   2|
                                       |a   a |
                                       + 2   2+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   lnf, lfn, lng, lgn =  [0,0,1,0]
                                         + 1   2+
                                         |a   a |
                                         | 1   1|
   f, g =  [[domain= +,codomain= +,data= |      |],1]
                                         | 1   2|
                                         |a   a |
                                         + 2   2+
   [1,2]

$\label{eq18}\ {\left({{{a_{1}^{1}}\ {|_{\ x}^{\ x}}}+{{a_{1}^{2}}\ {|_{\ y}^{\ x}}}+{{a_{2}^{1}}\ {|_{\ x}^{\ y}}}+{{a_{2}^{2}}\ {|_{\ y}^{\ y}}}}\right)}\ {\left(3 \right)}$

(18)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

3*A

$\label{eq19}{3 \ {a_{1}^{1}}\ {|_{\ x}^{\ x}}}+{3 \ {a_{1}^{2}}\ {|_{\ y}^{\ x}}}+{3 \ {a_{2}^{1}}\ {|_{\ x}^{\ y}}}+{3 \ {a_{2}^{2}}\ {|_{\ y}^{\ y}}}$

(19)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

A/3

                  + 0
                  - -
                  + 0
   arity warning: ---
                  + 0
                  - -
                  + 0
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                       + 1   2+
                                       |a   a |
                                       | 1   1|
      rm= [domain= +,codomain= +,data= |      |]]
                                       | 1   2|
                                       |a   a |
                                       + 2   2+
                                                     +1  0+
   lead r =  [lm= 1,mm= [domain= +,codomain= +,data= |    |],rm= 1]
                                                     +0  1+
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
   trail r =
                                       + 1   2+
                                       |a   a |
                                       | 1   1|
     [lm= [domain= +,codomain= +,data= |      |], mm= 1,
                                       | 1   2|
                                       |a   a |
                                       + 2   2+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   lnf, lfn, lng, lgn =  [0,0,1,0]
                                         + 1   2+
                                         |a   a |
                                         | 1   1|
   f, g =  [[domain= +,codomain= +,data= |      |],1]
                                         | 1   2|
                                         |a   a |
                                         + 2   2+
   [1,2]

$\label{eq20}\ {\left({{{a_{1}^{1}}\ {|_{\ x}^{\ x}}}+{{a_{1}^{2}}\ {|_{\ y}^{\ x}}}+{{a_{2}^{1}}\ {|_{\ x}^{\ y}}}+{{a_{2}^{2}}\ {|_{\ y}^{\ y}}}}\right)}\ {\left(3 \right)}$

(20)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

identities

axiom

I:L := [1]

$\label{eq21}{|_{\ x}^{\ x}}+{|_{\ y}^{\ y}}$

(21)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

I*I

$\label{eq22}\ {{\left({{|_{\ x}^{\ x}}+{|_{\ y}^{\ y}}}\right)}^2}$

(22)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

arity(I*I)

$\label{eq23}{+^2}\over{+^2}$

(23)

Type: ClosedProp?(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

I/I

                                                     +1  0+
   lead r =  [lm= 1,mm= [domain= +,codomain= +,data= |    |],rm= 1]
                                                     +0  1+
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
                                                     +1  0+
   lead r =  [lm= 1,mm= [domain= +,codomain= +,data= |    |],rm= 1]
                                                     +0  1+
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+

$\label{eq24}{|_{\ x}^{\ x}}+{|_{\ y}^{\ y}}$

(24)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

H:L:=[1,2]

$\label{eq25}{|_{\ x \ x}^{\ x \ x}}+{|_{\ x \ y}^{\ x \ y}}+{|_{\ y \ x}^{\ y \ x}}+{|_{\ y \ y}^{\ y \ y}}$

(25)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

arity(H)

$\label{eq26}{+^2}\over{+^2}$

(26)

Type: ClosedProp?(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

eval(I*I)

$\label{eq27}{|_{\ x \ x}^{\ x \ x}}+{|_{\ x \ y}^{\ x \ y}}+{|_{\ y \ x}^{\ y \ x}}+{|_{\ y \ y}^{\ y \ y}}$

(27)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

arity eval(I*I)

$\label{eq28}{+^2}\over{+^2}$

(28)

Type: ClosedProp?(ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer)))

axiom

test( I*I = H )

$\label{eq29} \mbox{\rm true}$

(29)

Type: Boolean

axiom

-- twist
X:L := [2,1]

$\label{eq30}{|_{\ x \ x}^{\ x \ x}}+{|_{\ y \ x}^{\ x \ y}}+{|_{\ x \ y}^{\ y \ x}}+{|_{\ y \ y}^{\ y \ y}}$

(30)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

test(X/X=H)

   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
     [[domain= + ,codomain= + ,data= |              |],
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
      [domain= + ,codomain= + ,data= |              |]]
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
   f/g = I*I

$\label{eq31} \mbox{\rm true}$

(31)

Type: Boolean

axiom

test(X/H=X)

   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                         ++1  0+  +0  1++
                                         ||    |  |    ||
                    2            2       |+0  0+  +0  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  0+  +0  0+|
                                         ||    |  |    ||
                                         ++1  0+  +0  1++
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
                                         ++1  0+  +0  1++
                                         ||    |  |    ||
                    2            2       |+0  0+  +0  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  0+  +0  0+|
                                         ||    |  |    ||
                                         ++1  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
     [[domain= + ,codomain= + ,data= |              |],
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
                                     ++1  0+  +0  1++
                                     ||    |  |    ||
                2            2       |+0  0+  +0  0+|
      [domain= + ,codomain= + ,data= |              |]]
                                     |+0  0+  +0  0+|
                                     ||    |  |    ||
                                     ++1  0+  +0  1++
   [2,1,3,4]

$\label{eq32} \mbox{\rm true}$

(32)

Type: Boolean

axiom

test(H/X=X)

   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                         ++1  0+  +0  1++
                                         ||    |  |    ||
                    2            2       |+0  0+  +0  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  0+  +0  0+|
                                         ||    |  |    ||
                                         ++1  0+  +0  1++
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
   trail r =
                                         ++1  0+  +0  1++
                                         ||    |  |    ||
                    2            2       |+0  0+  +0  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  0+  +0  0+|
                                         ||    |  |    ||
                                         ++1  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
                                     ++1  0+  +0  1++
                                     ||    |  |    ||
                2            2       |+0  0+  +0  0+|
     [[domain= + ,codomain= + ,data= |              |],
                                     |+0  0+  +0  0+|
                                     ||    |  |    ||
                                     ++1  0+  +0  1++
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
      [domain= + ,codomain= + ,data= |              |]]
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
   [1,2,4,3]

$\label{eq33} \mbox{\rm true}$

(33)

Type: Boolean

axiom

-- printing
I*X*X*I

$\label{eq34}\begin{array}{@{}l} \displaystyle \ {\left({{|_{\ x}^{\ x}}+{|_{\ y}^{\ y}}}\right)}\ \cdot \ \ \displaystyle {{\left({{|_{\ x \ x}^{\ x \ x}}+{|_{\ y \ x}^{\ x \ y}}+{|_{\ x \ y}^{\ y \ x}}+{|_{\ y \ y}^{\ y \ y}}}\right)}^2}\ \cdot \ \ \displaystyle {\left({{|_{\ x}^{\ x}}+{|_{\ y}^{\ y}}}\right)}$

(34)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

(I*X*X*I)/(X*I*I*X)

   lead r =
                                              +1  0+
     [lm= 1, mm= [domain= +,codomain= +,data= |    |],
                                              +0  1+
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+

       rm =
                                          ++1  0+  +0  0++
                                          ||    |  |    ||
                     2            2       |+0  0+  +1  0+|
           [domain= + ,codomain= + ,data= |              |]
                                          |+0  1+  +0  0+|
                                          ||    |  |    ||
                                          ++0  0+  +0  1++
        *
                                        +1  0+
           [domain= +,codomain= +,data= |    |]
                                        +0  1+
       ]
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |],
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      mm= [domain= +,codomain= +,data= |    |], rm= 1]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   lnf, lfn, lng, lgn =  [1,0,0,1]
   f, g =
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
     [[domain= + ,codomain= + ,data= |              |],
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
      [domain= + ,codomain= + ,data= |              |]]
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
   [4,1,2,5,6,3]
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+

       rm =
                                          ++1  0+  +0  0++
                                          ||    |  |    ||
                     2            2       |+0  0+  +1  0+|
           [domain= + ,codomain= + ,data= |              |]
                                          |+0  1+  +0  0+|
                                          ||    |  |    ||
                                          ++0  0+  +0  1++
        *
                                        +1  0+
           [domain= +,codomain= +,data= |    |]
                                        +0  1+
       ]
   lead r =
                                              +1  0+
     [lm= 1, mm= [domain= +,codomain= +,data= |    |],
                                              +0  1+
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
      rm= [domain= + ,codomain= + ,data= |              |]]
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |],
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      mm= [domain= +,codomain= +,data= |    |], rm= 1]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   trail r =
                                         ++1  0+  +0  0++
                                         ||    |  |    ||
                    2            2       |+0  0+  +1  0+|
     [lm= [domain= + ,codomain= + ,data= |              |], mm= 1,
                                         |+0  1+  +0  0+|
                                         ||    |  |    ||
                                         ++0  0+  +0  1++
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,1,1,0]
   f, g =
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
     [[domain= + ,codomain= + ,data= |              |],
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
                                     ++1  0+  +0  0++
                                     ||    |  |    ||
                2            2       |+0  0+  +1  0+|
      [domain= + ,codomain= + ,data= |              |]]
                                     |+0  1+  +0  0+|
                                     ||    |  |    ||
                                     ++0  0+  +0  1++
   [1,2,4,3,5,6]

$\label{eq35}\begin{array}{@{}l} \displaystyle \ {\left({ \begin{array}{@{}l} \displaystyle {|_{\ x \ x \ x}^{\ x \ x \ x}}+{|_{\ y \ x \ x}^{\ x \ x \ y}}+{|_{\ x \ x \ y}^{\ x \ y \ x}}+ \ \ \displaystyle {|_{\ y \ x \ y}^{\ x \ y \ y}}+{|_{\ x \ y \ x}^{\ y \ x \ x}}+{|_{\ y \ y \ x}^{\ y \ x \ y}}+ \ \ \displaystyle {|_{\ x \ y \ y}^{\ y \ y \ x}}+{|_{\ y \ y \ y}^{\ y \ y \ y}}$

(35)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

-- trace
U:L:=ev(1)

$\label{eq36}{|^{\ x \ x}}+{|^{\ y \ y}}$

(36)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

Ω:L:=co(1)

$\label{eq37}{|_{\ x \ x}}+{|_{\ y \ y}}$

(37)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

Ω/U

   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                                2       +1  0+
      rm= [domain= 0,codomain= + ,data= |    |]]
                                        +0  1+
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+
                    2                   +1  0+
      rm= [domain= + ,codomain= 0,data= |    |]]
                                        +0  1+
   trail r =
                                2       +1  0+
     [lm= [domain= 0,codomain= + ,data= |    |], mm= 1,
                                        +0  1+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
                    2                   +1  0+
     [lm= [domain= + ,codomain= 0,data= |    |], mm= 1,
                                        +0  1+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,0,0,0]
   f, g =
                            2       +1  0+
     [[domain= 0,codomain= + ,data= |    |],
                                    +0  1+
                2                   +1  0+
      [domain= + ,codomain= 0,data= |    |]]
                                    +0  1+
   []

$\label{eq38}2$

(38)

Type: ClosedLinearOperator?(OrderedVariableList?([x,y]),Expression(Integer))

axiom

test
  ( I Ω  ) /
  (  U I ) = I

   lead r =
                                              +1  0+
     [lm= 1, mm= [domain= +,codomain= +,data= |    |],
                                              +0  1+
                                2       +1  0+
      rm= [domain= 0,codomain= + ,data= |    |]]
                                        +0  1+
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+

       rm =
                     2                   +1  0+
           [domain= + ,codomain= 0,data= |    |]
                                         +0  1+
        *
                                        +1  0+
           [domain= +,codomain= +,data= |    |]
                                        +0  1+
       ]
   trail r =
                                2       +1  0+
     [lm= [domain= 0,codomain= + ,data= |    |], mm= 1,
                                        +0  1+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   trail r =
                    2                   +1  0+
     [lm= [domain= + ,codomain= 0,data= |    |],
                                        +0  1+
                                       +1  0+
      mm= [domain= +,codomain= +,data= |    |], rm= 1]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   lnf, lfn, lng, lgn =  [1,0,0,1]
   f, g =
                            2       +1  0+
     [[domain= 0,codomain= + ,data= |    |],
                                    +0  1+
                2                   +1  0+
      [domain= + ,codomain= 0,data= |    |]]
                                    +0  1+
   [2,1]

$\label{eq39} \mbox{\rm true}$

(39)

Type: Boolean

axiom

test
  (  Ω I ) /
  ( I U  ) = I

   lead r =
                                       +1  0+
     [lm= [domain= +,codomain= +,data= |    |], mm= 1,
                                       +0  1+

       rm =
                                 2       +1  0+
           [domain= 0,codomain= + ,data= |    |]
                                         +0  1+
        *
                                        +1  0+
           [domain= +,codomain= +,data= |    |]
                                        +0  1+
       ]
   lead r =
                                              +1  0+
     [lm= 1, mm= [domain= +,codomain= +,data= |    |],
                                              +0  1+
                    2                   +1  0+
      rm= [domain= + ,codomain= 0,data= |    |]]
                                        +0  1+
                                               +1  0+
   lead r =  [lm= [domain= +,codomain= +,data= |    |],mm= 1,rm= 1]
                                               +0  1+
   trail r =
                                2       +1  0+
     [lm= [domain= 0,codomain= + ,data= |    |],
                                        +0  1+
                                       +1  0+
      mm= [domain= +,codomain= +,data= |    |], rm= 1]
                                       +0  1+
                                                            +1  0+
   trail r =  [lm= 1,mm= 1,rm= [domain= +,codomain= +,data= |    |]]
                                                            +0  1+
   trail r =
                    2                   +1  0+
     [lm= [domain= + ,codomain= 0,data= |    |], mm= 1,
                                        +0  1+
                                       +1  0+
      rm= [domain= +,codomain= +,data= |    |]]
                                       +0  1+
   lnf, lfn, lng, lgn =  [0,1,1,0]
   f, g =
                            2       +1  0+
     [[domain= 0,codomain= + ,data= |    |],
                                    +0  1+
                2                   +1  0+
      [domain= + ,codomain= 0,data= |    |]]
                                    +0  1+
   [2,1]

$\label{eq40} \mbox{\rm true}$

(40)

Type: Boolean

Back to the top.

Comments

Please leave comments and suggestions.

Thanks

Bill Page