MathAction DependentTypeTest2

login home contents what's new discussion bug reports help links subscribe changes refresh edit

SandBox
DependentTypeTest1 ← ↑ → DerivFunc

DependentTypeTest2
last edited 3 years ago by pagani

fricas
(1) -> <spad>
--)lisp (defvar |$inclAssertions| nil)

-- in principle d:V[k]->V[k+1], then what is d d = 0?
-- each vector space V[k] has its own zero! But we will
-- only use one zero form for all. ZeroChain()?
fricas
)abbrev category CCHNCAT CoChainCategory
CoChainCategory() : Category == SetCategory with
 degree : % -> Polynomial Integer 
 mainType : % -> String -- trick: get the type
fricas
)abbrev category ZCHNCAT ZeroChainCategory
ZeroChainCategory() : Category == SetCategory with
 null : %
fricas
)abbrev domain ZCHN ZeroChain
ZeroChain : Exports == Implementation where
 BOP ==> BasicOperator 
 PINT ==> Polynomial Integer
 Exports == Join(CoChainCategory,ZeroChainCategory) with
 degree : % -> PINT 
 d : % -> %
 --null : %
 Implementation == BOP add 
 Rep := BOP 
 null == operator("0"::Symbol) 
 degree x == 0::PINT
 d x == null()
 mainType x == "ZeroChain"
fricas
)abbrev domain COCHN CoChain
CoChain(p) : Exports == Implementation where 
 p:Polynomial Integer
 BOP ==> BasicOperator 
 CTOF ==> CoercibleTo OutputForm
 CVTS ==> ConvertibleTo String
 PINT ==> Polynomial Integer
 Exports == Join(CTOF, CVTS, CoChainCategory) with
 coerce : Symbol -> %
 degree : % -> PINT 
 Implementation == BOP add 
 Rep := BOP 
 coerce(s:Symbol):% == operator s
 degree x == p
 mainType x == "CoChain"
fricas
)abbrev domain WEDGE WedgeProduct
WedgeProduct(a,b) : Exports == Implementation where 
 CCCAT ==> CoChainCategory
 OF ==> OutputForm
 a:CCCAT
 b:CCCAT 
 CTOF ==> CoercibleTo OutputForm
 CVTS ==> ConvertibleTo String
 PINT ==> Polynomial Integer
 Exports == Join(CTOF, CVTS, CoChainCategory) with
 if a has ZeroChainCategory or b has ZeroChainCategory then
 _* : (a,b) -> ZeroChain
 else
 _* : (a,b) -> %
 degree : % -> PINT 
 Implementation == add 
 if a has ZeroChainCategory or b has ZeroChainCategory then
 Rep := ZeroChain
 (x:a * y:b):ZeroChain == null()$ZeroChain 
 else
 Rep := Record(left:a,right:b) 
 x * y == [x,y]@Rep
 degree x == degree(x.left)$a + degree(x.right)$b
 mainType x == "WedgeProduct"
 coerce(x:%):OutputForm == tensor(x.left::OF,x.right::OF)
 ------ temp using tensor, lack of wedge symbol
fricas
)abbrev domain EXTDF ExteriorDerivative
ExteriorDerivative(a) : Exports == Implementation where 
 CCCAT ==> CoChainCategory
 OF ==> OutputForm
 a:CCCAT
 CTOF ==> CoercibleTo OutputForm
 CVTS ==> ConvertibleTo String
 PINT ==> Polynomial Integer
 Exports == Join(CTOF, CVTS, CoChainCategory) with
 d : % -> ZeroChain
 d : a -> %
 degree : % -> PINT 
 Implementation == add
 if a has ZeroChainCategory then
 Rep := ZeroChain
 else
 Rep := Record(arg:a) 
 d(x:%):ZeroChain == null()$ZeroChain
 d(x:a):% == [x]@Rep
 degree x == 1 + degree(x.arg)$a 
 mainType x == "ExteriorDerivative"
 coerce(x:%):OutputForm ==
 dsym:=outputForm("d"::Symbol)$OF
 mainType(x.arg)$a = "CoChain" => hconcat(dsym,x.arg::OF) 
 hconcat(dsym,paren(x.arg::OF))
