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

Edit detail for SandBoxDomainOfComputation revision 3 of 7

1 2 3 4 5 6 7
Editor: Bill Page
Time: 2017/04/13 19:53:22 GMT+0
Note: subtypes

added:
  -- cache operators

changed:
-  assume(assume(x,'nonNegativeInteger),'integer) == assume(x,'integer)
-  assume(assume(x,'positiveInteger),'integer) == assume(x,'integer)
-  assume(assume(x,'nonNegativeInteger),'nonNegativeInteger) == assume(x,'nonNegativeinteger)
-  assume(assume(x,'positiveInteger),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'integer),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'integer),'positiveInteger) == assume(x,'positiveInteger)
  --
  assume(assume(x,'nonNegativeInteger),'integer) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'positiveInteger) == assume(x,'positiveInteger)
  --
  assume(assume(x,'positiveInteger),'integer) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'positiveInteger) == assume(x,'positiveInteger)

changed:
-  prove markConstants x = assume(x,t)
  p := prove markConstants x
  e := equation(p, prove markConstants assume(p,t))
  output e
  e


changed:
-assume(assume(x,'positiveInteger),'integer)
assume(x,'positiveInteger)+1
prove markConstants %
assume(assume(x,'nonNegativeInteger),'positiveInteger)

added:
check(-3,'positiveInteger)
check(0,'positiveInteger)
--
assume(x,'nonNegativeInteger)
prove %
check(assume(x,'positiveInteger),'nonNegativeInteger)
assume(x,'nonNegativeInteger)+1
prove markConstants %
assume(assume(x,'integer),'nonNegativeInteger)
prove %
check(assume(x,'nonNegativeInteger),'nonNegativeInteger)
check(assume(x,'nonNegativeInteger)+1,'nonNegativeInteger)
check(3,'nonNegativeInteger)
check(-3,'nonNegativeInteger)
check(0,'nonNegativeInteger)
--
assume(x,'integer)
prove %
check(assume(x,'positiveInteger),'integer)
assume(x,'integer)+1
prove markConstants %
assume(assume(x,'integer),'integer)
prove %
check(assume(x,'integer),'integer)
check(assume(x,'integer)+1,'integer)
check(3,'integer)
check(-3,'integer)
check(0,'integer)

And "assume" system based on equational reasoning.

fricas
domains:=empty()$Table(Symbol,BasicOperator)

\label{eq1} \mbox{\rm table} \left({}\right)(1)
Type: Table(Symbol,BasicOperator?)
fricas
assume(x:Expression Integer,t:Symbol):Expression Integer ==
  -- cache operators
  if not key?(t,domains) then domains.t := operator t
  (domains.t) x
Function declaration assume : (Expression(Integer),Symbol) -> Expression(Integer) has been added to workspace.
Type: Void
fricas
markConstants(x:Expression Integer):Expression Integer ==
  if (s:=isPlus(x)) case List Expression Integer then
    return reduce(+,[markConstants i for i in s::List Expression Integer])
  if (s:=isTimes(x)) case List Expression Integer then
    return reduce(*,[markConstants i for i in s::List Expression Integer])
  if (r:=retractIfCan(x)@Union(Integer,"failed")) case Integer then
    if r<0 then return assume(x,'integer)
    if r>0 then return assume(x,'positiveInteger)
    return assume(x, 'nonNegativeInteger)
  return x
Function declaration markConstants : Expression(Integer) -> Expression(Integer) has been added to workspace.
Type: Void
fricas
prove := rule
  -- subtypes
  assume(assume(x,'integer),'integer) == assume(x,'integer)
  assume(assume(x,'integer),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'integer),'positiveInteger) == assume(x,'positiveInteger)
  --
  assume(assume(x,'nonNegativeInteger),'integer) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'nonNegativeInteger) == assume(x,'nonNegativeInteger)
  assume(assume(x,'nonNegativeInteger),'positiveInteger) == assume(x,'positiveInteger)
  --
  assume(assume(x,'positiveInteger),'integer) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'positiveInteger),'positiveInteger) == assume(x,'positiveInteger)
  -- operations
  assume(x,'integer) + assume(y,'integer) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'nonNegativeInteger) == assume(x+y,'integer)
  assume(x,'integer) + assume(y,'positiveInteger) == assume(x+y,'integer)
  assume(x,'nonNegativeInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'nonNegativeInteger)
  assume(x,'positiveInteger)+assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger)+assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
fricas
Compiling function assume with type (Expression(Integer),Symbol) -> 
      Expression(Integer)

\label{eq2}\begin{array}{@{}l}
\displaystyle
\left\{{{integer \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: integer}\right)}}, \: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({integer \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{integer \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: nonNegativeInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{integer \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{nonNegativeInteger \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{positiveInteger \left({positiveInteger \left({x}\right)}\right)}\mbox{\rm = =}{{{\tt'}assume}\left({x , \: positiveInteger}\right)}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{integer \left({y}\right)}+{integer \left({x}\right)}+ \%B}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%B}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonNegativeInteger \left({y}\right)}+{integer \left({x}\right)}+ \%C}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%C}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({y}\right)}+{integer \left({x}\right)}+ \%D}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: integer}\right)}+ \%D}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{nonNegativeInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%E}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: nonNegativeInteger}\right)}+ \%E}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%F}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: nonNegativeInteger}\right)}+ \%F}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({y}\right)}+{positiveInteger \left({x}\right)}+ \%G}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%G}}, \right.
\
\
\displaystyle
\left.\: \right.
\
\
\displaystyle
\left.{{{positiveInteger \left({x}\right)}+{nonNegativeInteger \left({y}\right)}+ \%H}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%H}}\right\} 
(2)
Type: Ruleset(Integer,Integer,Expression(Integer))
fricas
check(x:Expression Integer,t:Symbol):Boolean ==
  --k:=retractIfCan(prove markConstants x)@Union(Kernel Expression Integer,"failed")
  --if k case Kernel Expression Integer then is?(k,t) else false
  p := prove markConstants x
  e := equation(p, prove markConstants assume(p,t))
  output e
  e
Function declaration check : (Expression(Integer),Symbol) -> Boolean has been added to workspace.
Type: Void

fricas
assume(x,'positiveInteger)

\label{eq3}positiveInteger \left({x}\right)(3)
Type: Expression(Integer)
fricas
prove %

\label{eq4}positiveInteger \left({x}\right)(4)
Type: Expression(Integer)
fricas
assume(x,'positiveInteger)+1

\label{eq5}{positiveInteger \left({x}\right)}+ 1(5)
Type: Expression(Integer)
fricas
prove markConstants %
fricas
Compiling function markConstants with type Expression(Integer) -> 
      Expression(Integer)

\label{eq6}positiveInteger \left({x + 1}\right)(6)
Type: Expression(Integer)
fricas
assume(assume(x,'nonNegativeInteger),'positiveInteger)

\label{eq7}positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)(7)
Type: Expression(Integer)
fricas
prove %

\label{eq8}positiveInteger \left({x}\right)(8)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'positiveInteger)
fricas
Compiling function check with type (Expression(Integer),Symbol) -> 
      Boolean 
   positiveInteger(x) = positiveInteger(x)

\label{eq9} \mbox{\rm true} (9)
Type: Boolean
fricas
check(assume(x,'positiveInteger)+1,'positiveInteger)
positiveInteger(x + 1) = positiveInteger(x + 1)

\label{eq10} \mbox{\rm true} (10)
Type: Boolean
fricas
check(3,'positiveInteger)
positiveInteger(3) = positiveInteger(3)

\label{eq11} \mbox{\rm true} (11)
Type: Boolean
fricas
check(-3,'positiveInteger)
integer(- 3) = positiveInteger(- 3)

\label{eq12} \mbox{\rm false} (12)
Type: Boolean
fricas
check(0,'positiveInteger)
nonNegativeInteger(0) = positiveInteger(0)

\label{eq13} \mbox{\rm false} (13)
Type: Boolean
fricas
--
assume(x,'nonNegativeInteger)

\label{eq14}nonNegativeInteger \left({x}\right)(14)
Type: Expression(Integer)
fricas
prove %

\label{eq15}nonNegativeInteger \left({x}\right)(15)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'nonNegativeInteger)
positiveInteger(x) = positiveInteger(x)

\label{eq16} \mbox{\rm true} (16)
Type: Boolean
fricas
assume(x,'nonNegativeInteger)+1

\label{eq17}{nonNegativeInteger \left({x}\right)}+ 1(17)
Type: Expression(Integer)
fricas
prove markConstants %

\label{eq18}positiveInteger \left({x + 1}\right)(18)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'nonNegativeInteger)

\label{eq19}nonNegativeInteger \left({integer \left({x}\right)}\right)(19)
Type: Expression(Integer)
fricas
prove %

\label{eq20}nonNegativeInteger \left({x}\right)(20)
Type: Expression(Integer)
fricas
check(assume(x,'nonNegativeInteger),'nonNegativeInteger)
nonNegativeInteger(x) = nonNegativeInteger(x)

\label{eq21} \mbox{\rm true} (21)
Type: Boolean
fricas
check(assume(x,'nonNegativeInteger)+1,'nonNegativeInteger)
positiveInteger(x + 1) = positiveInteger(x + 1)

\label{eq22} \mbox{\rm true} (22)
Type: Boolean
fricas
check(3,'nonNegativeInteger)
positiveInteger(3) = positiveInteger(3)

\label{eq23} \mbox{\rm true} (23)
Type: Boolean
fricas
check(-3,'nonNegativeInteger)
integer(- 3) = nonNegativeInteger(- 3)

\label{eq24} \mbox{\rm false} (24)
Type: Boolean
fricas
check(0,'nonNegativeInteger)
nonNegativeInteger(0) = nonNegativeInteger(0)

\label{eq25} \mbox{\rm true} (25)
Type: Boolean
fricas
--
assume(x,'integer)

\label{eq26}integer \left({x}\right)(26)
Type: Expression(Integer)
fricas
prove %

\label{eq27}integer \left({x}\right)(27)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'integer)
positiveInteger(x) = positiveInteger(x)

\label{eq28} \mbox{\rm true} (28)
Type: Boolean
fricas
assume(x,'integer)+1

\label{eq29}{integer \left({x}\right)}+ 1(29)
Type: Expression(Integer)
fricas
prove markConstants %

\label{eq30}integer \left({x + 1}\right)(30)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'integer)

\label{eq31}integer \left({integer \left({x}\right)}\right)(31)
Type: Expression(Integer)
fricas
prove %

\label{eq32}integer \left({x}\right)(32)
Type: Expression(Integer)
fricas
check(assume(x,'integer),'integer)
integer(x) = integer(x)

\label{eq33} \mbox{\rm true} (33)
Type: Boolean
fricas
check(assume(x,'integer)+1,'integer)
integer(x + 1) = integer(x + 1)

\label{eq34} \mbox{\rm true} (34)
Type: Boolean
fricas
check(3,'integer)
positiveInteger(3) = positiveInteger(3)

\label{eq35} \mbox{\rm true} (35)
Type: Boolean
fricas
check(-3,'integer)
integer(- 3) = integer(- 3)

\label{eq36} \mbox{\rm true} (36)
Type: Boolean
fricas
check(0,'integer)
nonNegativeInteger(0) = nonNegativeInteger(0)

\label{eq37} \mbox{\rm true} (37)
Type: Boolean
fricas
domains

\label{eq38} \mbox{\rm table} \left({{positiveInteger = positiveInteger}, \:{nonNegativeInteger = nonNegativeInteger}, \:{integer = integer}}\right)(38)
Type: Table(Symbol,BasicOperator?)