|
|
|
last edited 15 years ago by page |
Edit detail for SandBoxNonZeroIntegerInOpenAxiom revision 1 of 1
| 1 | ||
|
Editor: page
Time: 2009/01/08 17:23:13 GMT-8 |
||
| Note: new | ||
changed: - Algebra SandBoxNonZeroInteger is an attempt to define the domain of Integers without 0 as a SubDomain. \begin{spad} )abbrev domain NZINT NonZeroInteger NonZeroInteger: Join(OrderedAbelianSemiGroup, Monoid --,CoercibleTo(Integer) ) with commutative("*") gcd: (%,%) -> % ++ gcd(a,b) computes the greatest common divisor of two ++ positive integers \spad{a} and b. _-: % -> % --retract:Integer->% --retractIfCan:Integer->Union(%,"failed") --retract:NonNegativeInteger->% --retractIfCan:NonNegativeInteger->Union(%,"failed") --convert:NonNegativeInteger->% == SubDomain(Integer,not(#1 = 0)) add Rep == Integer x:% y:% z:Integer nz:NonNegativeInteger -x == (-(x pretend Integer)) pretend % x+y == (z:=(x pretend Integer)+(y pretend Integer)) = 0 => error "zero" z pretend % --coerce(x):Integer == x pretend Integer --retract(z)== z pretend % --convert(nz):% == retract(nz) --retractIfCan(z) == -- zero?(z) => "failed" -- retract(z) --retract(nz)== nz pretend % --retractIfCan(nz) == -- zero?(nz) => "failed" -- retract(nz) \end{spad} \begin{axiom} )show NZINT \end{axiom} \begin{axiom} i:NZINT := 1$NZINT i:NZINT := (1::Integer) i:NZINT := 1 \end{axiom} \begin{axiom} j:NZINT := -1 \end{axiom} \begin{axiom} j:NZINT:=-i i+1 j+1 i+j \end{axiom} \begin{axiom} i-j retractIfCan(0)$NZINT \end{axiom} Can we define 'NonZero' as a functor? \begin{spad} )abbrev domain NZ NonZero NonZero(T:Ring): Join(OrderedAbelianSemiGroup, Monoid) with Commutative("*") _-: % -> % == SubDomain(T,not(#1 = 0)) add Rep == T x:% y:% z:T -x == (-(x pretend T)) pretend % x+y == (z:=(x pretend T)+(y pretend T)) = 0 => error "zero" z pretend % \end{spad} \begin{axiom} )show NonZero(Float) \end{axiom} \begin{axiom} f:NonZero(Float):=1 g:NonZero(Float):=-f f+(1.1::NonZero(Float)) f + -g f+g \end{axiom}
Algebra
Algebra
SandBoxNonZeroInteger is an attempt to define the domain of Integers without 0 as a SubDomain.
\begin{spad} )abbrev domain NZINT NonZeroInteger NonZeroInteger: Join(OrderedAbelianSemiGroup, Monoid --,CoercibleTo(Integer) ) with commutative("*") gcd: (%,%) -> % ++ gcd(a,b) computes the greatest common divisor of two ++ positive integers \spad{a} and b. _-: % -> % --retract:Integer->% --retractIfCan:Integer->Union(%,"failed") --retract:NonNegativeInteger->% --retractIfCan:NonNegativeInteger->Union(%,"failed") --convert:NonNegativeInteger->% == SubDomain(Integer,not(#1 = 0)) add Rep == Integer x:% y:% z:Integer nz:NonNegativeInteger -x == (-(x pretend Integer)) pretend % x+y == (z:=(x pretend Integer)+(y pretend Integer)) = 0 => error "zero" z pretend %
--coerce(x):Integer == x pretend Integer --retract(z)== z pretend % --convert(nz):% == retract(nz) --retractIfCan(z) == -- zero?(z) => "failed" -- retract(z) --retract(nz)== nz pretend % --retractIfCan(nz) == -- zero?(nz) => "failed" -- retract(nz) \end{spad}
\begin{axiom} )show NZINT \end{axiom}
\begin{axiom} i:NZINT := 1$NZINT i:NZINT := (1::Integer) i:NZINT := 1 \end{axiom} \begin{axiom} j:NZINT := -1 \end{axiom} \begin{axiom} j:NZINT:=-i i+1 j+1 i+j \end{axiom}
\begin{axiom} i-j retractIfCan(0)$NZINT \end{axiom}
Can we define NonZero as a functor?
\begin{spad}
)abbrev domain NZ NonZero
NonZero(T:Ring): Join(OrderedAbelianSemiGroup, Monoid) with
Commutative("*")
_-: % -> %
== SubDomain(T,not(#1 = 0)) add
Rep == T
x:%
y:%
z:T
-x == (-(x pretend T)) pretend %
x+y ==
(z:=(x pretend T)+(y pretend T)) = 0 => error "zero"
z pretend %
\end{spad}
\begin{axiom} )show NonZero(Float) \end{axiom}
\begin{axiom} f:NonZero(Float):=1 g:NonZero(Float):=-f f+(1.1::NonZero(Float)) f + -g f+g \end{axiom}
Some or all expressions may not have rendered properly, because Axiom returned the following error:
Error: export FRICAS=/usr/local/lib/open-axiom/x86_64-unknown-linux/1.3.0-2009-01-05; export ALDORROOT=/usr/local/aldor/linux/1.1.0; export PATH=$ALDORROOT/bin:$PATH; export HOME=/var/zope2/var/LatexWiki; ulimit -t 600; export LD_LIBRARY_PATH=/usr/local/lib/open-axiom/x86_64-unknown-linux/1.3.0-2009-01-05/lib; LANG=en_US.UTF-8 $FRICAS/bin/FRICASsys < /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3437484353503122027-25px.axm /bin/sh: /usr/local/lib/open-axiom/x86_64-unknown-linux/1.3.0-2009-01-05/bin/FRICASsys: not found
Some or all expressions may not have rendered properly, because Latex returned the following error:
This is pdfTeXk, Version 3.141592-1.40.3 (Web2C 7.5.6) \write18 enabled. %&-line parsing enabled. entering extended mode (./7851149973523920894-16.0px.tex LaTeX2e <2005/12/01> Babel <v3.8h> and hyphenation patterns for english, usenglishmax, dumylang, noh yphenation, arabic, farsi, croatian, ukrainian, russian, bulgarian, czech, slov ak, danish, dutch, finnish, basque, french, german, ngerman, ibycus, greek, mon ogreek, ancientgreek, hungarian, italian, latin, mongolian, norsk, icelandic, i nterlingua, turkish, coptic, romanian, welsh, serbian, slovenian, estonian, esp eranto, uppersorbian, indonesian, polish, portuguese, spanish, catalan, galicia n, swedish, ukenglish, pinyin, loaded. (/usr/share/texmf-texlive/tex/latex/base/article.cls Document Class: article 2005/09/16 v1.4f Standard LaTeX document class (/usr/share/texmf-texlive/tex/latex/base/size12.clo)) (/usr/share/texmf-texlive/tex/latex/ucs/ucs.sty (/usr/share/texmf-texlive/tex/latex/ucs/data/uni-global.def)) (/usr/share/texmf-texlive/tex/latex/base/inputenc.sty (/usr/share/texmf-texlive/tex/latex/ucs/utf8x.def)) (/usr/share/texmf-texlive/tex/latex/bbm/bbm.sty) (/usr/share/texmf-texlive/tex/latex/jknapltx/mathrsfs.sty) (/usr/share/texmf-texlive/tex/latex/base/fontenc.sty (/usr/share/texmf-texlive/tex/latex/base/t1enc.def)) (/usr/share/texmf-texlive/tex/latex/pstricks/pstricks.sty (/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.tex `PSTricks' v1.15 <2006/12/22> (tvz) (/usr/share/texmf-texlive/tex/generic/pstricks/pstricks.con)) (/usr/share/texmf/tex/latex/xcolor/xcolor.sty (/etc/texmf/tex/latex/config/color.cfg) (/usr/share/texmf-texlive/tex/latex/graphics/dvips.def) (/usr/share/texmf-texlive/tex/latex/graphics/dvipsnam.def))) (/usr/share/texmf-texlive/tex/latex/graphics/epsfig.sty (/usr/share/texmf-texlive/tex/latex/graphics/graphicx.sty (/usr/share/texmf-texlive/tex/latex/graphics/keyval.sty) (/usr/share/texmf-texlive/tex/latex/graphics/graphics.sty (/usr/share/texmf-texlive/tex/latex/graphics/trig.sty) (/etc/texmf/tex/latex/config/graphics.cfg)))) (/usr/share/texmf-texlive/tex/latex/pst-grad/pst-grad.sty (/usr/share/texmf-texlive/tex/generic/pst-grad/pst-grad.tex (/usr/share/texmf-texlive/tex/latex/xkeyval/pst-xkey.tex (/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.sty (/usr/share/texmf-texlive/tex/latex/xkeyval/xkeyval.tex))) `pst-plot' v1.05, 2006/11/04 (tvz,dg,hv))) (/usr/share/texmf-texlive/tex/latex/pstricks/pst-plot.sty (/usr/share/texmf-texlive/tex/generic/pstricks/pst-plot.tex v97 patch 2, 1999/12/12 (/usr/share/texmf-texlive/tex/generic/multido/multido.tex v1.41, 2004/05/18 <tvz>))) (/usr/share/texmf-texlive/tex/latex/geometry/geometry.sty (/usr/share/texmf-texlive/tex/xelatex/xetexconfig/geometry.cfg)Package geometry Warning: `lmargin' and `rmargin' result in NEGATIVE (-108.405p t). `width' should be shortened in length.
) (/usr/share/texmf-texlive/tex/latex/amsmath/amsmath.sty For additional information on amsmath, use the `?
option. (/usr/share/texmf-texlive/tex/latex/amsmath/amstext.sty (/usr/share/texmf-texlive/tex/latex/amsmath/amsgen.sty)) (/usr/share/texmf-texlive/tex/latex/amsmath/amsbsy.sty) (/usr/share/texmf-texlive/tex/latex/amsmath/amsopn.sty)) (/usr/share/texmf-texlive/tex/latex/amsfonts/amsfonts.sty) (/usr/share/texmf-texlive/tex/latex/amsfonts/amssymb.sty) (/usr/share/texmf-texlive/tex/latex/amscls/amsthm.sty) (/usr/share/texmf-texlive/tex/latex/setspace/setspace.sty Package: `setspace6.7 <2000/12/01> ) (/usr/share/texmf-texlive/tex/generic/xypic/xy.sty (/usr/share/texmf-texlive/tex/generic/xypic/xy.tex Bootstrap'ing: catcodes, docmode, (/usr/share/texmf-texlive/tex/generic/xypic/xyrecat.tex) (/usr/share/texmf-texlive/tex/generic/xypic/xyidioms.tex)Xy-pic version 3.7 <1999/02/16> Copyright (c) 1991-1998 by Kristoffer H. Rose <krisrose@ens-lyon.fr> Xy-pic is free software: see the User's Guide for details.
Loading kernel: messages; fonts; allocations: state, direction, utility macros; pictures: \xy, positions, objects, decorations; kernel objects: directionals, circles, text; options; algorithms: directions, edges, connections; Xy-pic loaded)) (/usr/share/texmf-texlive/tex/generic/xypic/xyall.tex Xy-pic option: All features v.3.3 (/usr/share/texmf-texlive/tex/generic/xypic/xycurve.tex Xy-pic option: Curve and Spline extension v.3.7 curve, circles, loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyframe.tex Xy-pic option: Frame and Bracket extension v.3.7 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xycmtip.tex Xy-pic option: Computer Modern tip extension v.3.3 (/usr/share/texmf-texlive/tex/generic/xypic/xytips.tex Xy-pic option: More Tips extension v.3.3 loaded) loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyline.tex Xy-pic option: Line styles extension v.3.6 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyrotate.tex Xy-pic option: Rotate and Scale extension v.3.3 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xycolor.tex Xy-pic option: Colour extension v.3.3 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xymatrix.tex Xy-pic option: Matrix feature v.3.4 loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xyarrow.tex Xy-pic option: Arrow and Path feature v.3.5 path, \ar, loaded) (/usr/share/texmf-texlive/tex/generic/xypic/xygraph.tex Xy-pic option: Graph feature v.3.7 loaded) loaded) (/usr/share/texmf-texlive/tex/latex/tools/verbatim.sty) (/usr/share/texmf/tex/latex/graphviz/graphviz.sty (/usr/share/texmf-texlive/tex/latex/psfrag/psfrag.sty)) (/usr/share/texmf/tex/latex/sagetex.sty Writing sage input file 7851149973523920894-16.0px.sage (./7851149973523920894-16.0px.sout)) (/usr/share/texmf-texlive/tex/latex/gnuplottex/gnuplottex.sty (/usr/share/texmf-texlive/tex/latex/base/latexsym.sty) (/usr/share/texmf-texlive/tex/latex/moreverb/moreverb.sty) (/usr/share/texmf-texlive/tex/latex/base/ifthen.sty)) (./7851149973523920894-16.0px.aux) (/usr/share/texmf-texlive/tex/latex/ucs/ucsencs.def) Missing $ inserted. <inserted text> $ l.130 _ -: % -> % (/usr/share/texmf-texlive/tex/latex/jknapltx/ursfs.fd) (/usr/share/texmf-texlive/tex/latex/amsfonts/umsa.fd) (/usr/share/texmf-texlive/tex/latex/amsfonts/umsb.fd) (/usr/share/texmf-texlive/tex/latex/base/ulasy.fd) You can't use `macro parameter character #' in math mode. l.136 == SubDomain(Integer,not(# 1 = 0)) add Missing $ inserted. <inserted text> $ l.146
[1] (/usr/share/texmf-texlive/tex/latex/base/t1cmtt.fd)
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 160.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 165.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 168.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 174.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 178.
Missing $ inserted. <inserted text> $ l.183 _ -: % -> % You can't use `macro parameter character #' in math mode. l.184 == SubDomain(T,not(# 1 = 0)) add Missing $ inserted. <inserted text> $ l.193 \end{spad} \newpage
Overfull \hbox (19.6396pt too wide) in paragraph at lines 180--193 \T1/cmr/m/n/12 )abbrev do-main NZ NonZero NonZero(T:Ring): Join(OrderedAbelianS emiGroup, Monoid) with Com-mu-ta-tive("*") $[] \OT1/cmr/m/n/12 :== \OML/cmm/m/i t/12 SubDomain\OT1/cmr/m/n/12 (\OML/cmm/m/it/12 T; not\OT1/cmr/m/n/12 (1 = [2]
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 196.
LaTeX Warning: Characters dropped after `\end{axiom}' on input line 203.
[3] (./7851149973523920894-16.0px.aux) ) (see the transcript file for additional information) Output written on 7851149973523920894-16.0px.dvi (3 pages, 3368 bytes). Transcript written on 7851149973523920894-16.0px.log.