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

# 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

-- 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
domainOfComp:=empty()$Table(Symbol,BasicOperator)  (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)  (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
 (3)
Type: (Expression(Integer) -> Boolean)
fricas
simplifyAssumming := rule
-- trig rules
sin((n|int1(n))*2*%pi) == 0
cos((n|int1(n))*2*%pi) == 1
 (4)
Type: Ruleset(Integer,Integer,Expression(Integer))

Tests

fricas
assume(x,'positiveInteger)
 (5)
Type: Expression(Integer)
fricas
normalForm %
 (6)
Type: Expression(Integer)
fricas
assume(x,'positiveInteger)+1
 (7)
Type: Expression(Integer)
fricas
normalForm markConstants %
 (8)
Type: Expression(Integer)
fricas
assume(assume(x,'nonNegativeInteger),'positiveInteger)
 (9)
Type: Expression(Integer)
fricas
normalForm %
 (10)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'positiveInteger)
 (11)
Type: Boolean
fricas
check(assume(x,'positiveInteger)+1,'positiveInteger)
 (12)
Type: Boolean
fricas
check(3,'positiveInteger)
 (13)
Type: Boolean
fricas
check(-3,'positiveInteger)
 (14)
Type: Boolean
fricas
check(0,'positiveInteger)
 (15)
Type: Boolean
fricas
--
assume(x,'nonNegativeInteger)
 (16)
Type: Expression(Integer)
fricas
normalForm %
 (17)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'nonNegativeInteger)
 (18)
Type: Boolean
fricas
assume(x,'nonNegativeInteger)+1
 (19)
Type: Expression(Integer)
fricas
normalForm markConstants %
 (20)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'nonNegativeInteger)
 (21)
Type: Expression(Integer)
fricas
normalForm %
 (22)
Type: Expression(Integer)
fricas
check(assume(x,'nonNegativeInteger),'nonNegativeInteger)
 (23)
Type: Boolean
fricas
check(assume(x,'nonNegativeInteger)+1,'nonNegativeInteger)
 (24)
Type: Boolean
fricas
check(3,'nonNegativeInteger)
 (25)
Type: Boolean
fricas
check(-3,'nonNegativeInteger)
 (26)
Type: Boolean
fricas
check(0,'nonNegativeInteger)
 (27)
Type: Boolean
fricas
--
assume(x,'integer)
 (28)
Type: Expression(Integer)
fricas
normalForm %
 (29)
Type: Expression(Integer)
fricas
check(assume(x,'positiveInteger),'integer)
 (30)
Type: Boolean
fricas
assume(x,'integer)+1
 (31)
Type: Expression(Integer)
fricas
normalForm markConstants %
 (32)
Type: Expression(Integer)
fricas
assume(assume(x,'integer),'integer)
 (33)
Type: Expression(Integer)
fricas
normalForm %
 (34)
Type: Expression(Integer)
fricas
check(assume(x,'integer),'integer)
 (35)
Type: Boolean
fricas
check(assume(x,'integer)+1,'integer)
 (36)
Type: Boolean
fricas
check(3,'integer)
 (37)
Type: Boolean
fricas
check(-3,'integer)
 (38)
Type: Boolean
fricas
check(0,'integer)
 (39)
Type: Boolean
fricas
--
simplifyAssumming sin(n*2*%pi)
 (40)
Type: Expression(Integer)
fricas
simplifyAssumming sin(assume(n,'integer)*2*%pi)
 (41)
Type: Expression(Integer)

Dump domain cache

fricas
entries domainOfComp
 (42)
Type: List(BasicOperator?)