help links subscribe changes refresh edit

	Manipulating Expressions
	↑

SandBoxDomainOfComputation

Edit detail for SandBoxDomainOfComputation revision 7 of 7

	1 2 3 4 5 6 7
Editor: Bill Page Time: 2017/04/14 01:30:14 GMT+0
Note: improve names

changed:
-And "assume" system based on equational reasoning.
An "assume" system based on equational reasoning.

**assume(x,T)** returns a kernel **T(x)** intended to be interpreted as *forall(x:T)*.

changed:
-domains:=empty()$Table(Symbol,BasicOperator)
domainOfComp:=empty()$Table(Symbol,BasicOperator)

changed:
-  if not key?(t,domains) then domains.t := operator t
-  (domains.t) x
--- default assumptions about constants
  if not key?(t,domainOfComp) then domainOfComp.t := operator t
  (domainOfComp.t) x
\end{axiom}

Default assumptions about constants.
\begin{axiom} 

changed:
-Inference rules
Inference rules.

changed:
-prove := rule
normalForm := rule

changed:
-check if x is in t
Check if x is in t.

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

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

changed:
-simplification
Simplification

added:
-- conditions in rules need to be unary functions

changed:
-  -- trig
  -- trig rules

changed:
-tests
Tests

changed:
-prove %
normalForm %

changed:
-prove markConstants %
normalForm markConstants %

changed:
-prove %
normalForm %

changed:
-prove %
normalForm %

changed:
-prove markConstants %
normalForm markConstants %

changed:
-prove %
normalForm %

changed:
-prove %
normalForm %

changed:
-prove markConstants %
normalForm markConstants %

changed:
-prove %
normalForm %

changed:
-dump type cache
Dump domain cache

changed:
-entries domains
---for i in members(domains)@List Record(key:Symbol,entry:BasicOperator) repeat output i
entries domainOfComp

An "assume" system based on equational reasoning.

assume(x,T) returns a kernel T(x) intended to be interpreted as forall(x:T).

fricas

(1) -> domainOfComp:=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,domainOfComp) then domainOfComp.t := operator t
  (domainOfComp.t) x

   Function declaration assume : (Expression(Integer), Symbol) -> 
      Expression(Integer) has been added to workspace.

Type: Void

Default assumptions about constants.

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

Inference rules.

fricas

