help links subscribe changes refresh edit

	SandBox	SubDomain
SandBoxNonAssociativeAlgebra ←	↑		→ SandBoxObserverAsIdempotent

SandBoxNonZeroInteger

Edit detail for SandBoxNonZeroInteger revision 3 of 4

	1 2 3 4
Editor: Bill Page Time: 2008/12/03 10:31:38 GMT-8
Note: NonZero in general

added:
Can we define 'NonZero' as a functor?
\begin{spad}
)abbrev domain NZ NonZero
NonZero(T:Ring): Join(OrderedAbelianSemiGroup, Monoid, CommutativeStar) with
    _-: % -> %
 == SubDomain(T,#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

SandBoxNonZeroInteger? is an attempt to define the domain of Integers without 0 as a SubDomain?.

spad

)abbrev domain NZINT NonZeroInteger
NonZeroInteger: Join(OrderedAbelianSemiGroup, Monoid, CommutativeStar
                     --,CoercibleTo(Integer)
                    ) with
            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,#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)

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/3042217120178961765-25px001.spad using 
      old system compiler.
   NZINT abbreviates domain NonZeroInteger 
------------------------------------------------------------------------
   initializing NRLIB NZINT for NonZeroInteger 
   compiling into NRLIB NZINT 
   compiling exported - : $ -> $
      NZINT;-;2$;1 is replaced by - 
Time: 0.06 SEC.

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

(time taken in buildFunctor:  10)

;;;     ***       |NonZeroInteger| REDEFINED

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

   Cumulative Statistics for Constructor NonZeroInteger
      Time: 0.08 seconds

--------------non extending category----------------------
.. NonZeroInteger of cat 
(|Join| (|OrderedAbelianSemiGroup|) (|Monoid|) (|CommutativeStar|)
        (CATEGORY |domain| (SIGNATURE |gcd| ($ $ $)) (SIGNATURE - ($ $))))   has no 
(|IntegerNumberSystem|)    finalizing NRLIB NZINT 
   Processing NonZeroInteger for Browser database:
--------(gcd (% % %))---------
--->-->NonZeroInteger((- (% %))): Not documented!!!!
--->-->NonZeroInteger(constructor): Not documented!!!!
--->-->NonZeroInteger(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/NZINT.NRLIB/NZINT.lsp" (written 16 APR 2011 04:39:51 AM):

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

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

Built-in

There are at least two places where critical knowledge of sub-domains is built into FriCAS?.

In src/interp/i-util.boot we must extend the 'subDomainList':

boot

isSubDomain(d1,d2) ==
  -- d1 and d2 are different domains
  --subDomainList := '(Integer NonNegativeInteger PositiveInteger)
  subDomainList := '(Integer NonZeroInteger NonNegativeInteger PositiveInteger)
  ATOM d1 or ATOM d2 => nil
  l := MEMQ(CAR d2, subDomainList) =>
    MEMQ(CAR d1, CDR l)
  nil

boot

Value = T
; compiling file "/var/zope2/var/LatexWiki/1905831235319360423-25px002.clisp" (written 16 APR 2011 04:39:52 AM):

; /var/zope2/var/LatexWiki/1905831235319360423-25px002.fasl written
; compilation finished in 0:00:00.015
Value = T

In src/interp/daase.lisp we need to make sure NonZeroInteger is known to have a 'superdomain':

lisp

(defun getdatabase (constructor key)
 (declare (special $spadroot) (special *miss*))
 (when (eq *miss* t) (format t "getdatabase call: ~20a ~a~%" constructor key))
 (let (data table stream ignore struct)
  (declare (ignore ignore))
  (when (or (symbolp constructor)
          (and (eq key 'hascategory) (pairp constructor)))
  (case key
; note that abbreviation, constructorkind and cosig are heavy hitters
; thus they occur first in the list of things to check
   (abbreviation
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
      (setq data (database-abbreviation struct))))
   (constructorkind
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-constructorkind struct))))
   (cosig
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-cosig struct))))
   (operation
    (setq stream *operation-stream*)
    (setq data (gethash constructor *operation-hash*)))
   (constructormodemap
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-constructormodemap struct))))
   (constructorcategory
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-constructorcategory struct))
     (when (null data) ;domain or package then subfield of constructormodemap
      (setq data (cadar (getdatabase constructor 'constructormodemap))))))
   (operationalist
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-operationalist struct))))
   (modemaps
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-modemaps struct))))
   (hascategory
    (setq table  *hasCategory-hash*)
    (setq stream *category-stream*)
    (setq data (gethash constructor table)))
   (object
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-object struct))))
   (asharp?
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-object struct))))
   (niladic
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-niladic struct))))
   (constructor?
    (when (setq struct (get constructor 'database))
      (setq data (when (database-operationalist struct) t))))

   ;(superdomain ; only 2 superdomains in the world
   ; (case constructor
   ;  (|NonNegativeInteger|
   ;   (setq data '((|Integer|) (IF (< |#1| 0) |false| |true|))))
   ;  (|PositiveInteger|
   ;   (setq data '((|NonNegativeInteger|) (< 0 |#1|))))))
   (superdomain ; 3 superdomains in the world
    (case constructor
     (|NonNegativeInteger|
      (setq data '((|Integer|) (IF (< |#1| 0) |false| |true|))))
     (|NonZeroInteger|
      (setq data '((|Integer|) (IF (= |#1| 0) |false| |true|))))
     (|PositiveInteger|
      (setq data '((|NonZeroInteger|) (< 0 |#1|))))))

   (constructor
    (when (setq data (get constructor 'abbreviationfor))))
   (defaultdomain
    (setq data (cadr (assoc constructor *defaultdomain-list*))))
   (ancestors
    (setq stream *interp-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-ancestors struct))))
   (sourcefile
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-sourcefile struct))))
   (constructorform
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-constructorform struct))))
   (constructorargs
    (setq data (cdr (getdatabase constructor 'constructorform))))
   (attributes
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-attributes struct))))
   (predicates
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-predicates struct))))
   (documentation
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-documentation struct))))
   (parents
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-parents struct))))
   (users
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-users struct))))
   (dependents
    (setq stream *browse-stream*)
    (when (setq struct (get constructor 'database))
     (setq data (database-dependents struct))))
   (otherwise  (warn "~%(GETDATABASE ~a ~a) failed~%" constructor key)))
  (when (numberp data)                 ;fetch the real data
   (when *miss* (format t "getdatabase miss: ~20a ~a~%" constructor key))
   (file-position stream data)
   (setq data (unsqueeze (read stream)))
   (case key ; cache the result of the database read
    (operation           (setf (gethash constructor *operation-hash*) data))
    (hascategory         (setf (gethash constructor *hascategory-hash*) data))
    (constructorkind     (setf (database-constructorkind struct) data))
    (cosig               (setf (database-cosig struct) data))
    (constructormodemap  (setf (database-constructormodemap struct) data))
    (constructorcategory (setf (database-constructorcategory struct) data))
    (operationalist      (setf (database-operationalist struct) data))
    (modemaps            (setf (database-modemaps struct) data))
    (object              (setf (database-object struct) data))
    (niladic             (setf (database-niladic struct) data))
    (abbreviation        (setf (database-abbreviation struct) data))
    (constructor         (setf (database-constructor struct) data))
    (ancestors           (setf (database-ancestors struct) data))
    (constructorform     (setf (database-constructorform struct) data))
    (attributes          (setf (database-attributes struct) data))
    (predicates          (setf (database-predicates struct) data))
    (documentation       (setf (database-documentation struct) data))
    (parents             (setf (database-parents struct) data))
    (users               (setf (database-users struct) data))
    (dependents          (setf (database-dependents struct) data))
    (sourcefile          (setf (database-sourcefile struct) data))))
   (case key ; fixup the special cases
    (sourcefile
     (when (and data (string= (directory-namestring data) "")
             (string= (pathname-type data) "spad"))

      (setq data
       (concatenate 'string $spadroot "/../../src/algebra/" data))))
    (asharp?                               ; is this asharp code?
     (if (consp data)
      (setq data (cdr data))
      (setq data nil)))
    (object                                ; fix up system object pathname
     (if (consp data)
       (setq data
             (if (string= (directory-namestring (car data)) "")
                 (concatenate 'string $spadroot "/algebra/" (car data)
                                        "." *lisp-bin-filetype*)
               (car data)))
      (when (and data (string= (directory-namestring data) ""))
       (setq data (concatenate 'string $spadroot "/algebra/" data
                                          "." *lisp-bin-filetype*)))))))
  data))

lisp

; compiling file "/var/zope2/var/LatexWiki/2574875374267770522-25px003.lisp" (written 16 APR 2011 04:39:51 AM):

; /var/zope2/var/LatexWiki/2574875374267770522-25px003.fasl written
; compilation finished in 0:00:00.257
Value = T

axiom

isSubDomain(devaluate(NonNegativeInteger)$Lisp,devaluate(Integer)$Lisp)$Lisp

$\label{eq1}\left(\hbox{\axiomType{NonNegativeInteger}\ } \ \hbox{\axiomType{PositiveInteger}\ } \right)$

(1)

Type: SExpression?

axiom

isSubDomain(devaluate(PositiveInteger)$Lisp,devaluate(Integer)$Lisp)$Lisp

$\label{eq2}\left(\hbox{\axiomType{PositiveInteger}\ } \right)$

(2)

Type: SExpression?

axiom

isSubDomain(devaluate(NonZeroInteger)$Lisp,devaluate(Integer)$Lisp)$Lisp

$\label{eq3}\left(\hbox{\axiomType{NonZeroInteger}\ } \ \hbox{\axiomType{NonNegativeInteger}\ } \ \hbox{\axiomType{PositiveInteger}\ } \right)$

(3)

Type: SExpression?

axiom

)show NZINT

 NonZeroInteger  is a domain constructor
 Abbreviation for NonZeroInteger is NZINT 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------
 ?*? : (%,%) -> %                      ?*? : (PositiveInteger,%) -> %
 ?+? : (%,%) -> %                      -? : % -> %
 ?<? : (%,%) -> Boolean                ?<=? : (%,%) -> Boolean
 ?=? : (%,%) -> Boolean                ?>? : (%,%) -> Boolean
 ?>=? : (%,%) -> Boolean               1 : () -> %
 ?^? : (%,PositiveInteger) -> %        coerce : % -> OutputForm
 gcd : (%,%) -> %                      hash : % -> SingleInteger
 latex : % -> String                   max : (%,%) -> %
 min : (%,%) -> %                      one? : % -> Boolean
 recip : % -> Union(%,"failed")        sample : () -> %
 smaller? : (%,%) -> Boolean           ?~=? : (%,%) -> Boolean
 ?^? : (%,NonNegativeInteger) -> %

axiom

i:NZINT := 1$NZINT

$\label{eq4}1$

(4)

Type: NonZeroInteger?

axiom

i:NZINT := (1::Integer)

axiom

Compiling function G704 with type Integer -> Boolean

$\label{eq5}1$

(5)

Type: NonZeroInteger?

axiom

i:NZINT := 1

$\label{eq6}1$

(6)

Type: NonZeroInteger?

axiom

j:NZINT := -1

$\label{eq7}- 1$

(7)

Type: NonZeroInteger?

axiom

j:NZINT:=-i

$\label{eq8}- 1$

(8)

Type: NonZeroInteger?

axiom

i+1

$\label{eq9}2$

(9)

Type: PositiveInteger?

axiom

j+1

$\label{eq10}0$

(10)

Type: NonNegativeInteger?

axiom

i+j

   >> Error detected within library code:
   zero

axiom

i-j

$\label{eq11}2$

(11)

Type: PositiveInteger?

axiom

retractIfCan(0)$NZINT

   The function retractIfCan is not implemented in NonZeroInteger .

Can we define NonZero as a functor?

spad

)abbrev domain NZ NonZero
NonZero(T:Ring): Join(OrderedAbelianSemiGroup, Monoid, CommutativeStar) with
    _-: % -> %
 == SubDomain(T,#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 %

spad

   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/5447585626363364429-25px010.spad using 
      old system compiler.
   NZ abbreviates domain NonZero 
------------------------------------------------------------------------
   initializing NRLIB NZ for NonZero 
   compiling into NRLIB NZ 
   compiling exported - : $ -> $
Time: 0.03 SEC.

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

(time taken in buildFunctor:  0)

;;;     ***       |NonZero| REDEFINED

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

   Cumulative Statistics for Constructor NonZero
      Time: 0.04 seconds

   finalizing NRLIB NZ 
   Processing NonZero for Browser database:
--->-->NonZero((- (% %))): Not documented!!!!
--->-->NonZero(constructor): Not documented!!!!
--->-->NonZero(): Missing Description
; compiling file "/var/zope2/var/LatexWiki/NZ.NRLIB/NZ.lsp" (written 16 APR 2011 04:39:52 AM):

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

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

axiom

)show NonZero(Float)

 NonZero(Float) is a domain constructor.
 Abbreviation for NonZero is NZ 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------

 ?*? : (PositiveInteger,%) -> %        ?*? : (%,%) -> %
 ?+? : (%,%) -> %                      -? : % -> %
 ?<? : (%,%) -> Boolean                ?<=? : (%,%) -> Boolean
 ?=? : (%,%) -> Boolean                ?>? : (%,%) -> Boolean
 ?>=? : (%,%) -> Boolean               1 : () -> %
 ?^? : (%,PositiveInteger) -> %        coerce : % -> OutputForm
 hash : % -> SingleInteger             latex : % -> String
 max : (%,%) -> %                      min : (%,%) -> %
 one? : % -> Boolean                   recip : % -> Union(%,"failed")
 sample : () -> %                      smaller? : (%,%) -> Boolean
 ?~=? : (%,%) -> Boolean              
 ?^? : (%,NonNegativeInteger) -> %

axiom

f:NonZero(Float):=1

$\label{eq12}1.0$

(12)

Type: NonZero?(Float)

axiom

g:NonZero(Float):=-f

$\label{eq13}-{1.0}$

(13)

Type: NonZero?(Float)

axiom

f+(1.1::NonZero(Float))

   Cannot convert from type Float to NonZero(Float) for value
   1.1

f + -g

$\label{eq14}2.0$

(14)

Type: NonZero?(Float)

axiom

f+g

   >> Error detected within library code:
   zero