fricas
)abbrev domain HODGE HodgeStar
HodgeStar(a) : Exports == Implementation where 
 CCCAT ==> CoChainCategory
 OF ==> OutputForm
 a:CCCAT
 CTOF ==> CoercibleTo OutputForm
 CVTS ==> ConvertibleTo String
 PINT ==> Polynomial Integer
 Exports == Join(CTOF, CVTS, CoChainCategory) with
 hodge : a -> %
 degree : % -> PINT 
 Implementation == add 
 Rep := Record(arg:a) 
 n:PINT:="spacedim"::Symbol::PINT
 degree x == n - degree(x.arg)$a 
 hodge x == [x]@Rep
 mainType x == "HodgeStar"
 coerce(x:%):OutputForm ==
 dsym:=outputForm("*"::Symbol)$OF
 mT:String:=mainType(x.arg)$a
 mT ~= "WedgeProduct" => hconcat(dsym,x.arg::OF) 
 hconcat(dsym,paren(x.arg::OF))</spad>
fricas
Compiling FriCAS source code from file 
 /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5250937285633644280-25px001.spad
 using old system compiler.
 CCHNCAT abbreviates category CoChainCategory 
------------------------------------------------------------------------
 initializing NRLIB CCHNCAT for CoChainCategory 
 compiling into NRLIB CCHNCAT 
Time: 0 SEC.

 finalizing NRLIB CCHNCAT 
 Processing CoChainCategory for Browser database:
