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

This implementation of an Inductive (recursive) data type involves the categorical co-product construction. See: LimitsAndColimits

fricas
(1) -> )library colimits
fricas
Reading #P"/var/aw/var/LatexWiki/colimits.asy"
   Sum2 is now explicitly exposed in frame initial 
Sum2Functions is now explicitly exposed in frame initial
Sum3 is now explicitly exposed in frame initial
Sum3Functions is now explicitly exposed in frame initial

An example of Arithmetic Expressions as an Inductive Type

aldor
#pile
#include "axiom"
#library COLIMIT "colimits.ao"
import from COLIMIT
+++ Category of Integer-valued Arthemetic Expresions
ExprCat:Category == with eval: % -> Integer -- evaluates the expression as an Integer coerce: % -> OutputForm -- displays the expression
+++ Constructor for atomic Integers MkInt(Z:IntegerNumberSystem): ExprCat == add Rep == Integer -- Export eval(x:%):Integer == rep(x) coerce(x:%):OutputForm == outputForm rep x
+++ Constructor for additions MkAdd(X:ExprCat,Y:ExprCat): ExprCat == add Rep==Record(left:X,right:Y) import from Rep, OutputForm -- Local: plus(x:X,y:Y):OutputForm == paren(x::OutputForm + y::OutputForm); sum(x:X,y:Y):Integer == eval(x) + eval(y); -- Export: eval(x:%):Integer == sum explode rep x coerce(x:%):OutputForm == plus explode rep x
+++ Constructor for multiplications MkMul(X:ExprCat,Y:ExprCat): ExprCat == add Rep==Record(left:X,right:Y) import from Rep, OutputForm -- Local: times(x:X,y:Y):OutputForm== paren(x::OutputForm * y::OutputForm); product(x:X,y:Y):Integer == eval(x) * eval(y); -- Export: eval(x:%):Integer == product explode rep x coerce(x:%):OutputForm == times explode rep x
MI==>MkInt(Integer) MA==>MkAdd(%,%) MM==>MkMul(%,%)
+++ Constructor of Arithmetic Expressions over the Integers Expr: ExprCat == add Rep == Sum(MI,MA,MM) import from Rep, MI, MA, MM -- Export: eval(x:%):Integer == sum(Integer,eval,eval,eval)(rep x) coerce(x:%):OutputForm == sum(OutputForm,coerce,coerce,coerce)(rep x)
aldor
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/expr.as using
      Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/expr.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.

Now extend it to provide the Axiom interpreter interface.

aldor
#pile
#include "axiom"
#library EXPR "expr.ao"
import from EXPR
#library COLIMIT "colimits.ao"
import from COLIMIT
extend MkInt(Z:IntegerNumberSystem): with coerce: Z -> % -- converts a Z-valued object to an atomic Integer == add Rep == Integer -- Export coerce(i:Z):% == per(convert(i))
extend MkAdd(X:ExprCat,Y:ExprCat): with +: (X,Y) -> % -- returns an expression representing the sum == add Rep==Record(left:X,right:Y) import from Rep -- Export ((x:X) + (y:Y)):% == per [x,y]
extend MkMul(X:ExprCat,Y:ExprCat): with *: (X,Y) -> % -- returns an expression representing the product == add Rep==Record(left:X,right:Y) import from Rep -- Export ((x:X) * (y:Y)):% == per [x,y]
MI==>MkInt(Integer) MA==>MkAdd(%,%) MM==>MkMul(%,%)
+++ extends domain Expr as above extend Expr: with coerce: Integer -> % +:(%,%) -> % *:(%,%) -> % == add Rep == Sum(MI,MA,MM) import from Rep, MI, MA, MM -- Export: coerce(n: Integer):% == per(inject( n::MI )) ((x:%) + (y:%)):% == per(inject( (x + y)$MA )) ((x:%) * (y:%)):% == per(inject( (x * y)$MM ))
aldor
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1062037838131250571-25px003.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/1062037838131250571-25px003.as", line 2: 
#include "axiom"
^
[L2 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.

fricas
n:Expr:=3
Expr is not a valid type.

Ralf Hemmecke and Bill Page wrote:

Recursive Types

aldor
#include "axiom"
RecExpr:with {
    coerce: Integer -> %;
    +: (%, %) -> %;
    *: (%, %) -> %;
    coerce: % -> OutputForm;
    eval: % -> Integer;
}  == add {
    Rep == Union(MakeInt:Integer,
                 MakeAdd:Record(l:%, r:%),
                 MakeMul:Record(l:%, r:%));
    import from Rep;
    import from 'MakeInt', 'MakeAdd', 'MakeMul';
    import from OutputForm;
    --
    -- Local
    plus(x:%,y:%):OutputForm == paren(x::OutputForm + y::OutputForm);
    times(x:%,y:%):OutputForm== paren(x::OutputForm * y::OutputForm);
    sum(x:%,y:%):Integer     == eval(x) + eval(y);
    product(x:%,y:%):Integer == eval(x) * eval(y);
    --
    -- Input
    coerce(n: Integer):% == per [MakeInt==n];
    ((x:%) + (y:%)): %   == per [MakeAdd==[x,y]];
    ((x:%) * (y:%)): %   == per [MakeMul==[x,y]];
    --
    -- Output
    coerce(i:%):OutputForm == { n:=rep(i);
      n case MakeInt => outputForm    n.MakeInt;
      n case MakeAdd => plus  explode n.MakeAdd;
      n case MakeMul => times explode n.MakeMul;
      never;
    };
    --
    -- Evaluation
    eval(i:%):Integer == { n:=rep(i);
      n case MakeInt =>                 n.MakeInt;
      n case MakeAdd => sum     explode n.MakeAdd;
      n case MakeMul => product explode n.MakeMul;
      never;
    }
}
aldor
   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      Use the system command )set compiler args to change these 
      options.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/4075514935174965511-25px005.as", line 1: 
#include "axiom"
^
[L1 C1] #1 (Error) Could not open file `axiom'.
The )library system command was not called after compilation.

Here is an example expression

fricas
10::RecExpr
RecExpr is not a valid type.




  Subject:   Be Bold !!
  ( 15 subscribers )  
Please rate this page: