help links subscribe changes refresh edit

	Manipulating Expressions
	↑

SandBoxDomainOfComputation

Edit detail for SandBoxDomainOfComputation revision 2 of 7

	1 2 3 4 5 6 7
Editor: Bill Page Time: 2017/04/13 16:38:17 GMT+0
Note: subtypes

added:
And "assume" system based on equational reasoning.

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

changed:
-  assume(x,'positiveInteger)+(y|integer?(y) and integer(y)>=0) == assume(x+y,'positiveInteger)
  -- subtypes
  assume(assume(x,'integer),'integer) == assume(x,'integer)
  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)
  -- 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)

added:
  assume(x,'positiveInteger)+assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)

changed:
-  k:=retractIfCan(prove x)@Union(Kernel Expression Integer,"failed")
-  if k case Kernel Expression Integer then is?(k,t) else false
  --k:=retractIfCan(prove markConstants x)@Union(Kernel Expression Integer,"failed")
  --if k case Kernel Expression Integer then is?(k,t) else false
  prove markConstants x = assume(x,t)

added:
prove %
assume(assume(x,'positiveInteger),'integer)

And "assume" system based on equational reasoning.

fricas

(1) -> 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 ==
  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,'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)
  -- 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\{{= = \left({{integer \left({integer \left({x}\right)}\right)}, \:{integer \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{integer \left({nonNegativeInteger \left({x}\right)}\right)}, \:{integer \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{integer \left({positiveInteger \left({x}\right)}\right)}, \:{integer \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{nonNegativeInteger \left({nonNegativeInteger \left({x}\right)}\right)}, \:{nonNegativeinteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{nonNegativeInteger \left({positiveInteger \left({x}\right)}\right)}, \:{nonNegativeInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{{integer \left({y}\right)}+{integer \left({x}\right)}+ \%B}, \:{{integer \left({y + x}\right)}+ \%B}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{nonNegativeInteger \left({y}\right)}+{integer \left({x}\right)}+ \%C}, \:{{integer \left({y + x}\right)}+ \%C}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({y}\right)}+{integer \left({x}\right)}+ \%D}, \:{{integer \left({y + x}\right)}+ \%D}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{nonNegativeInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%E}, \:{{nonNegativeInteger \left({y + x}\right)}+ \%E}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%F}, \:{{nonNegativeInteger \left({y + x}\right)}+ \%F}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({y}\right)}+{positiveInteger \left({x}\right)}+ \%G}, \:{{positiveInteger \left({y + x}\right)}+ \%G}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({x}\right)}+{nonNegativeInteger \left({y}\right)}+ \%H}, \:{{positiveInteger \left({y + x}\right)}+ \%H}}\right)}\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
  prove markConstants x = assume(x,t)

   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(assume(x,'positiveInteger),'integer)

$\label{eq5}integer \left({positiveInteger \left({x}\right)}\right)$

(5)

Type: Expression(Integer)

fricas

prove %

$\label{eq6}integer \left({x}\right)$

(6)

Type: Expression(Integer)

fricas

check(assume(x,'positiveInteger),'positiveInteger)

fricas

Compiling function markConstants with type Expression(Integer) -> 
      Expression(Integer)

fricas

Compiling function check with type (Expression(Integer), Symbol) -> 
      Boolean

$\label{eq7} \mbox{\rm false}$

(7)

Type: Boolean

fricas

check(assume(x,'positiveInteger)+1,'positiveInteger)

$\label{eq8} \mbox{\rm false}$

(8)

Type: Boolean

fricas

check(3,'positiveInteger)

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

(9)

Type: Boolean

fricas

domains

$\label{eq10} \mbox{\rm table} \left({{nonNegativeinteger = nonNegativeinteger}, \:{positiveInteger = positiveInteger}, \:{nonNegativeInteger = nonNegativeInteger}, \:{integer = integer}}\right)$

(10)

Type: Table(Symbol,BasicOperator?)