--->-->CoChainCategory(constructor): Not documented!!!!
--->-->CoChainCategory((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->CoChainCategory((mainType ((String) %))): Not documented!!!!
--->-->CoChainCategory(): Missing Description
; compiling file "/var/aw/var/LatexWiki/CCHNCAT.NRLIB/CCHNCAT.lsp" (written 04 AUG 2025 05:31:50 PM):

; wrote /var/aw/var/LatexWiki/CCHNCAT.NRLIB/CCHNCAT.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
 CoChainCategory is now explicitly exposed in frame initial 
 CoChainCategory will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/CCHNCAT.NRLIB/CCHNCAT

 ZCHNCAT abbreviates category ZeroChainCategory 
------------------------------------------------------------------------
 initializing NRLIB ZCHNCAT for ZeroChainCategory 
 compiling into NRLIB ZCHNCAT 
Time: 0 SEC.

 finalizing NRLIB ZCHNCAT 
 Processing ZeroChainCategory for Browser database:
--->-->ZeroChainCategory(constructor): Not documented!!!!
--->-->ZeroChainCategory((null (%) constant)): Not documented!!!!
--->-->ZeroChainCategory(): Missing Description
; compiling file "/var/aw/var/LatexWiki/ZCHNCAT.NRLIB/ZCHNCAT.lsp" (written 04 AUG 2025 05:31:50 PM):

; wrote /var/aw/var/LatexWiki/ZCHNCAT.NRLIB/ZCHNCAT.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
 ZeroChainCategory is now explicitly exposed in frame initial 
 ZeroChainCategory will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/ZCHNCAT.NRLIB/ZCHNCAT

 ZCHN abbreviates domain ZeroChain 
------------------------------------------------------------------------
 initializing NRLIB ZCHN for ZeroChain 
 compiling into NRLIB ZCHN 
 compiling exported null : () -> %
Time: 0 SEC.

 compiling exported degree : % -> Polynomial Integer
Time: 0.02 SEC.

 compiling exported d : % -> %
Time: 0 SEC.

 compiling exported mainType : % -> String
 ZCHN;mainType;%S;4 is replaced by ZeroChain 
Time: 0 SEC.

(time taken in buildFunctor: 0)
Time: 0 SEC.

 Cumulative Statistics for Constructor ZeroChain
 Time: 0.02 seconds

--------------non extending category----------------------
.. ZeroChain of cat 
(|Join| (|CoChainCategory|) (|ZeroChainCategory|)
 (CATEGORY |domain| (SIGNATURE |degree| ((|Polynomial| (|Integer|)) %))
 (SIGNATURE |d| (% %)))) has no 
(|OrderedSet|) finalizing NRLIB ZCHN 
 Processing ZeroChain for Browser database:
--->-->ZeroChain(constructor): Not documented!!!!
--->-->ZeroChain((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->ZeroChain((d (% %))): Not documented!!!!
--->-->ZeroChain(): Missing Description
; compiling file "/var/aw/var/LatexWiki/ZCHN.NRLIB/ZCHN.lsp" (written 04 AUG 2025 05:31:50 PM):

; wrote /var/aw/var/LatexWiki/ZCHN.NRLIB/ZCHN.fasl
; compilation finished in 0:00:00.016
------------------------------------------------------------------------
 ZeroChain is now explicitly exposed in frame initial 
 ZeroChain will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/ZCHN.NRLIB/ZCHN

 COCHN abbreviates domain CoChain 
------------------------------------------------------------------------
 initializing NRLIB COCHN for CoChain 
 compiling into NRLIB COCHN 
 compiling exported coerce : Symbol -> %
Time: 0 SEC.

 compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

 compiling exported mainType : % -> String
 COCHN;mainType;%S;3 is replaced by CoChain 
Time: 0 SEC.

(time taken in buildFunctor: 0)
Time: 0 SEC.

 Cumulative Statistics for Constructor CoChain
 Time: 0 seconds

--------------non extending category----------------------
.. CoChain(#1) of cat 
(|Join| (|CoercibleTo| (|OutputForm|)) (|ConvertibleTo| (|String|))
 (|CoChainCategory|)
 (CATEGORY |domain| (SIGNATURE |coerce| (% (|Symbol|)))
 (SIGNATURE |degree| ((|Polynomial| (|Integer|)) %)))) has no 
(|OrderedSet|) finalizing NRLIB COCHN 
 Processing CoChain for Browser database:
--->-->CoChain(constructor): Not documented!!!!
--->-->CoChain((coerce (% (Symbol)))): Not documented!!!!
--->-->CoChain((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->CoChain(): Missing Description
; compiling file "/var/aw/var/LatexWiki/COCHN.NRLIB/COCHN.lsp" (written 04 AUG 2025 05:31:50 PM):

; wrote /var/aw/var/LatexWiki/COCHN.NRLIB/COCHN.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
 CoChain is now explicitly exposed in frame initial 
 CoChain will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/COCHN.NRLIB/COCHN

 WEDGE abbreviates domain WedgeProduct 
------------------------------------------------------------------------
 initializing NRLIB WEDGE for WedgeProduct 
 compiling into NRLIB WEDGE 
****** Domain: a already in scope
augmenting a: (ZeroChainCategory)
Local variable Rep type redefined: (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %)))) to (Join (OrderedSet) (CATEGORY domain (SIGNATURE name ((Symbol) %)) (SIGNATURE properties ((AssociationList (Symbol) (None)) %)) (SIGNATURE copy (% %)) (SIGNATURE operator (% (Symbol))) (SIGNATURE operator (% (Symbol) (NonNegativeInteger))) (SIGNATURE arity ((Union (NonNegativeInteger) failed) %)) (SIGNATURE nullary? ((Boolean) %)) (SIGNATURE unary? ((Boolean) %)) (SIGNATURE nary? ((Boolean) %)) (SIGNATURE weight ((NonNegativeInteger) %)) (SIGNATURE weight (% % (NonNegativeInteger))) (SIGNATURE equality (% % (Mapping (Boolean) % %))) (SIGNATURE comparison (% % (Mapping (Boolean) % %))) (SIGNATURE display ((Union (Mapping (OutputForm) (List (OutputForm))) failed) %)) (SIGNATURE display (% % (Mapping (OutputForm) (List (OutputForm))))) (SIGNATURE display (% % (Mapping (OutputForm) (OutputForm)))) (SIGNATURE input (% % (Mapping (InputForm) (List (InputForm))))) (SIGNATURE input ((Union (Mapping (InputForm) (List (InputForm))) failed) %)) (SIGNATURE is? ((Boolean) % (Symbol))) (SIGNATURE has? ((Boolean) % (Symbol))) (SIGNATURE assert (% % (Symbol))) (SIGNATURE deleteProperty! (% % (Symbol))) (SIGNATURE property ((Union (None) failed) % (Symbol))) (SIGNATURE setProperty (% % (Symbol) (None))) (SIGNATURE setProperties (% % (AssociationList (Symbol) (None))))))
 compiling exported * : (a,b) -> ZeroChain
Time: 0 SEC.

****** Domain: b already in scope
augmenting b: (ZeroChainCategory)
 compiling exported * : (a,b) -> ZeroChain
Time: 0 SEC.

Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left a) (: right b)) a b)) (SIGNATURE ~= ((Boolean) (Record (: left a) (: right b)) (Record (: left a) (: right b)))) (SIGNATURE coerce ((OutputForm) (Record (: left a) (: right b)))) (SIGNATURE elt (a (Record (: left a) (: right b)) left)) (SIGNATURE elt (b (Record (: left a) (: right b)) right)) (SIGNATURE setelt! (a (Record (: left a) (: right b)) left a)) (SIGNATURE setelt! (b (Record (: left a) (: right b)) right b)) (SIGNATURE copy ((Record (: left a) (: right b)) (Record (: left a) (: right b)))))) to (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %))))
 compiling exported * : (a,b) -> %
 WEDGE;*;ab%;3 is replaced by CONS 