normalForm := 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,'integer),'nonZero) == assume(x,'nonZero)
  --
  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,'nonNegativeInteger),'nonZero) == 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)
  assume(assume(x,'positiveInteger),'nonZero) == assume(x,'positive)
  --
  assume(assume(x,'nonZero),'integer) == assume(x,'nonZero)
  assume(assume(x,'nonZero),'nonNegativeInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'positiveInteger) == assume(x,'positiveInteger)
  assume(assume(x,'nonZero),'nonZero) == assume(x,'nonZero)
  -- 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,'integer) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonNegativeInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'nonNegativeInteger)
  assume(x,'nonNegativeInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'nonNegativeInteger) + assume(y,'nonZero) == assume(x+y, 'integer)
  assume(x,'positiveInteger) + assume(y,'positiveInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonNegativeInteger) == assume(x+y,'positiveInteger)
  assume(x,'positiveInteger) + assume(y,'nonZero) == assume(x+y,'integer)
  assume(x,'nonZero) + assume(y,'nonZero) == assume(x+y,'integer)
  --
  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,'integer) * assume(y,'nonZero) == 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,'nonNegativeInteger) * assume(y,'nonZero) == assume(x*y, 'integer)
  assume(x,'positiveInteger) * assume(y,'positiveInteger) == assume(x*y,'positiveInteger)
  assume(x,'positiveInteger) * assume(y,'nonNegativeInteger) == assume(x*y,'nonNegativeInteger)
  assume(x,'positiveInteger) * assume(y,'nonZero) == assume(x*y,'nonZero)
  assume(x,'nonZero) * assume(y,'nonZero) == assume(x*y,'nonZero)

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({{nonNegativeInteger \left({integer \left({x}\right)}\right)}, \:{nonNegativeInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{positiveInteger \left({integer \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{nonZero \left({integer \left({x}\right)}\right)}, \:{nonZero \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{integer \left({nonNegativeInteger \left({x}\right)}\right)}, \:{nonNegativeInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{nonNegativeInteger \left({nonNegativeInteger \left({x}\right)}\right)}, \:{nonNegativeInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{nonZero \left({nonNegativeInteger \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{integer \left({positiveInteger \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{nonNegativeInteger \left({positiveInteger \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{positiveInteger \left({positiveInteger \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{nonZero \left({positiveInteger \left({x}\right)}\right)}, \:{positive \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{integer \left({nonZero \left({x}\right)}\right)}, \:{nonZero \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{nonNegativeInteger \left({nonZero \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{positiveInteger \left({nonZero \left({x}\right)}\right)}, \:{positiveInteger \left({x}\right)}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{nonZero \left({nonZero \left({x}\right)}\right)}, \:{nonZero \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({{{nonZero \left({y}\right)}+{integer \left({x}\right)}+ \%E}, \:{{integer \left({y + x}\right)}+ \%E}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{nonNegativeInteger \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)}+{nonNegativeInteger \left({x}\right)}+ \%G}, \:{{positiveInteger \left({y + x}\right)}+ \%G}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{nonZero \left({y}\right)}+{nonNegativeInteger \left({x}\right)}+ \%H}, \:{{integer \left({y + x}\right)}+ \%H}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({y}\right)}+{positiveInteger \left({x}\right)}+ \%I}, \:{{positiveInteger \left({y + x}\right)}+ \%I}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({x}\right)}+{nonNegativeInteger \left({y}\right)}+ \%J}, \:{{positiveInteger \left({y + x}\right)}+ \%J}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{positiveInteger \left({x}\right)}+{nonZero \left({y}\right)}+ \%K}, \:{{integer \left({y + x}\right)}+ \%K}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{{nonZero \left({y}\right)}+{nonZero \left({x}\right)}+ \%L}, \:{{integer \left({y + x}\right)}+ \%L}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{\%M \ {integer \left({x}\right)}\ {integer \left({y}\right)}}, \:{\%M \ {integer \left({x \ y}\right)}}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{\%N \ {integer \left({x}\right)}\ {nonNegativeInteger \left({y}\right)}}, \:{\%N \ {integer \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{\%O \ {integer \left({x}\right)}\ {positiveInteger \left({y}\right)}}, \:{\%O \ {integer \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{\%P \ {integer \left({x}\right)}\ {nonZero \left({y}\right)}}, \:{\%P \ {integer \left({x \ y}\right)}}}\right)}, \: \right. \ \ \displaystyle \left.{= = \left({{\%Q \ {nonNegativeInteger \left({x}\right)}\ {nonNegativeInteger \left({y}\right)}}, \:{\%Q \ {nonNegativeInteger \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{\%R \ {nonNegativeInteger \left({x}\right)}\ {positiveInteger \left({y}\right)}}, \:{\%R \ {nonNegativeInteger \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{\%S \ {nonNegativeInteger \left({x}\right)}\ {nonZero \left({y}\right)}}, \:{\%S \ {integer \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{\%T \ {positiveInteger \left({x}\right)}\ {positiveInteger \left({y}\right)}}, \:{\%T \ {positiveInteger \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{\%U \ {nonNegativeInteger \left({y}\right)}\ {positiveInteger \left({x}\right)}}, \:{\%U \ {nonNegativeInteger \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\: \right. \ \ \displaystyle \left.{= = \left({{\%V \ {nonZero \left({y}\right)}\ {positiveInteger \left({x}\right)}}, \:{\%V \ {nonZero \left({x \ y}\right)}}}\right)}, \right. \ \ \displaystyle \left.\:{= = \left({{\%W \ {nonZero \left({x}\right)}\ {nonZero \left({y}\right)}}, \:{\%W \ {nonZero \left({x \ y}\right)}}}\right)}\right\}$

(2)

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

Check if x is in t.

fricas

check(x:Expression Integer,t:Symbol):Boolean ==
  --output("check: ",x::OutputForm)$OutputPackage
  p := normalForm markConstants x
  e := equation(p, normalForm markConstants assume(p,t))
  --output e
  e

   Function declaration check : (Expression(Integer), Symbol) -> 
      Boolean has been added to workspace.

Type: Void

Simplification

fricas

-- conditions in rules need to be unary functions
int1 := (m:Expression Integer):Boolean+->check(m,'integer)

fricas

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

fricas

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

$\label{eq3}\mbox{theMap (...)}$

(3)

Type: (Expression(Integer) -> Boolean)

fricas

simplifyAssumming := rule
  -- trig rules
  sin((n|int1(n))*2*%pi) == 0
  cos((n|int1(n))*2*%pi) == 1

$\label{eq4}\left\{{= = \left({{\sin \left({2 \ n \ \pi}\right)}, \: 0}\right)}, \:{= = \left({{\cos \left({2 \ n \ \pi}\right)}, \: 1}\right)}\right\}$

(4)

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

Tests

fricas

assume(x,'positiveInteger)

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

(5)

Type: Expression(Integer)

fricas

normalForm %

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

(6)

Type: Expression(Integer)

fricas

assume(x,'positiveInteger)+1

$\label{eq7}{positiveInteger \left({x}\right)}+ 1$

(7)

Type: Expression(Integer)

fricas

normalForm markConstants %

$\label{eq8}positiveInteger \left({x + 1}\right)$

(8)

Type: Expression(Integer)

fricas

assume(assume(x,'nonNegativeInteger),'positiveInteger)

$\label{eq9}positiveInteger \left({nonNegativeInteger \left({x}\right)}\right)$

(9)

Type: Expression(Integer)

fricas

normalForm %

$\label{eq10}positiveInteger \left({x}\right)$

(10)

Type: Expression(Integer)

fricas

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

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

(11)

Type: Boolean

fricas

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

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

(12)

Type: Boolean

fricas

check(3,'positiveInteger)

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

(13)

Type: Boolean

fricas

check(-3,'positiveInteger)

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

(14)

Type: Boolean

fricas

check(0,'positiveInteger)

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

(15)

Type: Boolean

fricas

--
assume(x,'nonNegativeInteger)

$\label{eq16}nonNegativeInteger \left({x}\right)$

(16)

Type: Expression(Integer)

fricas

normalForm %

$\label{eq17}nonNegativeInteger \left({x}\right)$

(17)

Type: Expression(Integer)

fricas

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

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

(18)

Type: Boolean

fricas

assume(x,'nonNegativeInteger)+1

$\label{eq19}{nonNegativeInteger \left({x}\right)}+ 1$

(19)

Type: Expression(Integer)

fricas

normalForm markConstants %

$\label{eq20}positiveInteger \left({x + 1}\right)$

(20)

Type: Expression(Integer)

fricas

assume(assume(x,'integer),'nonNegativeInteger)

$\label{eq21}nonNegativeInteger \left({integer \left({x}\right)}\right)$

(21)

Type: Expression(Integer)

fricas

normalForm %

$\label{eq22}nonNegativeInteger \left({x}\right)$

(22)

Type: Expression(Integer)

fricas

check(assume(x,'nonNegativeInteger),'nonNegativeInteger)

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

(23)

Type: Boolean

fricas

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

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

(24)

Type: Boolean

fricas

check(3,'nonNegativeInteger)

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

(25)

Type: Boolean

fricas

check(-3,'nonNegativeInteger)

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

(26)

Type: Boolean

fricas

check(0,'nonNegativeInteger)

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

(27)

Type: Boolean

fricas

--
assume(x,'integer)

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

(28)

Type: Expression(Integer)

fricas

normalForm %

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

(29)

Type: Expression(Integer)

fricas

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

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

(30)

Type: Boolean

fricas

assume(x,'integer)+1

$\label{eq31}{integer \left({x}\right)}+ 1$

(31)

Type: Expression(Integer)

fricas

normalForm markConstants %

$\label{eq32}integer \left({x + 1}\right)$

(32)

Type: Expression(Integer)

fricas

assume(assume(x,'integer),'integer)

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

(33)

Type: Expression(Integer)

fricas

normalForm %

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

(34)

Type: Expression(Integer)

fricas

check(assume(x,'integer),'integer)

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

(35)

Type: Boolean

fricas

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

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

(36)

Type: Boolean

fricas

check(3,'integer)

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

(37)

Type: Boolean

fricas

check(-3,'integer)

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

(38)

Type: Boolean

fricas

check(0,'integer)

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

(39)

Type: Boolean

fricas

--
simplifyAssumming sin(n*2*%pi)

$\label{eq40}\sin \left({2 \ n \ \pi}\right)$

(40)

Type: Expression(Integer)

fricas

simplifyAssumming sin(assume(n,'integer)*2*%pi)

$\label{eq41}0$

(41)

Type: Expression(Integer)

Dump domain cache

fricas

entries domainOfComp

$\label{eq42}\begin{array}{@{}l} \displaystyle \left[ positive , \: nonZero , \: positiveInteger , \: nonNegativeInteger , \: \right. \ \ \displaystyle \left.integer \right]$

(42)

Type: List(BasicOperator?)