Changes between Version 13 and Version 14 of Symbolic Expressions


Ignore:
Timestamp:
02/13/10 18:33:15 (16 years ago)
Author:
Stephen Siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Symbolic Expressions

    v13 v14  
    33Write here your thoughts on the new design of the symbolic module.
    44
    5 == Interface ==
     5== Organization ==
    66
    7 These are the items exported by the symbolic module:
     7The following directory/package structure will be used:
     8 * `symbolic.IF`: interface.  All items that will be exported go in here.
     9    * `symbolic.IF.type`
     10    * `symbolic.IF.expression`
     11 * `symbolic.real`: this is an implementation based on real-arithmetic and canonical forms.
     12    * `symbolic.real.type`
     13    * `symbolic.real.expression`
     14 * `SymbolicModule`
     15    * `public static SymbolicUniverseIF newRealUniverse();`
    816
    9 In symbolic.type:
    10  * SymbolicTypeIF
    11  * SymbolicPrimitiveTypeIF /* int, real, boolean */
    12  * SymbolicArrayTypeIF
    13     * SymbolicExpressionIF extent();
    14     * SymbolicExpressionIF elementType();
    15  * SymbolicTupleTypeIF
    16     * int numFields();
    17     * SymbolicTypeIF fieldType(int index);
    18  * SymbolicFunctionTypeIF
    19     * int numInputs();
    20     * SymbolicTypeIF inputType(int index);
    21     * SymbolicTypeIF outputType();
     17== Interface `symbolic.IF` ==
    2218
    23 In symbolic.expression:
    24  * SymbolicExpressionIF
    25     * int id(); /* every expression has a unique id number */
    26     * SymbolicTypeIF type();
    27  * SymbolicConstantIF extends SymbolicExpressionIF
    28  * ConcreteExpressionIF extends SymbolicExpressionIF
    29     * Rational value();
    30  * SymbolicFunctionIF extends SymbolicConstantIF
    31     * SymbolicFunctionTypeIF type();
    32  * SymbolicEvaluatedFunctionIF extends SymbolicExpressionIF
    33     * SymbolicFunctionIF function();
    34     * SymbolicExpressionIF argument(int index);
    35     * SymbolicExpressionIF[] arguments();
     19Package `symbolic.IF.type`:
     20 * `SymbolicTypeIF`
     21 * `SymbolicPrimitiveTypeIF` /* int, real, boolean */
     22 * `SymbolicArrayTypeIF`
     23    * `SymbolicExpressionIF extent();`
     24    * `SymbolicExpressionIF elementType();`
     25 * `SymbolicTupleTypeIF`
     26    * `int numFields();`
     27    * `SymbolicTypeIF fieldType(int index);`
     28 * `SymbolicFunctionTypeIF`
     29    * `int numInputs();`
     30    * `SymbolicTypeIF inputType(int index);`
     31    * `SymbolicTypeIF outputType();`
    3632
    37 In symbolic:
    38  * SymbolicUniverseIF
    39     * SymbolicPrimitiveTypeIF booleanType();
    40     * SymbolicPrimitiveTypeIF integerType();
    41     * SymbolicPrimitiveTypeIF realType();
    42     * SymbolicArrayTypeIF arrayType(SymbolicTypeIF elementType, SymbolicExpressionIF extent);
    43     * SymbolicTupleTypeIF tupleType(SymbolicTypeIF[] fieldTypes);
    44     * ConcreteExpressionIF concreteExpression(Rational rational);
    45     * ConcreteExpressionIF concreteExpression(int value);
    46     * ConcreteExpressionIF concreteExpression(double value);
    47     * SymbolicConstantIF symbolicConstant(SymbolicTypeIF type, String name);
    48     * SymbolicExpressionIF add(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    49     * SymbolicExpressionIF subtract(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    50     * SymbolicExpressionIF multiply(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    51     * SymbolicExpressionIF divide(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    52     * SymbolicExpressionIF minus(SymbolicExpressionIF arg);
    53     * SymbolicExpressionIF and(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    54     * SymbolicExpressionIF or(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    55     * SymbolicExpressionIF not(SymbolicExpressionIF arg);
    56     * SymbolicExpressionIF cond(SymbolicExpressionIF predicate, SymbolicExpressionIF trueValue, SymbolicExpressionIF falseValue);
    57     * SymbolicExpressionIF lessThan(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    58     * SymbolicExpressionIF lessThanEquals(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    59     * SymbolicExpressionIF equals(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    60     * SymbolicExpressionIF arrayRead(SymbolicExpressionIF array, SymbolicExpressionIF index);
    61     * SymbolicExpressionIF arrayWrite(SymbolicExpressionIF array, SymbolicExpressionIF index, SymbolicExpressionIF value);
    62     * SymbolicExpressionIF tupleRead(SymbolicExpressionIF tuple, int index);
    63     * SymbolicExpressionIF tupleWrite(SymbolicExpressionIF tuple, int index, SymbolicExpressionIF value);
    64  * SymbolicSimplifierIF
    65     * SymbolicExpressionIF newAssumption();
    66     * SymbolicExpressionIF simplify(SymbolicExpressionIF expression);
     33Package `symbolic.IF.expression`:
     34 * `SymbolicExpressionIF`
     35    * `int id();` /* every expression has a unique id number */
     36    * `SymbolicTypeIF type();`
     37 * `SymbolicConstantIF extends SymbolicExpressionIF`
     38 * `ConcreteExpressionIF extends SymbolicExpressionIF`
     39    * `Rational value();`
     40 * `SymbolicFunctionIF extends SymbolicConstantIF`
     41    * `SymbolicFunctionTypeIF type();`
     42 * `SymbolicEvaluatedFunctionIF extends SymbolicExpressionIF`
     43    * `SymbolicFunctionIF function();`
     44    * `SymbolicExpressionIF argument(int index);`
     45    * `SymbolicExpressionIF[] arguments();`
     46
     47package `symbolic`:
     48 * `SymbolicUniverseIF`
     49    * `SymbolicPrimitiveTypeIF booleanType();`
     50    * `SymbolicPrimitiveTypeIF integerType();`
     51    * `SymbolicPrimitiveTypeIF realType();`
     52    * `SymbolicArrayTypeIF arrayType(SymbolicTypeIF elementType, SymbolicExpressionIF extent);`
     53    * `SymbolicTupleTypeIF tupleType(SymbolicTypeIF[] fieldTypes);`
     54    * `ConcreteExpressionIF concreteExpression(Rational rational);`
     55    * `ConcreteExpressionIF concreteExpression(int value);`
     56    * `ConcreteExpressionIF concreteExpression(double value);`
     57    * `SymbolicConstantIF symbolicConstant(SymbolicTypeIF type, String name);`
     58    * `SymbolicExpressionIF add(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     59    * `SymbolicExpressionIF subtract(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     60    * `SymbolicExpressionIF multiply(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     61    * `SymbolicExpressionIF divide(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     62    * `SymbolicExpressionIF minus(SymbolicExpressionIF arg);`
     63    * `SymbolicExpressionIF and(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     64    * `SymbolicExpressionIF or(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     65    * `SymbolicExpressionIF not(SymbolicExpressionIF arg);`
     66    * `SymbolicExpressionIF cond(SymbolicExpressionIF predicate, SymbolicExpressionIF trueValue, SymbolicExpressionIF falseValue);`
     67    * `SymbolicExpressionIF lessThan(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     68    * `SymbolicExpressionIF lessThanEquals(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     69    * `SymbolicExpressionIF equals(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);`
     70    * `SymbolicExpressionIF arrayRead(SymbolicExpressionIF array, SymbolicExpressionIF index);`
     71    * `SymbolicExpressionIF arrayWrite(SymbolicExpressionIF array, SymbolicExpressionIF index, SymbolicExpressionIF value);`
     72    * `SymbolicExpressionIF tupleRead(SymbolicExpressionIF tuple, int index);`
     73    * `SymbolicExpressionIF tupleWrite(SymbolicExpressionIF tuple, int index, SymbolicExpressionIF value);`
     74 * `SymbolicSimplifierIF`
     75    * `SymbolicExpressionIF newAssumption();`
     76    * `SymbolicExpressionIF simplify(SymbolicExpressionIF expression);`
    6777 
    6878 
    6979In util we need to export:
    70 * Rational /* infinite precision rational numbers */
    71    * static Rational rational(int value);
    72    * static Rational rational(double value);
    73    * static Rational rational(BigInteger value);
    74    * static Rational add(Rational arg0, Rational arg1);
    75    * static Rational subtract(Rational arg0, Rational arg1);
    76    * static Rational multiply(Rational arg0, Rational arg1);
    77    * static Rational divide(Rational arg0, Rational arg1);
    78    * static Rational minus(Rational arg);
    79    * static int compare(Rational arg0, Rational arg1); /* +-0 */
    80    * boolean isInteger();
    81    * BigInteger intValue();
    82    * BigInteger numerator();
    83    * BigInteger denominator();
    84    * BigInteger floor();
    85    * BigInteger ceil();
    86    * boolean isGT0();
    87    * boolean isGTE0();
    88    * boolean is0();
     80 * `Rational` /* infinite precision rational numbers */
     81    * `static Rational rational(int value);`
     82    * `static Rational rational(double value);`
     83    * `static Rational rational(BigInteger value);`
     84    * `static Rational add(Rational arg0, Rational arg1);`
     85    * `static Rational subtract(Rational arg0, Rational arg1);`
     86    * `static Rational multiply(Rational arg0, Rational arg1);`
     87    * `static Rational divide(Rational arg0, Rational arg1);`
     88    * `static Rational minus(Rational arg);`
     89    * `static int compare(Rational arg0, Rational arg1);` /* +-0 */
     90    * `boolean isInteger();`
     91    * `BigInteger intValue();`
     92    * `BigInteger numerator();`
     93    * `BigInteger denominator();`
     94    * `BigInteger floor();`
     95    * `BigInteger ceil();`
     96    * `boolean isGT0();`
     97    * `boolean isGTE0();`
     98    * `boolean is0();`
    8999
    90 == Implementation ==
     100== Implementation: `symbolic.real` ==
    91101
    92 Package cexpression will implement the interface defined above.
     102Package `symbolic.real` will implement the interface defined above.
    93103The idea is to aggressively put every expression into a canonical form.  It assumes real arithmetic, so addition and multiplication are as in the real numbers.
    94104
    95105Additional Interfaces:
    96 * PrimitiveCExpressionIF
     106 * `PrimitiveExpression`
     107    * these are expressions that are not formed by numerical or logical operators
    97108    * classes implementing this interface
    98        * ArrayRead
    99        * ArrayWrite
    100        * TupleRead
    101        * TupleWrite
    102        * SymbolicConstant
    103        * RelationalCExpression
    104        * EvaluatedFunction
     109       * `ArrayRead`
     110       * `ArrayWrite`
     111       * `TupleRead`
     112       * `TupleWrite`
     113       * `SymbolicConstant`
     114       * `RelationalExpression`
     115       * `EvaluatedFunction`
     116       * `ConcreteExpression`
    105117
    106118Classes:
    107  * CExpression implements SymbolicExpressionIF
    108  * AndCExpression extends CExpression
    109     * clauses: set of OrCExpression
    110  * OrCExpression extends CExpression
    111     * clauses: set of BasicCExpression
    112  * BasicCExpression extends CExpression
    113     * boolean not(); /* if true insert not here */
    114     * PrimitiveCExpressionIF primitiveExpression();
    115  * RelationalCExpression extends CExpression implements PrimitiveCExpressionIF
    116    * enum RelationKind { GT0, EQ0 };
    117    * RelationKind kind();
    118    * PolynomialCExpression expression();
    119  * PolynomialCExpression extends CExpression
    120     * terms: set of MonomialCExpression
    121  * MonomialCExpression extends CExpression
    122     * coefficient: Rational
    123     * factors: set of pairs (PrimitiveCExpression, n), where n is a positive integer
    124  * RationalCExpression extends CExpression
    125     * numerator, denominator: PolynomialCExpression
     119 * `RealExpression implements SymbolicExpressionIF`
     120 * `ConcreteExpression extends RealExpression implements ConcreteExpressionIF`
     121 * `RealFunction extends RealExpression implements SymbolicFunctionIF`
     122 * `EvaluatedFunction extends RealExpression implements SymbolicEvaluatedFunctionIF`
     123 * `ArrayRead extends RealExpression`
     124 * `ArrayWrite extends RealExpression`
     125 * `TupleRead extends RealExpression`
     126 * `TupleWrite extends RealExpression`
     127 * `SymbolicConstant  extends RealExpression implements SymbolicConstantIF`
     128 * `AndExpression extends RealExpression`
     129    * clauses: set of `OrExpression`
     130 * `OrExpression extends RealExpression`
     131    * clauses: set of `BasicExpression`
     132 * `BasicExpression extends RealExpression`
     133    * `boolean not();` /* if true insert not operator here */
     134    * `PrimitiveExpression primitiveExpression();`
     135 * `RelationalExpression extends RealExpression implements PrimitiveExpression`
     136   * `enum RelationKind { GT0, EQ0 };`
     137   * `RelationKind kind();`
     138   * `Polynomial expression();`
     139 * `Polynomial extends RealExpression`
     140    * terms: set of `Monomial`
     141    * factorization: set of `Polynomial`
     142       * this is redundant information giving a factorization of the polynomial into polynomials of lower degree.  It is used for simplification.
     143 * `Monomial extends RealExpression`
     144    * coefficient: `Rational`
     145    * factors: set of pairs (`PrimitiveExpression X, int i`), where i>0, representing the product X_1^{i_1}...X_n^{i_n}
     146 * `RationalExpression extends RealExpression`
     147    * numerator, denominator: `Polynomial`
    126148
    127149Some facts which show how to put any expression into this canonical form:
    128  * x>=y <=> !(y-x>0)
    129  * x<y <=> y-x>0
    130  * x<=y <=> !(x-y>0)
     150 * `x>=y <=> !(y-x>0)`
     151 * `x<y <=> y-x>0`
     152 * `x<=y <=> !(x-y>0)`
     153 * `x>y <=> x-y>0`
     154 * `x!=y <=> !(x=y)`
     155 * `!(p&&q) <=> (!p)||(!q)`
     156 * `(p&&q)||r <=> (p||r)&&(q||r)`
     157 * `!(p||q) <=> (!p)&&(!q)`
    131158
    132 Big question: how to find command factors in denominator?
    133  
     159=== `RealExpressionFactory` ===
    134160
    135 === CExpressionFactory ===
    136 
    137  * CExpression symbolicConstant(...)
    138  * AndCExpression and(Collection<OrCExpression>)
    139  * OrCExpression or(Collection<BasicCExpression>)
     161`public class RealExpressionFactory`
     162 * `RealExpression symbolicConstant(...)`
     163 * `AndExpression and(Collection<OrExpression>)`
     164 * `OrExpression or(Collection<BasicExpression>)`
    140165etc.
    141166
    142167
    143 === CExpressionUniverse implements SymbolicUniverseIF ===
     168=== `RealUniverse implements SymbolicUniverseIF` ===
    144169
    145 uses CExpressionFactory
     170`public class RealUniverse implements SymbolicUniverseIF`
     171 * `RealExpression SymbolicConstant(...)`
     172 * `RealExpression and(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1)`
     173etc.
     174