Time: 0 SEC.

 compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

 compiling exported mainType : % -> String
 WEDGE;mainType;%S;5 is replaced by WedgeProduct 
Time: 0 SEC.

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

(time taken in buildFunctor: 0)
Time: 0 SEC.

 Warnings: 
 [1] *: signature of lhs not unique: ab chosen

 Cumulative Statistics for Constructor WedgeProduct
 Time: 0 seconds

 finalizing NRLIB WEDGE 
 Processing WedgeProduct for Browser database:
--->-->WedgeProduct(constructor): Not documented!!!!
--->-->WedgeProduct((* ((ZeroChain) a b))): Not documented!!!!
--->-->WedgeProduct((* (% a b))): Not documented!!!!
--->-->WedgeProduct((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->WedgeProduct(): Missing Description
; compiling file "/var/aw/var/LatexWiki/WEDGE.NRLIB/WEDGE.lsp" (written 04 AUG 2025 05:31:50 PM):

; wrote /var/aw/var/LatexWiki/WEDGE.NRLIB/WEDGE.fasl
; compilation finished in 0:00:00.016
------------------------------------------------------------------------
 WedgeProduct is now explicitly exposed in frame initial 
 WedgeProduct will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/WEDGE.NRLIB/WEDGE

 EXTDF abbreviates domain ExteriorDerivative 
------------------------------------------------------------------------
 initializing NRLIB EXTDF for ExteriorDerivative 
 compiling into NRLIB EXTDF 
****** Domain: a already in scope
augmenting a: (ZeroChainCategory)
Local variable Rep type redefined: (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %)))) to (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: left a) (: right b)) a b)) (SIGNATURE ~= ((Boolean) (Record (: left a) (: right b)) (Record (: left a) (: right b)))) (SIGNATURE coerce ((OutputForm) (Record (: left a) (: right b)))) (SIGNATURE elt (a (Record (: left a) (: right b)) left)) (SIGNATURE elt (b (Record (: left a) (: right b)) right)) (SIGNATURE setelt! (a (Record (: left a) (: right b)) left a)) (SIGNATURE setelt! (b (Record (: left a) (: right b)) right b)) (SIGNATURE copy ((Record (: left a) (: right b)) (Record (: left a) (: right b))))))
Local variable Rep type redefined: (Join (SetCategory) (CATEGORY domain (SIGNATURE construct ((Record (: arg a)) a)) (SIGNATURE ~= ((Boolean) (Record (: arg a)) (Record (: arg a)))) (SIGNATURE coerce ((OutputForm) (Record (: arg a)))) (SIGNATURE elt (a (Record (: arg a)) arg)) (SIGNATURE setelt! (a (Record (: arg a)) arg a)) (SIGNATURE copy ((Record (: arg a)) (Record (: arg a)))))) to (Join (CoChainCategory) (ZeroChainCategory) (CATEGORY domain (SIGNATURE degree ((Polynomial (Integer)) %)) (SIGNATURE d (% %))))
 compiling exported d : % -> ZeroChain
Time: 0 SEC.

 compiling exported d : a -> %
 EXTDF;d;a%;2 is replaced by LIST 
Time: 0 SEC.

 compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

 compiling exported mainType : % -> String
 EXTDF;mainType;%S;4 is replaced by ExteriorDerivative 
Time: 0 SEC.

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

(time taken in buildFunctor: 0)
Time: 0 SEC.

 Cumulative Statistics for Constructor ExteriorDerivative
 Time: 0.02 seconds

 finalizing NRLIB EXTDF 
 Processing ExteriorDerivative for Browser database:
