help links subscribe changes refresh edit

	Manipulating Expressions
	↑

SandBoxDomainOfComputation

Edit detail for SandBoxDomainOfComputation revision 1 of 7

	1 2 3 4 5 6 7
Editor: Bill Page Time: 2017/04/13 14:56:33 GMT+0
Note:

changed:
-
\begin{axiom}
domains:=empty()$Table(Symbol,BasicOperator)
assume(x:Expression Integer,t:Symbol):Expression Integer ==
  if not key?(t,domains) then domains.t := operator t
  (domains.t) x
prove := rule
  assume(x,'positiveInteger)+(y|integer?(y) and integer(y)>=0) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger)+assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
check(x:Expression Integer,t:Symbol):Boolean ==
  k:=retractIfCan(prove x)@Union(Kernel Expression Integer,"failed")
  if k case Kernel Expression Integer then is?(k,t) else false
\end{axiom}

\begin{axiom}
assume(x,'positiveInteger)
prove %
check(assume(x,'positiveInteger),'positiveInteger)
check(assume(x,'positiveInteger)+1,'positiveInteger)
check(3,'positiveInteger)
domains
\end{axiom}

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

prove := rule
  assume(x,'positiveInteger)+(y|integer?(y) and integer(y)>=0) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger)+assume(y,'positiveInteger) == assume(x+y,'positiveInteger)

fricas

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

$\label{eq2}\begin{array}{@{}l} \displaystyle \left\{{{{positiveInteger \left({x}\right)}+ y}\mbox{\rm = =}{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{{{positiveInteger \left({y}\right)}+{positiveInteger \left({x}\right)}+ \%B}\mbox{\rm = =}{{{{\tt'}assume}\left({{y + x}, \: positiveInteger}\right)}+ \%B}}\right\}$

(2)

Type: Ruleset(Integer,Integer,Expression(Integer))

fricas

check(x:Expression Integer,t:Symbol):Boolean ==
  k:=retractIfCan(prove x)@Union(Kernel Expression Integer,"failed")
  if k case Kernel Expression Integer then is?(k,t) else false

   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

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

fricas

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

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

(5)

Type: Boolean

fricas

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

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

(6)

Type: Boolean

fricas

check(3,'positiveInteger)

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

(7)

Type: Boolean

fricas

domains

$\label{eq8} \mbox{\rm table} \left({positiveInteger = positiveInteger}\right)$

(8)

Type: Table(Symbol,BasicOperator?)