--->-->ExteriorDerivative(constructor): Not documented!!!!
--->-->ExteriorDerivative((d ((ZeroChain) %))): Not documented!!!!
--->-->ExteriorDerivative((d (% a))): Not documented!!!!
--->-->ExteriorDerivative((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->ExteriorDerivative(): Missing Description
; compiling file "/var/aw/var/LatexWiki/EXTDF.NRLIB/EXTDF.lsp" (written 04 AUG 2025 05:31:50 PM):

; wrote /var/aw/var/LatexWiki/EXTDF.NRLIB/EXTDF.fasl
; compilation finished in 0:00:00.008
------------------------------------------------------------------------
 ExteriorDerivative is now explicitly exposed in frame initial 
 ExteriorDerivative will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/EXTDF.NRLIB/EXTDF

 HODGE abbreviates domain HodgeStar 
------------------------------------------------------------------------
 initializing NRLIB HODGE for HodgeStar 
 compiling into NRLIB HODGE 
 compiling exported degree : % -> Polynomial Integer
Time: 0 SEC.

 compiling exported hodge : a -> %
 HODGE;hodge;a%;2 is replaced by LIST 
Time: 0 SEC.

 compiling exported mainType : % -> String
 HODGE;mainType;%S;3 is replaced by HodgeStar 
Time: 0 SEC.

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

(time taken in buildFunctor: 0)
Time: 0 SEC.

 Cumulative Statistics for Constructor HodgeStar
 Time: 0.01 seconds

 finalizing NRLIB HODGE 
 Processing HodgeStar for Browser database:
--->-->HodgeStar(constructor): Not documented!!!!
--->-->HodgeStar((hodge (% a))): Not documented!!!!
--->-->HodgeStar((degree ((Polynomial (Integer)) %))): Not documented!!!!
--->-->HodgeStar(): Missing Description
; compiling file "/var/aw/var/LatexWiki/HODGE.NRLIB/HODGE.lsp" (written 04 AUG 2025 05:31:51 PM):

; wrote /var/aw/var/LatexWiki/HODGE.NRLIB/HODGE.fasl
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
 HodgeStar is now explicitly exposed in frame initial 
 HodgeStar will be automatically loaded when needed from 
 /var/aw/var/LatexWiki/HODGE.NRLIB/HODGE

fricas
f:=f::CoChain(p)
\label{eq1}f (1)
Type: CoChain?(p)
fricas
g:=g::CoChain(q)
\label{eq2}g (2)
Type: CoChain?(q)
fricas
h:=f*g
\label{eq3}f \otimes g (3)
Type: WedgeProduct?(CoChain?(p),CoChain?(q))
fricas
degree h
\label{eq4}q + p (4)
Type: Polynomial(Integer)
fricas
k:=h*f
\label{eq5}{f \otimes g}\otimes f (5)
Type: WedgeProduct?(WedgeProduct?(CoChain?(p),CoChain?(q)),CoChain?(p))
fricas
degree k
\label{eq6}q +{2 \ p} (6)
Type: Polynomial(Integer)
fricas
-- car dom (d f) --> ExteriorDerivative
Type: SExpression?
fricas
-- symbol car dom (d f) = 'ExteriorDerivative::Symbol => ok
degree d f --> p+1
\label{eq7}p + 1 (7)
Type: Polynomial(Integer)
fricas
hodge d h --> *d(f # g)
{d{\left(f \otimes g \right)}}" title=" \label{eq8}{d{\left(f \otimes g \right)}}" class="equation" src="images/8036090974347895857-16.0px.png" align="bottom" Style="vertical-align:text-bottom" width="66" height="18"/> (8)
Type: HodgeStar?(ExteriorDerivative?(WedgeProduct?(CoChain?(p),CoChain?(q))))
fricas
r:=degree hodge h
\label{eq9}spacedim - q - p (9)
Type: Polynomial(Integer)
fricas
eval(r,[p=7,q=3,'spacedim=15]) --> notice the quote!
\label{eq10}5 (10)
Type: Polynomial(Integer)
fricas
-->degree % --> spacedim - q - p - 1

null()$ZeroChain
\label{eq11}0 (11)
Type: ZeroChain?
fricas
z:=d d f
\label{eq12}0 (12)
Type: ZeroChain?
fricas
z*f
\label{eq13}0 (13)
Type: ZeroChain?
fricas
f*z
\label{eq14}0 (14)
Type: ZeroChain?
fricas
CoChain(p) has ZeroChainCategory
\label{eq15} \mbox{\rm false} (15)
Type: Boolean
fricas
ZeroChain has ZeroChainCategory
\label{eq16} \mbox{\rm true} (16)
Type: Boolean




Subject: Be Bold !!
( 15 subscribers )
Please rate this page:

AltStyle によって変換されたページ (->オリジナル) /